%------------------------------------------------------------------------------ % File : Nitpick---2016 % Problem : LCL687-10.015 : TPTP v7.3.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : isabelle tptp_nitpick %d %s % Computer : n184.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.5MB % OS : Linux 3.10.0-862.11.6.el7.x86_64 % CPULimit : 300s % DateTime : Wed Feb 27 13:24:53 EST 2019 % Result : Satisfiable 64.24s % Output : FiniteModel 64.24s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : LCL687-10.015 : TPTP v7.3.0. Released v7.3.0. % 0.00/0.06 % Command : isabelle tptp_nitpick %d %s % 0.03/0.26 % Computer : n184.star.cs.uiowa.edu % 0.03/0.26 % Model : x86_64 x86_64 % 0.03/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.26 % Memory : 32218.5MB % 0.03/0.26 % OS : Linux 3.10.0-862.11.6.el7.x86_64 % 0.03/0.26 % CPULimit : 300 % 0.03/0.26 % DateTime : Thu Feb 21 22:52:00 CST 2019 % 0.03/0.26 % CPUTime : % 14.87/4.76 Building HOL-TPTP ... % 44.51/22.19 Finished HOL-TPTP (0:00:16 elapsed time, 0:00:28 cpu time, factor 1.68) % 44.55/22.27 0:00:20 elapsed time, 0:00:28 cpu time, factor 1.35 % 64.24/37.45 Nitpicking formula... % 64.24/37.45 Timestamp: 22:52:27 % 64.24/37.45 Using SAT solver "Lingeling_JNI" The following solvers are configured: % 64.24/37.45 "Lingeling_JNI", "CryptoMiniSat_JNI", "MiniSat_JNI", "SAT4J", "SAT4J_Light" % 64.24/37.45 Batch 1 of 20: Trying 5 scopes: % 64.24/37.45 card TPTP_Interpret.ind = 1 % 64.24/37.45 card TPTP_Interpret.ind = 2 % 64.24/37.45 card TPTP_Interpret.ind = 3 % 64.24/37.45 card TPTP_Interpret.ind = 4 % 64.24/37.45 card TPTP_Interpret.ind = 5 % 64.24/37.45 % SZS status Satisfiable % SZS output start FiniteModel % 64.24/37.45 Nitpick found a model for card TPTP_Interpret.ind = 2: % 64.24/37.45 % 64.24/37.45 Constants: % 64.24/37.45 bnd_ifeq = % 64.24/37.45 (\<lambda>x. _) % 64.24/37.45 (i1 := (\<lambda>x. _) % 64.24/37.45 (i1 := (\<lambda>x. _) % 64.24/37.45 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1), % 64.24/37.45 i2 := (\<lambda>x. _)(i1 := i2, i2 := i2)), % 64.24/37.45 i2 := (\<lambda>x. _) % 64.24/37.45 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1), % 64.24/37.45 i2 := (\<lambda>x. _)(i1 := i2, i2 := i2))), % 64.24/37.45 i2 := (\<lambda>x. _) % 64.24/37.45 (i1 := (\<lambda>x. _) % 64.24/37.45 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1), % 64.24/37.45 i2 := (\<lambda>x. _)(i1 := i1, i2 := i1)), % 64.24/37.45 i2 := (\<lambda>x. _) % 64.24/37.45 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1), % 64.24/37.45 i2 := (\<lambda>x. _)(i1 := i2, i2 := i2)))) % 64.24/37.45 bnd_p1 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p10 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p11 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p12 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p13 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p14 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p15 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p16 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p17 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p18 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p19 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p2 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p20 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p21 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p22 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p23 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p24 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p25 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p26 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p27 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p28 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p29 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p3 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p30 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p31 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p32 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p33 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p34 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p35 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p36 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p37 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p38 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p39 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p4 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p40 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p41 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p42 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p43 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p44 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p45 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p46 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p47 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p48 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p49 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p5 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p50 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p51 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p52 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p53 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p54 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p55 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p56 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p57 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p58 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p59 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p6 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p60 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p61 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p62 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p63 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p64 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p65 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p66 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p67 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p68 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p69 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p7 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p70 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p71 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p72 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p73 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p74 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p75 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p76 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p77 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p78 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p79 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p8 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p80 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p81 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p82 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p83 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p84 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p85 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p9 = (\<lambda>x. _)(i1 := i2, i2 := i2) % 64.24/37.45 bnd_p90 = (\<lambda>x. _)(i1 := i1, i2 := i2) % 64.24/37.45 bnd_r1 = % 64.24/37.45 (\<lambda>x. _) % 64.24/37.45 (i1 := (\<lambda>x. _)(i1 := i2, i2 := i2), % 64.24/37.45 i2 := (\<lambda>x. _)(i1 := i2, i2 := i2)) % 64.24/37.45 bnd_sK10_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK11_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK12_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK13_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK14_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK15_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK16_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK17_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK18_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK19_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK1_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK20_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK21_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK22_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK23_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK24_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK25_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK26_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK27_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK28_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK29_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK2_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK30_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK31_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK32_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK33_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK34_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK35_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK36_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK37_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK38_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK39_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK3_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK40_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK41_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK42_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK43_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK44_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK45_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK46_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK47_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK48_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK49_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK4_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK50_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK51_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK52_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK53_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK54_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK55_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK56_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK57_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK58_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK59_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK5_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK60_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK61_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK62_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK63_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK64_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK65_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK66_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK67_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK68_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK69_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK6_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK70_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK71_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK72_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK73_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK74_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK75_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK76_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK77_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK78_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK79_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK7_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK80_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK81_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK82_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK83_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK84_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK85_main_Y = (\<lambda>x. _)(i1 := i2, i2 := i1) % 64.24/37.45 bnd_sK86_main_Y = i1 % 64.24/37.45 bnd_sK87_main_X = i1 % 64.24/37.45 bnd_sK88_main_Y = i2 % 64.24/37.45 bnd_sK89_main_X = i1 % 64.24/37.45 bnd_sK8_main_X = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_sK9_main_Y = (\<lambda>x. _)(i1 := i1, i2 := i1) % 64.24/37.45 bnd_true = i2 % 64.24/37.45 bnd_tuple = % 64.24/37.45 (\<lambda>x. _) % 64.24/37.45 (i1 := (\<lambda>x. _)(i1 := i2, i2 := i1), % 64.24/37.45 i2 := (\<lambda>x. _)(i1 := i2, i2 := i1)) % 64.24/37.45 % SZS output end FiniteModel % 64.24/37.45 Total time: 9.6 s %------------------------------------------------------------------------------