%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYO607+1 : TPTP v8.2.0. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 20:27:30 EDT 2024 % Result : Theorem 13.01s 13.06s % Output : CNFRefutation 13.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYO607+1 : TPTP v8.2.0. Released v7.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n018.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 07:04:54 EDT 2024 % 0.13/0.34 % CPUTime : % 0.49/0.60 start to proof:theBenchmark % 12.96/13.05 %------------------------------------------- % 12.96/13.05 % File :CSE---1.7 % 12.96/13.05 % Problem :theBenchmark % 12.96/13.05 % Transform :cnf % 12.96/13.05 % Format :tptp:raw % 12.96/13.05 % Command :java -jar mcs_scs.jar %d %s % 12.96/13.05 % 12.96/13.05 % Result :Theorem 12.400000s % 12.96/13.05 % Output :CNFRefutation 12.400000s % 12.96/13.05 %------------------------------------------- % 13.01/13.05 %------------------------------------------------------------------------------ % 13.01/13.05 % File : SYO607+1 : TPTP v8.2.0. Released v7.0.0. % 13.01/13.05 % Domain : Syntactic % 13.01/13.05 % Problem : RM3 problem 6 % 13.01/13.05 % Version : Especial. % 13.01/13.05 % English : % 13.01/13.05 % 13.01/13.05 % Refs : [Pel16] Pelletier (2016), Email to Geoff Sutcliffe % 13.01/13.05 % : [PSH17] Pelletier et al. (2017), Automated Reasoning for the D % 13.01/13.05 % Source : [Pel16] % 13.01/13.05 % Names : n06.p [Pel16] % 13.01/13.05 % 13.01/13.05 % Status : Theorem % 13.01/13.05 % Rating : 0.00 v7.5.0, 0.05 v7.4.0, 0.00 v7.0.0 % 13.01/13.05 % Syntax : Number of formulae : 5 ( 0 unt; 0 def) % 13.01/13.05 % Number of atoms : 25 ( 0 equ) % 13.01/13.05 % Maximal formula atoms : 13 ( 5 avg) % 13.01/13.05 % Number of connectives : 28 ( 8 ~; 5 |; 12 &) % 13.01/13.05 % ( 3 <=>; 0 =>; 0 <=; 0 <~>) % 13.01/13.05 % Maximal formula depth : 10 ( 6 avg) % 13.01/13.05 % Maximal term depth : 1 ( 1 avg) % 13.01/13.05 % Number of predicates : 5 ( 5 usr; 0 prp; 2-2 aty) % 13.01/13.05 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 13.01/13.05 % Number of variables : 23 ( 11 !; 12 ?) % 13.01/13.05 % SPC : FOF_THM_RFO_NEQ % 13.01/13.05 % 13.01/13.05 % Comments : Translated from RM3 using the truth evaluation approach [PSH17]. % 13.01/13.05 %------------------------------------------------------------------------------ % 13.01/13.05 fof(nc6,conjecture, % 13.01/13.05 ( ? [A] : % 13.01/13.05 ( g_false_only(a,A) % 13.01/13.05 & ? [B] : g_false_only(A,B) ) % 13.01/13.05 | ? [A] : % 13.01/13.05 ! [B] : g_true_only(A,B) % 13.01/13.05 | ( ? [A] : % 13.01/13.05 ( ( g_both(a,A) % 13.01/13.05 | ( ? [B] : g_both(A,B) % 13.01/13.05 & ~ ? [B] : g_false_only(A,B) ) ) % 13.01/13.05 & ~ g_true_only(a,A) % 13.01/13.05 & ~ ! [B] : g_true_only(A,B) ) % 13.01/13.05 & ~ ? [A] : % 13.01/13.05 ( g_false_only(a,A) % 13.01/13.05 & ? [B] : g_false_only(A,B) ) % 13.01/13.05 & ? [A] : % 13.01/13.05 ( ? [B] : g_both(A,B) % 13.01/13.05 & ~ ? [B] : g_false_only(A,B) ) % 13.01/13.05 & ~ ? [A] : % 13.01/13.05 ! [B] : g_true_only(A,B) ) ) ). % 13.01/13.05 % 13.01/13.05 fof(true_only_g,axiom, % 13.01/13.05 ! [X_2,X_1] : % 13.01/13.05 ( g_true_only(X_2,X_1) % 13.01/13.05 <=> ( g_true(X_2,X_1) % 13.01/13.05 & ~ g_false(X_2,X_1) ) ) ). % 13.01/13.05 % 13.01/13.05 fof(both_g,axiom, % 13.01/13.05 ! [X_2,X_1] : % 13.01/13.05 ( g_both(X_2,X_1) % 13.01/13.05 <=> ( g_true(X_2,X_1) % 13.01/13.05 & g_false(X_2,X_1) ) ) ). % 13.01/13.05 % 13.01/13.06 fof(false_only_g,axiom, % 13.01/13.06 ! [X_2,X_1] : % 13.01/13.06 ( g_false_only(X_2,X_1) % 13.01/13.06 <=> ( g_false(X_2,X_1) % 13.01/13.06 & ~ g_true(X_2,X_1) ) ) ). % 13.01/13.06 % 13.01/13.06 fof(exhaustion_g,axiom, % 13.01/13.06 ! [X_2,X_1] : % 13.01/13.06 ( g_true_only(X_2,X_1) % 13.01/13.06 | g_both(X_2,X_1) % 13.01/13.06 | g_false_only(X_2,X_1) ) ). % 13.01/13.06 % 13.01/13.06 %------------------------------------------------------------------------------ % 13.01/13.06 %------------------------------------------- % 13.01/13.06 % Proof found % 13.01/13.06 % SZS status Theorem for theBenchmark % 13.01/13.06 % SZS output start Proof % 13.01/13.06 %ClaNum:16(EqnAxiom:0) % 13.01/13.06 %VarNum:95(SingletonVarNum:45) % 13.01/13.06 %MaxLitNum:8 % 13.01/13.06 %MaxfuncDepth:1 % 13.01/13.06 %SharedTerms:6 % 13.01/13.06 %goalClause: 1 6 13 14 15 16 % 13.01/13.06 %singleGoalClaCount:1 % 13.01/13.06 [1]~P1(x11,f1(x11)) % 13.01/13.06 [2]~P1(x21,x22)+P2(x21,x22) % 13.01/13.06 [3]~P3(x31,x32)+P2(x31,x32) % 13.01/13.06 [4]~P5(x41,x42)+P4(x41,x42) % 13.01/13.06 [5]~P3(x51,x52)+P4(x51,x52) % 13.01/13.06 [6]~P5(x61,x62)+~P5(a2,x61) % 13.01/13.06 [8]~P2(x81,x82)+~P5(x81,x82) % 13.01/13.06 [9]~P4(x91,x92)+~P1(x91,x92) % 13.01/13.06 [7]P1(x71,x72)+P3(x71,x72)+P5(x71,x72) % 13.01/13.06 [10]P2(x101,x102)+~P4(x101,x102)+P5(x101,x102) % 13.01/13.06 [11]P4(x111,x112)+~P2(x111,x112)+P1(x111,x112) % 13.01/13.06 [12]~P2(x121,x122)+~P4(x121,x122)+P3(x121,x122) % 13.01/13.06 [13]P1(x131,x132)+~P3(x134,x135)+P1(a2,x131)+~P3(a2,x131)+P5(x134,f4(x134))+P1(a3,x133)+P5(a2,a5) % 13.01/13.06 [14]P1(x141,x142)+~P3(x144,x145)+P1(a2,x141)+~P3(a2,x141)+P5(x144,f4(x144))+P1(a3,x143)+P5(a5,a7) % 13.01/13.06 [15]P1(x151,x152)+~P3(x154,x155)+~P3(x151,x156)+P1(a2,x151)+P5(x151,f6(x151))+P5(x154,f4(x154))+P1(a3,x153)+P5(a2,a5) % 13.01/13.06 [16]P1(x161,x162)+~P3(x164,x165)+~P3(x161,x166)+P1(a2,x161)+P5(x161,f6(x161))+P5(x164,f4(x164))+P1(a3,x163)+P5(a5,a7) % 13.01/13.06 %EqnAxiom % 13.01/13.06 % 13.01/13.06 %------------------------------------------- % 13.01/13.07 cnf(17,plain, % 13.01/13.07 (~P1(x171,f1(x171))), % 13.01/13.07 inference(rename_variables,[],[1])). % 13.01/13.07 cnf(19,plain, % 13.01/13.07 (P1(f1(a2),x191)+~P3(x192,x193)+~P3(f1(a2),x194)+P5(f1(a2),f6(f1(a2)))+P5(a2,a5)+P5(x192,f4(x192))+P1(a3,x195)), % 13.01/13.07 inference(scs_inference,[],[1,17,15])). % 13.01/13.07 cnf(20,plain, % 13.01/13.07 (P1(x201,x202)+~P3(x203,x204)+P1(a2,x201)+~P3(a2,x201)+P5(x203,f4(x203))+P5(a2,a5)), % 13.01/13.07 inference(scs_inference,[],[1,13])). % 13.01/13.07 cnf(21,plain, % 13.01/13.07 (P1(x211,x212)+~P3(x213,x214)+P1(a2,x211)+~P3(a2,x211)+P5(x213,f4(x213))+P5(a5,a7)), % 13.01/13.07 inference(scs_inference,[],[1,14])). % 13.01/13.07 cnf(23,plain, % 13.01/13.07 (P1(x231,x232)+~P3(x233,x234)+~P3(x231,x235)+P1(a2,x231)+P5(x231,f6(x231))+P5(x233,f4(x233))+P5(a5,a7)), % 13.01/13.07 inference(scs_inference,[],[1,16])). % 13.01/13.07 cnf(25,plain, % 13.01/13.07 (P5(x251,f4(x251))+P1(f1(a2),x252)+~P3(x251,x253)+P5(a2,a5)+~P3(a2,f1(a2))), % 13.01/13.07 inference(scs_inference,[],[1,20])). % 13.01/13.07 cnf(26,plain, % 13.01/13.07 (P5(x261,f4(x261))+~P3(x261,x262)+P1(f1(a2),x263)+~P3(f1(a2),x264)+P5(f1(a2),f6(f1(a2)))+P5(a2,a5)), % 13.01/13.07 inference(scs_inference,[],[1,19])). % 13.01/13.07 cnf(28,plain, % 13.01/13.07 (P5(x281,f4(x281))+P1(f1(a2),x282)+~P3(x281,x283)+P5(a5,a7)+~P3(a2,f1(a2))), % 13.01/13.07 inference(scs_inference,[],[1,21])). % 13.01/13.07 cnf(29,plain, % 13.01/13.07 (P5(x291,f4(x291))+~P3(x291,x292)+~P3(a2,f1(a2))+P5(a2,a5)), % 13.01/13.07 inference(scs_inference,[],[1,25])). % 13.01/13.07 cnf(32,plain, % 13.01/13.07 (P5(x321,f4(x321))+~P3(x321,x322)+~P3(f1(a2),x323)+P5(f1(a2),f6(f1(a2)))+P5(a2,a5)), % 13.01/13.07 inference(scs_inference,[],[1,26])). % 13.01/13.07 cnf(33,plain, % 13.01/13.07 (P5(x331,f4(x331))+~P3(x331,x332)+~P3(a2,f1(a2))+P5(a5,a7)), % 13.01/13.07 inference(scs_inference,[],[1,28])). % 13.01/13.07 cnf(42,plain, % 13.01/13.07 (~P5(x421,x422)+~P1(x421,x422)), % 13.01/13.07 inference(scs_inference,[],[2,8])). % 13.01/13.07 cnf(73,plain, % 13.01/13.07 (~P5(x731,x732)+~P3(x731,x732)), % 13.01/13.07 inference(scs_inference,[],[3,8])). % 13.01/13.07 cnf(166,plain, % 13.01/13.07 (P3(x1661,f1(x1661))+~P5(a2,x1661)), % 13.01/13.07 inference(scs_inference,[],[1,6,7])). % 13.01/13.07 cnf(657,plain, % 13.01/13.07 (P2(x6571,x6572)+P3(x6571,x6572)+P5(x6571,x6572)), % 13.01/13.07 inference(scs_inference,[],[2,7])). % 13.01/13.07 cnf(688,plain, % 13.01/13.07 (P5(x6881,x6882)+P2(x6881,x6882)), % 13.01/13.07 inference(scs_inference,[],[657,3])). % 13.01/13.07 cnf(1116,plain, % 13.01/13.07 (P4(x11161,x11162)+P2(x11161,x11162)), % 13.01/13.07 inference(scs_inference,[],[4,688])). % 13.01/13.07 cnf(1147,plain, % 13.01/13.07 (P4(x11471,f1(x11471))), % 13.01/13.07 inference(scs_inference,[],[1,1116,11])). % 13.01/13.07 cnf(1148,plain, % 13.01/13.07 (P3(x11481,f1(x11481))+~P2(x11481,f1(x11481))), % 13.01/13.07 inference(scs_inference,[],[1147,12])). % 13.01/13.07 cnf(1182,plain, % 13.01/13.07 (P3(x11821,f1(x11821))+P5(x11821,f1(x11821))), % 13.01/13.07 inference(scs_inference,[],[1148,688])). % 13.01/13.07 cnf(1243,plain, % 13.01/13.07 (P3(a2,f1(a2))+~P5(f1(a2),x12431)), % 13.01/13.07 inference(scs_inference,[],[1182,6])). % 13.01/13.07 cnf(1274,plain, % 13.01/13.07 (P2(f1(a2),x12741)+P3(a2,f1(a2))), % 13.01/13.07 inference(scs_inference,[],[1243,688])). % 13.01/13.07 cnf(1488,plain, % 13.01/13.07 (P2(a2,x14881)+~P5(x14881,x14882)), % 13.01/13.07 inference(scs_inference,[],[6,688])). % 13.01/13.07 cnf(1519,plain, % 13.01/13.07 (P3(x15191,f1(x15191))+P2(a2,x15191)), % 13.01/13.07 inference(scs_inference,[],[1488,1182])). % 13.01/13.07 cnf(1611,plain, % 13.01/13.07 (P2(x16111,x16112)+~P5(a2,x16111)), % 13.01/13.07 inference(scs_inference,[],[6,688])). % 13.01/13.07 cnf(1642,plain, % 13.01/13.07 (P2(a2,x16421)+P2(x16421,x16422)), % 13.01/13.07 inference(scs_inference,[],[1611,688])). % 13.01/13.07 cnf(2664,plain, % 13.01/13.07 (~P2(a2,f1(a2))+P5(a2,f4(a2))+P5(a2,a5)), % 13.01/13.07 inference(scs_inference,[],[1148,29])). % 13.01/13.07 cnf(2911,plain, % 13.01/13.07 (~P2(a2,f1(a2))+P5(a2,f4(a2))+P5(a5,a7)), % 13.01/13.07 inference(scs_inference,[],[1148,33])). % 13.01/13.07 cnf(3188,plain, % 13.01/13.07 (P5(a2,f1(a2))+P5(a2,f4(a2))+P5(a2,a5)), % 13.01/13.07 inference(scs_inference,[],[1182,29])). % 13.01/13.07 cnf(3219,plain, % 13.01/13.07 (~P5(f4(a2),x32191)+P5(a2,f1(a2))+P5(a2,a5)), % 13.01/13.07 inference(scs_inference,[],[3188,6])). % 13.01/13.07 cnf(3250,plain, % 13.01/13.07 (~P2(a2,f1(a2))+~P5(f4(a2),x32501)+P5(a2,a5)), % 13.01/13.07 inference(scs_inference,[],[3219,8])). % 13.01/13.07 cnf(3744,plain, % 13.01/13.07 (P5(a2,f1(a2))+P5(a2,f4(a2))+P5(a5,a7)), % 13.01/13.07 inference(scs_inference,[],[1182,33])). % 13.01/13.07 cnf(3775,plain, % 13.01/13.07 (~P5(f4(a2),x37751)+P5(a2,f1(a2))+P5(a5,a7)), % 13.01/13.07 inference(scs_inference,[],[3744,6])). % 13.01/13.07 cnf(3806,plain, % 13.01/13.07 (~P2(a2,f1(a2))+~P5(f4(a2),x38061)+P5(a5,a7)), % 13.01/13.07 inference(scs_inference,[],[3775,8])). % 13.01/13.07 cnf(3837,plain, % 13.01/13.07 (~P3(a2,f1(a2))+~P5(f4(a2),x38371)+P5(a5,a7)), % 13.01/13.07 inference(scs_inference,[],[3806,3])). % 13.01/13.07 cnf(4115,plain, % 13.01/13.07 (P3(f4(a2),f1(f4(a2)))+~P2(a2,f1(a2))+P5(a2,a5)), % 13.01/13.07 inference(scs_inference,[],[1182,3250])). % 13.01/13.07 cnf(4762,plain, % 13.01/13.07 (P3(f4(a2),f1(f4(a2)))+~P3(a2,f1(a2))+P5(a5,a7)), % 13.01/13.07 inference(scs_inference,[],[1182,3837])). % 13.01/13.07 cnf(4793,plain, % 13.01/13.07 (P3(f4(a2),f1(f4(a2)))+P2(f1(a2),x47931)+P5(a5,a7)), % 13.01/13.07 inference(scs_inference,[],[4762,1274])). % 13.01/13.07 cnf(4824,plain, % 13.01/13.07 (P2(f4(a2),f1(f4(a2)))+P2(f1(a2),x48241)+P5(a5,a7)), % 13.01/13.07 inference(scs_inference,[],[4793,3])). % 13.01/13.07 cnf(4855,plain, % 13.01/13.07 (P2(f4(a2),f1(f4(a2)))+P2(f1(a2),x48551)+~P5(a2,a5)), % 13.01/13.07 inference(scs_inference,[],[4824,6])). % 13.01/13.07 cnf(4886,plain, % 13.01/13.07 (P3(f4(a2),f1(f4(a2)))+P2(f1(a2),x48861)+~P5(a2,a5)), % 13.01/13.07 inference(scs_inference,[],[1147,4855,12])). % 13.01/13.07 cnf(7097,plain, % 13.01/13.07 (~P4(x70971,f1(x70971))+~P3(a2,f1(a2))+P5(x70971,f4(x70971))+~P2(x70971,f1(x70971))+P5(a2,a5)), % 13.01/13.07 inference(scs_inference,[],[1147,12,29])). % 13.01/13.07 cnf(7313,plain, % 13.01/13.07 (~P4(x73131,f1(x73131))+~P3(a2,f1(a2))+P5(x73131,f4(x73131))+~P2(x73131,f1(x73131))+P5(a5,a7)), % 13.01/13.07 inference(scs_inference,[],[1147,12,33])). % 13.01/13.07 cnf(7560,plain, % 13.01/13.07 (P3(f1(a2),f1(f1(a2)))+P3(f4(a2),f1(f4(a2)))+~P5(a2,a5)), % 13.01/13.07 inference(scs_inference,[],[1147,12,4886])). % 13.01/13.07 cnf(7591,plain, % 13.01/13.07 (P3(f1(a2),f1(f1(a2)))+P3(f4(a2),f1(f4(a2)))+~P2(a2,f1(a2))), % 13.01/13.07 inference(scs_inference,[],[7560,4115])). % 13.01/13.07 cnf(7622,plain, % 13.01/13.07 (P2(f1(a2),f1(f1(a2)))+P3(f4(a2),f1(f4(a2)))+~P2(a2,f1(a2))), % 13.01/13.07 inference(scs_inference,[],[7591,3])). % 13.01/13.07 cnf(7653,plain, % 13.01/13.07 (P2(f4(a2),f1(f4(a2)))+P2(f1(a2),f1(f1(a2)))+~P2(a2,f1(a2))), % 13.01/13.07 inference(scs_inference,[],[7622,3])). % 13.01/13.07 cnf(7684,plain, % 13.01/13.07 (P3(f1(a2),f1(f1(a2)))+~P2(a2,f1(a2))+P2(f4(a2),f1(f4(a2)))), % 13.01/13.07 inference(scs_inference,[],[1147,7653,12])). % 13.01/13.07 cnf(7715,plain, % 13.01/13.07 (P3(f1(a2),f1(f1(a2)))+P2(f4(a2),f1(f4(a2)))), % 13.01/13.08 inference(scs_inference,[],[7684,1519])). % 13.01/13.08 cnf(7746,plain, % 13.01/13.08 (P2(f1(a2),f1(f1(a2)))+P2(f4(a2),f1(f4(a2)))), % 13.01/13.08 inference(scs_inference,[],[7715,3])). % 13.01/13.08 cnf(7777,plain, % 13.01/13.08 (P3(f4(a2),f1(f4(a2)))+P2(f1(a2),f1(f1(a2)))), % 13.01/13.08 inference(scs_inference,[],[1147,7746,12])). % 13.01/13.08 cnf(7808,plain, % 13.01/13.08 (P3(f1(a2),f1(f1(a2)))+P3(f4(a2),f1(f4(a2)))), % 13.01/13.08 inference(scs_inference,[],[1147,7777,12])). % 13.01/13.08 cnf(9404,plain, % 13.01/13.08 (~P5(a5,x94041)+P5(a2,f4(a2))+~P2(a2,f1(a2))), % 13.01/13.08 inference(scs_inference,[],[2664,6])). % 13.01/13.08 cnf(11956,plain, % 13.01/13.08 (~P2(a2,f1(a2))+P5(a2,f4(a2))), % 13.01/13.08 inference(scs_inference,[],[2911,9404])). % 13.01/13.08 cnf(11987,plain, % 13.01/13.08 (~P3(a2,f1(a2))+P5(a2,f4(a2))), % 13.01/13.08 inference(scs_inference,[],[11956,3])). % 13.01/13.08 cnf(12018,plain, % 13.01/13.08 (P5(a2,f1(a2))+P5(a2,f4(a2))), % 13.01/13.08 inference(scs_inference,[],[11987,1182])). % 13.01/13.08 cnf(12049,plain, % 13.01/13.08 (P4(a2,f4(a2))+P5(a2,f1(a2))), % 13.01/13.08 inference(scs_inference,[],[12018,4])). % 13.01/13.08 cnf(12080,plain, % 13.01/13.08 (~P5(f1(a2),x120801)+P4(a2,f4(a2))), % 13.01/13.08 inference(scs_inference,[],[12049,6])). % 13.01/13.08 cnf(12111,plain, % 13.01/13.08 (~P1(a2,f4(a2))+~P5(f1(a2),x121111)), % 13.01/13.08 inference(scs_inference,[],[12080,9])). % 13.01/13.08 cnf(12605,plain, % 13.01/13.08 (~P5(f1(a2),x126051)+P5(a2,f4(a2))), % 13.01/13.08 inference(scs_inference,[],[11956,1488])). % 13.01/13.08 cnf(12636,plain, % 13.01/13.08 (~P5(f4(a2),x126361)+~P5(f1(a2),x126362)), % 13.01/13.08 inference(scs_inference,[],[12605,6])). % 13.01/13.08 cnf(12667,plain, % 13.01/13.08 (P2(f4(a2),x126671)+~P5(f1(a2),x126672)), % 13.01/13.08 inference(scs_inference,[],[12636,688])). % 13.01/13.08 cnf(12698,plain, % 13.01/13.08 (P3(f4(a2),f1(f4(a2)))+~P5(f1(a2),x126981)), % 13.01/13.08 inference(scs_inference,[],[1147,12667,12])). % 13.01/13.08 cnf(12821,plain, % 13.01/13.08 (~P5(f4(a2),x128211)+~P2(a2,f1(a2))), % 13.01/13.08 inference(scs_inference,[],[11956,6])). % 13.01/13.08 cnf(12852,plain, % 13.01/13.08 (~P3(a2,f1(a2))+~P5(f4(a2),x128521)), % 13.01/13.08 inference(scs_inference,[],[12821,3])). % 13.01/13.08 cnf(13253,plain, % 13.01/13.08 (~P2(a2,f4(a2))+~P2(a2,f1(a2))), % 13.01/13.08 inference(scs_inference,[],[11956,8])). % 13.01/13.08 cnf(13284,plain, % 13.01/13.08 (~P3(a2,f1(a2))+~P2(a2,f4(a2))), % 13.01/13.08 inference(scs_inference,[],[13253,3])). % 13.01/13.08 cnf(13315,plain, % 13.01/13.08 (P5(a2,f1(a2))+~P2(a2,f4(a2))), % 13.01/13.08 inference(scs_inference,[],[13284,1182])). % 13.01/13.08 cnf(13346,plain, % 13.01/13.08 (~P5(f1(a2),x133461)+~P2(a2,f4(a2))), % 13.01/13.08 inference(scs_inference,[],[13315,6])). % 13.01/13.08 cnf(13377,plain, % 13.01/13.08 (~P3(a2,f4(a2))+~P5(f1(a2),x133771)), % 13.01/13.08 inference(scs_inference,[],[13346,3])). % 13.01/13.08 cnf(13531,plain, % 13.01/13.08 (P2(f1(a2),x135311)+P5(a2,f4(a2))), % 13.01/13.08 inference(scs_inference,[],[11956,1642])). % 13.01/13.08 cnf(13562,plain, % 13.01/13.08 (~P5(f4(a2),x135621)+P2(f1(a2),x135622)), % 13.01/13.08 inference(scs_inference,[],[13531,6])). % 13.01/13.08 cnf(13593,plain, % 13.01/13.08 (P2(f4(a2),x135931)+P2(f1(a2),x135932)), % 13.01/13.08 inference(scs_inference,[],[13562,688])). % 13.01/13.08 cnf(16015,plain, % 13.01/13.08 (P2(f4(a2),x160151)+~P2(a2,f1(a2))), % 13.01/13.08 inference(scs_inference,[],[688,12821])). % 13.01/13.08 cnf(16046,plain, % 13.01/13.08 (~P3(a2,f1(a2))+P2(f4(a2),x160461)), % 13.01/13.08 inference(scs_inference,[],[16015,3])). % 13.01/13.08 cnf(16077,plain, % 13.01/13.08 (P5(a2,f1(a2))+P2(f4(a2),x160771)), % 13.01/13.08 inference(scs_inference,[],[16046,1182])). % 13.01/13.08 cnf(16983,plain, % 13.01/13.08 (~P3(a2,f1(a2))+~P2(f4(a2),f1(f4(a2)))+P5(a2,a5)), % 13.01/13.08 inference(scs_inference,[],[1147,12852,7097])). % 13.01/13.08 cnf(17385,plain, % 13.01/13.08 (~P3(a2,f1(a2))+~P2(f4(a2),f1(f4(a2)))+P5(a5,a7)), % 13.01/13.08 inference(scs_inference,[],[1147,12852,7313])). % 13.01/13.08 cnf(17416,plain, % 13.01/13.08 (~P2(a2,f1(a2))+~P2(f4(a2),f1(f4(a2)))+P5(a5,a7)), % 13.01/13.08 inference(scs_inference,[],[17385,1148])). % 13.01/13.08 cnf(17447,plain, % 13.01/13.08 (~P5(f1(a2),x174471)+~P2(f4(a2),f1(f4(a2)))+P5(a5,a7)), % 13.01/13.08 inference(scs_inference,[],[17416,1488])). % 13.01/13.08 cnf(17478,plain, % 13.01/13.08 (~P3(f4(a2),f1(f4(a2)))+~P5(f1(a2),x174781)+P5(a5,a7)), % 13.01/13.08 inference(scs_inference,[],[17447,3])). % 13.01/13.08 cnf(17509,plain, % 13.01/13.08 (P2(f1(a2),x175091)+~P3(f4(a2),f1(f4(a2)))+P5(a5,a7)), % 13.01/13.08 inference(scs_inference,[],[17478,688])). % 13.01/13.08 cnf(17540,plain, % 13.01/13.08 (P3(f1(a2),f1(f1(a2)))+~P3(f4(a2),f1(f4(a2)))+P5(a5,a7)), % 13.01/13.08 inference(scs_inference,[],[1147,17509,12])). % 13.01/13.08 cnf(17571,plain, % 13.01/13.08 (P3(f1(a2),f1(f1(a2)))+P5(a5,a7)), % 13.01/13.08 inference(scs_inference,[],[17540,7808])). % 13.01/13.08 cnf(18364,plain, % 13.01/13.08 (~P3(a2,f1(a2))+~P2(a2,f1(a2))+P5(a2,a5)), % 13.01/13.08 inference(scs_inference,[],[16015,16983])). % 13.01/13.08 cnf(18395,plain, % 13.01/13.08 (~P2(a2,f1(a2))+P5(a2,a5)), % 13.01/13.08 inference(scs_inference,[],[18364,1148])). % 13.01/13.08 cnf(18426,plain, % 13.01/13.08 (~P3(a2,f1(a2))+P5(a2,a5)), % 13.01/13.08 inference(scs_inference,[],[18395,3])). % 13.01/13.08 cnf(18457,plain, % 13.01/13.08 (P5(a2,f1(a2))+P5(a2,a5)), % 13.01/13.08 inference(scs_inference,[],[18426,1182])). % 13.01/13.08 cnf(18488,plain, % 13.01/13.08 (~P5(f1(a2),x184881)+P5(a2,a5)), % 13.01/13.08 inference(scs_inference,[],[18457,6])). % 13.01/13.08 cnf(19353,plain, % 13.01/13.08 (~P2(a2,a5)+~P2(a2,f1(a2))), % 13.01/13.08 inference(scs_inference,[],[18395,8])). % 13.01/13.08 cnf(19384,plain, % 13.01/13.08 (~P3(a2,f1(a2))+~P2(a2,a5)), % 13.01/13.08 inference(scs_inference,[],[19353,3])). % 13.01/13.08 cnf(19415,plain, % 13.01/13.08 (P5(a2,f1(a2))+~P2(a2,a5)), % 13.01/13.08 inference(scs_inference,[],[19384,1182])). % 13.01/13.08 cnf(19446,plain, % 13.01/13.08 (~P5(f1(a2),x194461)+~P2(a2,a5)), % 13.01/13.08 inference(scs_inference,[],[19415,6])). % 13.01/13.08 cnf(19477,plain, % 13.01/13.08 (~P5(a5,x194771)+~P5(f1(a2),x194772)), % 13.01/13.08 inference(scs_inference,[],[19446,1488])). % 13.01/13.08 cnf(19508,plain, % 13.01/13.08 (P2(f1(a2),x195081)+~P5(a5,x195082)), % 13.01/13.08 inference(scs_inference,[],[19477,688])). % 13.01/13.08 cnf(19539,plain, % 13.01/13.08 (P3(f1(a2),f1(f1(a2)))+P2(f1(a2),x195391)), % 13.01/13.08 inference(scs_inference,[],[19508,17571])). % 13.01/13.08 cnf(19570,plain, % 13.01/13.08 (P2(f1(a2),f1(f1(a2)))+P2(f1(a2),x195701)), % 13.01/13.08 inference(scs_inference,[],[19539,3])). % 13.01/13.08 cnf(19571,plain, % 13.01/13.08 (P2(f1(a2),f1(f1(a2)))), % 13.01/13.08 inference(factoring_inference,[],[19570])). % 13.01/13.08 cnf(20467,plain, % 13.01/13.08 (P3(f1(a2),f1(f1(a2)))), % 13.01/13.08 inference(scs_inference,[],[19571,1147,12])). % 13.01/13.08 cnf(20475,plain, % 13.01/13.08 (P5(x204751,f4(x204751))+~P3(x204751,x204752)+P5(a2,a5)+P5(f1(a2),f6(f1(a2)))), % 13.01/13.08 inference(scs_inference,[],[20467,32])). % 13.01/13.08 cnf(20557,plain, % 13.01/13.08 (P5(a2,a5)+P5(f1(a2),f6(f1(a2)))), % 13.01/13.08 inference(scs_inference,[],[20467,18488,20475])). % 13.01/13.08 cnf(21016,plain, % 13.01/13.08 (P5(a2,a5)), % 13.01/13.08 inference(scs_inference,[],[18488,20557])). % 13.01/13.08 cnf(21017,plain, % 13.01/13.08 (~P5(a5,x210171)), % 13.01/13.08 inference(scs_inference,[],[21016,6])). % 13.01/13.08 cnf(21019,plain, % 13.01/13.08 (P3(a5,f1(a5))), % 13.01/13.08 inference(scs_inference,[],[21016,6,166])). % 13.01/13.08 cnf(21027,plain, % 13.01/13.08 (~P1(a2,a5)), % 13.01/13.08 inference(scs_inference,[],[21016,6,166,1611,4,8,42])). % 13.01/13.08 cnf(21042,plain, % 13.01/13.08 (~P3(a2,f1(a2))), % 13.01/13.08 inference(scs_inference,[],[21016,6,166,1611,4,8,42,73,17385,12667,688,16077,13593,16015,16046])). % 13.01/13.08 cnf(21046,plain, % 13.01/13.08 (P5(x210461,f6(x210461))+P5(x210462,f4(x210462))+P1(x210461,x210463)+~P3(x210462,x210464)+~P3(x210461,x210465)+P1(a2,x210461)), % 13.01/13.08 inference(scs_inference,[],[21017,23])). % 13.01/13.08 cnf(21050,plain, % 13.01/13.08 (~P2(f4(a2),f1(f4(a2)))+~P5(f1(a2),x210501)), % 13.01/13.08 inference(scs_inference,[],[21017,17447])). % 13.01/13.08 cnf(21051,plain, % 13.01/13.08 (~P5(f1(a2),x210511)+~P3(f4(a2),f1(f4(a2)))), % 13.01/13.08 inference(scs_inference,[],[21017,17478])). % 13.01/13.08 cnf(21077,plain, % 13.01/13.08 ($false), % 13.01/13.08 inference(scs_inference,[],[20467,1,21017,21019,21042,21027,1148,688,21046,12080,12111,12605,12698,13346,13377,21050,21051]), % 13.01/13.08 ['proof']). % 13.01/13.08 % SZS output end Proof % 13.01/13.08 % Total time :12.400000s %------------------------------------------------------------------------------