%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP127-1.004 : TPTP v8.2.0. Released v1.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/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 06:38:53 EDT 2024 % Result : Unsatisfiable 59.13s 59.54s % Output : CNFRefutation 59.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : GRP127-1.004 : TPTP v8.2.0. Released v1.2.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n018.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Jun 20 06:58:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.51/0.58 start to proof:theBenchmark % 59.06/59.53 %------------------------------------------- % 59.06/59.53 % File :CSE---1.7 % 59.06/59.53 % Problem :theBenchmark % 59.06/59.53 % Transform :cnf % 59.06/59.53 % Format :tptp:raw % 59.06/59.53 % Command :java -jar mcs_scs.jar %d %s % 59.06/59.53 % 59.06/59.53 % Result :Theorem 58.510000s % 59.06/59.53 % Output :CNFRefutation 58.510000s % 59.06/59.53 %------------------------------------------- % 59.06/59.54 %-------------------------------------------------------------------------- % 59.06/59.54 % File : GRP127-1.004 : TPTP v8.2.0. Released v1.2.0. % 59.06/59.54 % Domain : Group Theory (Quasigroups) % 59.06/59.54 % Problem : ((b.a).b).b) = a % 59.06/59.54 % Version : [Sla93] axioms. % 59.06/59.54 % English : Generate the multiplication table for the specified quasi- % 59.06/59.54 % group with 4 elements. % 59.06/59.54 % 59.06/59.54 % Refs : [Ben89] Bennett (1989), Quasigroup Identities and Mendelsohn D % 59.06/59.54 % : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 59.06/59.54 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 59.06/59.54 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 59.06/59.54 % Source : [Sla93] % 59.06/59.54 % Names : QG5 [Sla93] % 59.06/59.54 % : QG5 [FSB93] % 59.06/59.54 % : QG5 [SFS95] % 59.06/59.54 % : Bennett QG5 [TPTP] % 59.06/59.54 % 59.06/59.54 % Status : Unsatisfiable % 59.06/59.54 % Rating : 0.00 v2.1.0 % 59.06/59.54 % Syntax : Number of clauses : 22 ( 17 unt; 1 nHn; 21 RR) % 59.06/59.54 % Number of literals : 35 ( 0 equ; 22 neg) % 59.06/59.54 % Maximal clause size : 6 ( 1 avg) % 59.06/59.54 % Maximal term depth : 1 ( 1 avg) % 59.06/59.54 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty) % 59.06/59.54 % Number of functors : 4 ( 4 usr; 4 con; 0-0 aty) % 59.06/59.54 % Number of variables : 19 ( 0 sgn) % 59.06/59.54 % SPC : CNF_UNS_EPR_NEQ_NHN % 59.06/59.54 % 59.06/59.54 % Comments : [SFS93]'s axiomatization has been modified for this. % 59.06/59.54 % : Substitution axioms are not needed, as any positive equality % 59.06/59.54 % literals should resolve on negative ones directly. % 59.06/59.54 % : This problem is extensively investigated in [Ben89]. % 59.06/59.54 % : tptp2X: -f tptp -s4 GRP127-1.g % 59.06/59.54 %-------------------------------------------------------------------------- % 59.06/59.54 cnf(element_1,axiom, % 59.06/59.54 group_element(e_1) ). % 59.06/59.54 % 59.06/59.54 cnf(element_2,axiom, % 59.06/59.54 group_element(e_2) ). % 59.06/59.54 % 59.06/59.54 cnf(element_3,axiom, % 59.06/59.54 group_element(e_3) ). % 59.06/59.54 % 59.06/59.54 cnf(element_4,axiom, % 59.06/59.54 group_element(e_4) ). % 59.06/59.54 % 59.06/59.54 cnf(e_1_is_not_e_2,axiom, % 59.06/59.54 ~ equalish(e_1,e_2) ). % 59.06/59.54 % 59.06/59.54 cnf(e_1_is_not_e_3,axiom, % 59.06/59.54 ~ equalish(e_1,e_3) ). % 59.06/59.54 % 59.06/59.54 cnf(e_1_is_not_e_4,axiom, % 59.06/59.54 ~ equalish(e_1,e_4) ). % 59.06/59.54 % 59.06/59.54 cnf(e_2_is_not_e_1,axiom, % 59.06/59.54 ~ equalish(e_2,e_1) ). % 59.06/59.54 % 59.06/59.54 cnf(e_2_is_not_e_3,axiom, % 59.06/59.54 ~ equalish(e_2,e_3) ). % 59.06/59.54 % 59.06/59.54 cnf(e_2_is_not_e_4,axiom, % 59.06/59.54 ~ equalish(e_2,e_4) ). % 59.06/59.54 % 59.06/59.54 cnf(e_3_is_not_e_1,axiom, % 59.06/59.54 ~ equalish(e_3,e_1) ). % 59.06/59.54 % 59.06/59.54 cnf(e_3_is_not_e_2,axiom, % 59.06/59.54 ~ equalish(e_3,e_2) ). % 59.06/59.54 % 59.06/59.54 cnf(e_3_is_not_e_4,axiom, % 59.06/59.54 ~ equalish(e_3,e_4) ). % 59.06/59.54 % 59.06/59.54 cnf(e_4_is_not_e_1,axiom, % 59.06/59.54 ~ equalish(e_4,e_1) ). % 59.06/59.54 % 59.06/59.54 cnf(e_4_is_not_e_2,axiom, % 59.13/59.54 ~ equalish(e_4,e_2) ). % 59.13/59.54 % 59.13/59.54 cnf(e_4_is_not_e_3,axiom, % 59.13/59.54 ~ equalish(e_4,e_3) ). % 59.13/59.54 % 59.13/59.54 cnf(product_total_function1,axiom, % 59.13/59.54 ( ~ group_element(X) % 59.13/59.54 | ~ group_element(Y) % 59.13/59.54 | product(X,Y,e_1) % 59.13/59.54 | product(X,Y,e_2) % 59.13/59.54 | product(X,Y,e_3) % 59.13/59.54 | product(X,Y,e_4) ) ). % 59.13/59.54 % 59.13/59.54 cnf(product_total_function2,axiom, % 59.13/59.54 ( ~ product(X,Y,W) % 59.13/59.54 | ~ product(X,Y,Z) % 59.13/59.54 | equalish(W,Z) ) ). % 59.13/59.54 % 59.13/59.54 cnf(product_right_cancellation,axiom, % 59.13/59.54 ( ~ product(X,W,Y) % 59.13/59.54 | ~ product(X,Z,Y) % 59.13/59.54 | equalish(W,Z) ) ). % 59.13/59.54 % 59.13/59.54 cnf(product_left_cancellation,axiom, % 59.13/59.54 ( ~ product(W,Y,X) % 59.13/59.54 | ~ product(Z,Y,X) % 59.13/59.54 | equalish(W,Z) ) ). % 59.13/59.54 % 59.13/59.54 cnf(product_idempotence,axiom, % 59.13/59.54 product(X,X,X) ). % 59.13/59.54 % 59.13/59.54 cnf(qg3,negated_conjecture, % 59.13/59.54 ( ~ product(Y,X,Z1) % 59.13/59.54 | ~ product(Z1,Y,Z2) % 59.13/59.54 | product(Z2,Y,X) ) ). % 59.13/59.54 % 59.13/59.54 %-------------------------------------------------------------------------- % 59.13/59.54 %------------------------------------------- % 59.13/59.54 % Proof found % 59.13/59.54 % SZS status Theorem for theBenchmark % 59.13/59.54 % SZS output start Proof % 59.13/59.54 %ClaNum:22(EqnAxiom:0) % 59.13/59.54 %VarNum:46(SingletonVarNum:19) % 59.13/59.54 %MaxLitNum:6 % 59.13/59.54 %MaxfuncDepth:0 % 59.13/59.54 %SharedTerms:20 % 59.13/59.54 %goalClause: 21 % 59.13/59.54 [1]P1(a1) % 59.13/59.54 [2]P1(a2) % 59.13/59.54 [3]P1(a3) % 59.13/59.54 [4]P1(a4) % 59.13/59.54 [6]~P2(a1,a2) % 59.13/59.54 [7]~P2(a1,a3) % 59.13/59.54 [8]~P2(a1,a4) % 59.13/59.54 [9]~P2(a2,a1) % 59.13/59.54 [10]~P2(a2,a3) % 59.13/59.54 [11]~P2(a2,a4) % 59.13/59.54 [12]~P2(a3,a1) % 59.13/59.54 [13]~P2(a3,a2) % 59.13/59.54 [14]~P2(a3,a4) % 59.13/59.54 [15]~P2(a4,a1) % 59.13/59.54 [16]~P2(a4,a2) % 59.13/59.54 [17]~P2(a4,a3) % 59.13/59.54 [5]P3(x51,x51,x51) % 59.13/59.54 [18]~P3(x183,x184,x181)+P2(x181,x182)+~P3(x183,x184,x182) % 59.13/59.54 [19]~P3(x193,x191,x194)+P2(x191,x192)+~P3(x193,x192,x194) % 59.13/59.54 [20]~P3(x201,x203,x204)+P2(x201,x202)+~P3(x202,x203,x204) % 59.13/59.54 [21]~P3(x212,x213,x214)+P3(x211,x212,x213)+~P3(x214,x212,x211) % 59.13/59.54 [22]~P1(x222)+~P1(x221)+P3(x221,x222,a2)+P3(x221,x222,a3)+P3(x221,x222,a4)+P3(x221,x222,a1) % 59.13/59.54 %EqnAxiom % 59.13/59.54 % 59.13/59.54 %------------------------------------------- % 59.17/59.58 cnf(86,plain, % 59.17/59.58 (~P3(a1,a2,a1)), % 59.17/59.58 inference(scs_inference,[],[5,6,18,21])). % 59.17/59.58 cnf(148,plain, % 59.17/59.58 (~P3(a1,a4,a1)), % 59.17/59.58 inference(scs_inference,[],[8,5,18,21])). % 59.17/59.58 cnf(179,plain, % 59.17/59.58 (~P3(a2,a1,a2)), % 59.17/59.58 inference(scs_inference,[],[9,5,18,21])). % 59.17/59.58 cnf(182,plain, % 59.17/59.58 (P3(a2,a1,a4)+P3(a2,a1,a1)+P3(a2,a1,a3)), % 59.17/59.58 inference(scs_inference,[],[1,179,5,2,19,22])). % 59.17/59.58 cnf(271,plain, % 59.17/59.58 (~P3(a3,a2,a3)), % 59.17/59.58 inference(scs_inference,[],[10,5,18,21])). % 59.17/59.58 cnf(363,plain, % 59.17/59.58 (~P3(a1,a3,a1)), % 59.17/59.58 inference(scs_inference,[],[12,5,18,21])). % 59.17/59.58 cnf(501,plain, % 59.17/59.58 (~P3(a3,a4,a3)), % 59.17/59.58 inference(scs_inference,[],[14,5,18,21])). % 59.17/59.58 cnf(547,plain, % 59.17/59.58 (~P3(a4,a1,a4)), % 59.17/59.58 inference(scs_inference,[],[15,5,18,21])). % 59.17/59.58 cnf(593,plain, % 59.17/59.58 (~P3(a2,a4,a2)), % 59.17/59.58 inference(scs_inference,[],[16,5,18,21])). % 59.17/59.58 cnf(685,plain, % 59.17/59.58 (~P3(a4,a3,a4)), % 59.17/59.58 inference(scs_inference,[],[17,5,18,21])). % 59.17/59.58 cnf(1187,plain, % 59.17/59.58 (~P3(x11871,a1,a3)+~P3(a1,a3,x11871)), % 59.17/59.58 inference(scs_inference,[],[7,5,19,21])). % 59.17/59.58 cnf(1324,plain, % 59.17/59.58 (P3(a2,a1,a4)+P3(a2,a1,a1)+~P3(a1,a3,a2)), % 59.17/59.58 inference(scs_inference,[],[1187,182])). % 59.17/59.58 cnf(1552,plain, % 59.17/59.58 (P3(a1,a3,a2)+P3(a1,a3,a3)+~P3(a4,a1,a3)), % 59.17/59.58 inference(scs_inference,[],[363,3,1,1187,22])). % 59.17/59.58 cnf(1780,plain, % 59.17/59.58 (~P3(x17801,a1,a2)+~P3(a1,a2,x17801)), % 59.17/59.58 inference(scs_inference,[],[6,5,19,21])). % 59.17/59.58 cnf(1826,plain, % 59.17/59.58 (P3(a1,a2,a2)+P3(a1,a2,a4)+~P3(a3,a1,a2)), % 59.17/59.58 inference(scs_inference,[],[86,2,1,1780,22])). % 59.17/59.58 cnf(2236,plain, % 59.17/59.58 (~P3(x22361,a3,a1)+~P3(a3,a1,x22361)), % 59.17/59.58 inference(scs_inference,[],[7,5,19,21])). % 59.17/59.58 cnf(2556,plain, % 59.17/59.58 (~P3(x25561,a1,a4)+~P3(a1,a4,x25561)), % 59.17/59.58 inference(scs_inference,[],[8,5,19,21])). % 59.17/59.58 cnf(2602,plain, % 59.17/59.58 (P3(a1,a4,a4)+P3(a1,a4,a3)+~P3(a2,a1,a4)), % 59.17/59.58 inference(scs_inference,[],[148,4,1,2556,22])). % 59.17/59.58 cnf(2665,plain, % 59.17/59.58 (P3(a4,a3,a1)+P3(a4,a3,a2)+P3(a4,a3,a3)), % 59.17/59.58 inference(scs_inference,[],[685,5,4,3,18,22])). % 59.17/59.58 cnf(2668,plain, % 59.17/59.58 (P3(a4,a1,a1)+P3(a4,a1,a2)+P3(a4,a1,a3)), % 59.17/59.58 inference(scs_inference,[],[547,5,4,1,19,22])). % 59.17/59.58 cnf(2739,plain, % 59.17/59.58 (P3(a4,a3,a2)+P3(a4,a3,a3)+~P3(a3,a1,a4)), % 59.17/59.58 inference(scs_inference,[],[2665,2236])). % 59.17/59.58 cnf(2968,plain, % 59.17/59.58 (P3(a2,a1,a3)+P3(a2,a1,a1)+~P3(a1,a4,a2)), % 59.17/59.58 inference(scs_inference,[],[2556,182])). % 59.17/59.58 cnf(3287,plain, % 59.17/59.58 (P3(a1,a4,a4)+P3(a1,a4,a2)+~P3(a3,a1,a4)), % 59.17/59.58 inference(scs_inference,[],[148,4,1,2556,22])). % 59.17/59.58 cnf(4747,plain, % 59.17/59.58 (~P3(x47471,a4,a1)+~P3(a4,a1,x47471)), % 59.17/59.58 inference(scs_inference,[],[15,5,19,21])). % 59.17/59.58 cnf(4975,plain, % 59.17/59.58 (P3(a3,a4,a4)+P3(a3,a4,a2)+~P3(a4,a1,a3)), % 59.17/59.58 inference(scs_inference,[],[501,4,3,4747,22])). % 59.17/59.58 cnf(5111,plain, % 59.17/59.58 (~P3(x51111,a2,a4)+~P3(a2,a4,x51111)), % 59.17/59.58 inference(scs_inference,[],[16,5,19,21])). % 59.17/59.58 cnf(5430,plain, % 59.17/59.58 (~P3(a3,a1,a2)+P3(a1,a2,a2)+~P3(a2,a4,a1)), % 59.17/59.58 inference(scs_inference,[],[5111,1826])). % 59.17/59.58 cnf(5521,plain, % 59.17/59.58 (P3(a1,a2,a3)+P3(a1,a2,a2)+~P3(a2,a4,a1)), % 59.17/59.58 inference(scs_inference,[],[86,2,1,5111,22])). % 59.17/59.58 cnf(5703,plain, % 59.17/59.58 (~P3(x57031,a4,a3)+~P3(a4,a3,x57031)), % 59.17/59.58 inference(scs_inference,[],[17,5,19,21])). % 59.17/59.58 cnf(5749,plain, % 59.17/59.58 (P3(a4,a3,a3)+P3(a4,a3,a2)+~P3(a1,a4,a3)), % 59.17/59.58 inference(scs_inference,[],[685,3,4,5703,22])). % 59.17/59.58 cnf(6204,plain, % 59.17/59.58 (P3(a1,a4,a4)+P3(a1,a4,a2)+~P3(a4,a3,a1)), % 59.17/59.58 inference(scs_inference,[],[148,4,1,5703,22])). % 59.17/59.58 cnf(6340,plain, % 59.17/59.58 (~P3(x63401,a3,a2)+~P3(a3,a2,x63401)), % 59.17/59.58 inference(scs_inference,[],[10,5,19,21])). % 59.17/59.58 cnf(6568,plain, % 59.17/59.58 (P3(a3,a2,a4)+P3(a3,a2,a2)+~P3(a1,a3,a2)), % 59.17/59.58 inference(scs_inference,[],[271,2,3,6340,22])). % 59.17/59.58 cnf(20112,plain, % 59.17/59.58 (~P3(a2,a4,a3)+~P3(a1,a4,a2)+P3(a2,a1,a1)), % 59.17/59.58 inference(scs_inference,[],[8,19,2968])). % 59.17/59.58 cnf(30539,plain, % 59.17/59.58 (~P3(a1,a4,a3)+~P3(a2,a4,a1)+P3(a1,a2,a2)), % 59.17/59.58 inference(scs_inference,[],[11,19,5521])). % 59.17/59.58 cnf(31317,plain, % 59.17/59.58 (P3(x313171,x313171,x313171)), % 59.17/59.58 inference(rename_variables,[],[5])). % 59.17/59.58 cnf(31319,plain, % 59.17/59.58 (~P3(a4,a3,a3)), % 59.17/59.58 inference(scs_inference,[],[14,5,31317,18,20])). % 59.17/59.58 cnf(31325,plain, % 59.17/59.58 (~P3(a3,a1,a4)+~P3(a3,a2,a4)), % 59.17/59.58 inference(scs_inference,[],[501,14,5,31317,18,20,2739,21,6340])). % 59.17/59.58 cnf(31328,plain, % 59.17/59.58 (P3(a4,a3,a2)+P3(a4,a3,a1)), % 59.17/59.58 inference(scs_inference,[],[31319,2665])). % 59.17/59.58 cnf(31329,plain, % 59.17/59.58 (~P3(a1,a4,a3)+P3(a4,a3,a2)), % 59.17/59.58 inference(scs_inference,[],[31319,5749])). % 59.17/59.58 cnf(31341,plain, % 59.17/59.58 (P3(x313411,x313411,x313411)), % 59.17/59.58 inference(rename_variables,[],[5])). % 59.17/59.58 cnf(31343,plain, % 59.17/59.58 (~P3(a4,a1,a1)), % 59.17/59.58 inference(scs_inference,[],[8,5,31341,18,20])). % 59.17/59.58 cnf(31348,plain, % 59.17/59.58 (P3(a4,a1,a3)+P3(a4,a1,a2)), % 59.17/59.58 inference(scs_inference,[],[31343,2668])). % 59.17/59.58 cnf(31354,plain, % 59.17/59.58 (~P3(a3,a2,a2)), % 59.17/59.58 inference(scs_inference,[],[10,5,20])). % 59.17/59.58 cnf(31364,plain, % 59.17/59.58 (~P3(a1,a3,a2)+P3(a3,a2,a4)), % 59.17/59.58 inference(scs_inference,[],[31354,6568])). % 59.17/59.58 cnf(31399,plain, % 59.17/59.58 (P3(x313991,x313991,x313991)), % 59.17/59.58 inference(rename_variables,[],[5])). % 59.17/59.58 cnf(31401,plain, % 59.17/59.58 (~P3(a1,a3,a3)), % 59.17/59.58 inference(scs_inference,[],[12,5,31399,18,20])). % 59.17/59.58 cnf(31408,plain, % 59.17/59.58 (~P3(a4,a1,a3)+P3(a1,a3,a2)), % 59.17/59.58 inference(scs_inference,[],[31401,1552])). % 59.17/59.58 cnf(31423,plain, % 59.17/59.58 (~P3(a1,a3,a2)+~P3(a3,a1,a4)), % 59.17/59.58 inference(scs_inference,[],[31325,31364])). % 59.17/59.58 cnf(31443,plain, % 59.17/59.58 (P3(x314431,x314431,x314431)), % 59.17/59.58 inference(rename_variables,[],[5])). % 59.17/59.58 cnf(31445,plain, % 59.17/59.58 (~P3(a1,a2,a2)), % 59.17/59.58 inference(scs_inference,[],[9,5,31443,18,20])). % 59.17/59.58 cnf(31448,plain, % 59.17/59.58 (~P3(a2,a4,a1)+P3(a1,a2,a3)), % 59.17/59.58 inference(scs_inference,[],[9,5,31443,18,20,5521])). % 59.17/59.58 cnf(31454,plain, % 59.17/59.58 (~P3(a2,a4,a1)+~P3(a3,a1,a2)), % 59.17/59.58 inference(scs_inference,[],[31445,5430])). % 59.17/59.58 cnf(31460,plain, % 59.17/59.58 (~P3(a2,a4,a1)+~P3(a1,a4,a3)), % 59.17/59.58 inference(scs_inference,[],[31445,30539])). % 59.17/59.58 cnf(31466,plain, % 59.17/59.58 (P3(x314661,x314661,x314661)), % 59.17/59.58 inference(rename_variables,[],[5])). % 59.17/59.58 cnf(31468,plain, % 59.17/59.58 (~P3(a3,a4,a4)), % 59.17/59.58 inference(scs_inference,[],[17,5,31466,18,20])). % 59.17/59.58 cnf(31473,plain, % 59.17/59.58 (~P3(a4,a1,a3)+P3(a3,a4,a2)), % 59.17/59.58 inference(scs_inference,[],[31468,4975])). % 59.17/59.58 cnf(31480,plain, % 59.17/59.58 (P3(a4,a3,a1)+~P3(a2,a4,a3)), % 59.17/59.58 inference(scs_inference,[],[31328,5703])). % 59.17/59.58 cnf(31483,plain, % 59.17/59.58 (P3(x314831,x314831,x314831)), % 59.17/59.58 inference(rename_variables,[],[5])). % 59.17/59.58 cnf(31485,plain, % 59.17/59.58 (~P3(a1,a4,a4)), % 59.17/59.58 inference(scs_inference,[],[15,5,31483,18,20])). % 59.17/59.58 cnf(31489,plain, % 59.17/59.58 (~P3(a4,a3,a1)+P3(a1,a4,a2)), % 59.17/59.58 inference(scs_inference,[],[15,5,31483,18,20,3287,6204])). % 59.17/59.58 cnf(31491,plain, % 59.17/59.58 (~P3(a2,a1,a4)+P3(a1,a4,a3)), % 59.17/59.58 inference(scs_inference,[],[31485,2602])). % 59.17/59.58 cnf(31501,plain, % 59.17/59.58 (P3(x315011,x315011,x315011)), % 59.17/59.58 inference(rename_variables,[],[5])). % 59.17/59.58 cnf(31520,plain, % 59.17/59.58 (P3(a2,a1,a1)+P3(a2,a4,a3)), % 59.17/59.58 inference(scs_inference,[],[16,5,31501,4,593,2,18,20,22,4747,31348,31408,31423,31448,31454,31460,31473,31491,6340,1324])). % 59.17/59.58 cnf(31544,plain, % 59.17/59.58 (P3(x315441,x315441,x315441)), % 59.17/59.58 inference(rename_variables,[],[5])). % 59.17/59.58 cnf(31546,plain, % 59.17/59.58 (~P3(a2,a1,a1)), % 59.17/59.58 inference(scs_inference,[],[5,31544,6,18,20])). % 59.17/59.58 cnf(31549,plain, % 59.17/59.58 (P3(a2,a4,a3)), % 59.17/59.58 inference(scs_inference,[],[5,31544,6,18,20,31520])). % 59.17/59.58 cnf(31571,plain, % 59.17/59.58 (~P3(a1,a4,a2)), % 59.17/59.58 inference(scs_inference,[],[31546,31549,20112])). % 59.17/59.58 cnf(31579,plain, % 59.17/59.58 (P3(a4,a3,a1)), % 59.17/59.58 inference(scs_inference,[],[31549,31480])). % 59.17/59.58 cnf(31631,plain, % 59.17/59.58 ($false), % 59.17/59.58 inference(scs_inference,[],[31549,31571,31579,5703,31329,31489]), % 59.17/59.58 ['proof']). % 59.17/59.60 % SZS output end Proof % 59.17/59.60 % Total time :58.510000s %------------------------------------------------------------------------------