WATCH: 0.00 CPU 0.01 WC
cp: `/tmp/IsabelleP_25649_cl5-025/TTN012.thy' and `/tmp/IsabelleP_25649_cl5-025/TTN012.thy' are the same file

WATCH: 2.69 CPU 3.02 WC
Nitpick found a counterexample for card 'i = 2:

  Free variables:
    cF = (%x. _)
         (i1 := (%x. _)(i1 := i1, i2 := i1),
          i2 := (%x. _)(i1 := i1, i2 := i1))
    cG = (%x. _)(i1 := i2, i2 := i1)
    cK = i1
    cP = {}
    cR = (%x. _)(i1 := {i1}, i2 := {})
  Skolem constants:
    Q = (%x. _)(i1 := {}, i2 := {})
    X = i2
    Y = i1
Total time: 2.59 s.
% SZS status CounterSatisfiable for TTN012 : TTN012
val it = (): unit
ML> 
% Removing Isabelle's /tmp/IsabelleP_25649_cl5-025

WATCH: 14.84 CPU 5.35 WC

FINAL WATCH: 14.84 CPU 5.35 WC