%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP124-7.004 : TPTP v8.2.0. Released v1.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n020.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:50 EDT 2024 % Result : Unsatisfiable 59.60s 59.69s % Output : CNFRefutation 59.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP124-7.004 : TPTP v8.2.0. Released v1.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n020.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Jun 20 10:23:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.51/0.56 start to proof:theBenchmark % 59.60/59.68 %------------------------------------------- % 59.60/59.68 % File :CSE---1.7 % 59.60/59.68 % Problem :theBenchmark % 59.60/59.68 % Transform :cnf % 59.60/59.68 % Format :tptp:raw % 59.60/59.68 % Command :java -jar mcs_scs.jar %d %s % 59.60/59.68 % 59.60/59.68 % Result :Theorem 59.080000s % 59.60/59.68 % Output :CNFRefutation 59.080000s % 59.60/59.68 %------------------------------------------- % 59.60/59.69 %-------------------------------------------------------------------------- % 59.60/59.69 % File : GRP124-7.004 : TPTP v8.2.0. Released v1.2.0. % 59.60/59.69 % Domain : Group Theory (Quasigroups) % 59.60/59.69 % Problem : (3,1,2) conjugate orthogonality % 59.60/59.69 % Version : [Sla93] axioms : Augmented. % 59.60/59.69 % Theorem formulation : Uses a second group. % 59.60/59.69 % English : If ab=xy and a*b = x*y then a=x and b=y, where c*a=b iff ab=c. % 59.60/59.69 % Generate the multiplication table for the specified quasi- % 59.60/59.69 % group with 4 elements. % 59.60/59.69 % 59.60/59.69 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 59.60/59.69 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 59.60/59.69 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 59.60/59.69 % Source : [TPTP] % 59.60/59.69 % Names : % 59.60/59.69 % 59.60/59.69 % Status : Unsatisfiable % 59.60/59.69 % Rating : 0.00 v2.1.0 % 59.60/59.69 % Syntax : Number of clauses : 37 ( 27 unt; 2 nHn; 35 RR) % 59.60/59.69 % Number of literals : 63 ( 0 equ; 33 neg) % 59.60/59.69 % Maximal clause size : 6 ( 1 avg) % 59.60/59.69 % Maximal term depth : 1 ( 1 avg) % 59.60/59.69 % Number of predicates : 7 ( 7 usr; 0 prp; 1-3 aty) % 59.60/59.69 % Number of functors : 4 ( 4 usr; 4 con; 0-0 aty) % 59.60/59.69 % Number of variables : 37 ( 0 sgn) % 59.60/59.69 % SPC : CNF_UNS_EPR_NEQ_NHN % 59.60/59.69 % 59.60/59.69 % Comments : [SFS93]'s axiomatization has been modified for this. % 59.60/59.69 % : Substitution axioms are not needed, as any positive equality % 59.60/59.69 % literals should resolve on negative ones directly. % 59.60/59.69 % : Version 7 has simple isomorphism avoidance (as mentioned in % 59.60/59.69 % [FSB93]) % 59.60/59.69 % : tptp2X: -f tptp -s4 GRP124-7.g % 59.60/59.69 %-------------------------------------------------------------------------- % 59.60/59.69 cnf(e_1_then_e_2,axiom, % 59.60/59.69 next(e_1,e_2) ). % 59.60/59.69 % 59.60/59.69 cnf(e_2_then_e_3,axiom, % 59.60/59.69 next(e_2,e_3) ). % 59.60/59.69 % 59.60/59.69 cnf(e_3_then_e_4,axiom, % 59.60/59.69 next(e_3,e_4) ). % 59.60/59.69 % 59.60/59.69 cnf(e_2_greater_e_1,axiom, % 59.60/59.69 greater(e_2,e_1) ). % 59.60/59.69 % 59.60/59.69 cnf(e_3_greater_e_1,axiom, % 59.60/59.69 greater(e_3,e_1) ). % 59.60/59.69 % 59.60/59.69 cnf(e_4_greater_e_1,axiom, % 59.60/59.69 greater(e_4,e_1) ). % 59.60/59.69 % 59.60/59.69 cnf(e_3_greater_e_2,axiom, % 59.60/59.69 greater(e_3,e_2) ). % 59.60/59.69 % 59.60/59.69 cnf(e_4_greater_e_2,axiom, % 59.60/59.69 greater(e_4,e_2) ). % 59.60/59.69 % 59.60/59.69 cnf(e_4_greater_e_3,axiom, % 59.60/59.69 greater(e_4,e_3) ). % 59.60/59.69 % 59.60/59.69 cnf(no_redundancy,axiom, % 59.60/59.69 ( ~ product(X,e_1,Y) % 59.60/59.69 | ~ next(X,X1) % 59.60/59.69 | ~ greater(Y,X1) ) ). % 59.60/59.69 % 59.60/59.69 cnf(element_1,axiom, % 59.60/59.69 group_element(e_1) ). % 59.60/59.69 % 59.60/59.69 cnf(element_2,axiom, % 59.60/59.69 group_element(e_2) ). % 59.60/59.69 % 59.60/59.69 cnf(element_3,axiom, % 59.60/59.69 group_element(e_3) ). % 59.60/59.69 % 59.60/59.69 cnf(element_4,axiom, % 59.60/59.69 group_element(e_4) ). % 59.60/59.69 % 59.60/59.69 cnf(e_1_is_not_e_2,axiom, % 59.60/59.69 ~ equalish(e_1,e_2) ). % 59.60/59.69 % 59.60/59.69 cnf(e_1_is_not_e_3,axiom, % 59.60/59.69 ~ equalish(e_1,e_3) ). % 59.60/59.69 % 59.60/59.69 cnf(e_1_is_not_e_4,axiom, % 59.60/59.69 ~ equalish(e_1,e_4) ). % 59.60/59.69 % 59.60/59.69 cnf(e_2_is_not_e_1,axiom, % 59.60/59.69 ~ equalish(e_2,e_1) ). % 59.60/59.69 % 59.60/59.69 cnf(e_2_is_not_e_3,axiom, % 59.60/59.69 ~ equalish(e_2,e_3) ). % 59.60/59.69 % 59.60/59.69 cnf(e_2_is_not_e_4,axiom, % 59.60/59.69 ~ equalish(e_2,e_4) ). % 59.60/59.69 % 59.60/59.69 cnf(e_3_is_not_e_1,axiom, % 59.60/59.69 ~ equalish(e_3,e_1) ). % 59.60/59.69 % 59.60/59.69 cnf(e_3_is_not_e_2,axiom, % 59.60/59.69 ~ equalish(e_3,e_2) ). % 59.60/59.69 % 59.60/59.69 cnf(e_3_is_not_e_4,axiom, % 59.60/59.69 ~ equalish(e_3,e_4) ). % 59.60/59.69 % 59.60/59.69 cnf(e_4_is_not_e_1,axiom, % 59.60/59.69 ~ equalish(e_4,e_1) ). % 59.60/59.69 % 59.60/59.69 cnf(e_4_is_not_e_2,axiom, % 59.60/59.69 ~ equalish(e_4,e_2) ). % 59.60/59.69 % 59.60/59.69 cnf(e_4_is_not_e_3,axiom, % 59.60/59.69 ~ equalish(e_4,e_3) ). % 59.60/59.69 % 59.60/59.69 cnf(product1_total_function1,axiom, % 59.60/59.69 ( ~ group_element(X) % 59.60/59.69 | ~ group_element(Y) % 59.60/59.69 | product1(X,Y,e_1) % 59.60/59.69 | product1(X,Y,e_2) % 59.60/59.69 | product1(X,Y,e_3) % 59.60/59.69 | product1(X,Y,e_4) ) ). % 59.60/59.69 % 59.60/59.69 cnf(product1_total_function2,axiom, % 59.60/59.69 ( ~ product1(X,Y,W) % 59.60/59.69 | ~ product1(X,Y,Z) % 59.60/59.69 | equalish(W,Z) ) ). % 59.60/59.69 % 59.60/59.69 cnf(product1_right_cancellation,axiom, % 59.60/59.69 ( ~ product1(X,W,Y) % 59.60/59.69 | ~ product1(X,Z,Y) % 59.60/59.69 | equalish(W,Z) ) ). % 59.60/59.69 % 59.60/59.69 cnf(product1_left_cancellation,axiom, % 59.60/59.69 ( ~ product1(W,Y,X) % 59.60/59.69 | ~ product1(Z,Y,X) % 59.60/59.69 | equalish(W,Z) ) ). % 59.60/59.69 % 59.60/59.69 cnf(product1_idempotence,axiom, % 59.60/59.69 product1(X,X,X) ). % 59.60/59.69 % 59.60/59.69 cnf(product2_total_function1,axiom, % 59.60/59.69 ( ~ group_element(X) % 59.60/59.69 | ~ group_element(Y) % 59.60/59.69 | product2(X,Y,e_1) % 59.60/59.69 | product2(X,Y,e_2) % 59.60/59.69 | product2(X,Y,e_3) % 59.60/59.69 | product2(X,Y,e_4) ) ). % 59.60/59.69 % 59.60/59.69 cnf(product2_total_function2,axiom, % 59.60/59.69 ( ~ product2(X,Y,W) % 59.60/59.69 | ~ product2(X,Y,Z) % 59.60/59.69 | equalish(W,Z) ) ). % 59.60/59.69 % 59.60/59.69 cnf(product2_right_cancellation,axiom, % 59.60/59.69 ( ~ product2(X,W,Y) % 59.60/59.69 | ~ product2(X,Z,Y) % 59.60/59.69 | equalish(W,Z) ) ). % 59.60/59.69 % 59.60/59.69 cnf(product2_left_cancellation,axiom, % 59.60/59.69 ( ~ product2(W,Y,X) % 59.60/59.69 | ~ product2(Z,Y,X) % 59.60/59.69 | equalish(W,Z) ) ). % 59.60/59.69 % 59.60/59.69 cnf(product2_idempotence,axiom, % 59.60/59.69 product2(X,X,X) ). % 59.60/59.69 % 59.60/59.69 cnf(qg2a,negated_conjecture, % 59.60/59.69 ( ~ product1(X,Y,Z1) % 59.60/59.69 | ~ product1(Z1,X,Z2) % 59.60/59.69 | product2(Z2,Y,X) ) ). % 59.60/59.69 % 59.60/59.69 %-------------------------------------------------------------------------- % 59.60/59.69 %------------------------------------------- % 59.60/59.69 % Proof found % 59.60/59.69 % SZS status Theorem for theBenchmark % 59.60/59.69 % SZS output start Proof % 59.60/59.69 %ClaNum:37(EqnAxiom:0) % 59.60/59.69 %VarNum:89(SingletonVarNum:37) % 59.60/59.69 %MaxLitNum:6 % 59.60/59.69 %MaxfuncDepth:0 % 59.60/59.69 %SharedTerms:29 % 59.60/59.69 %goalClause: 35 % 59.60/59.69 [1]P1(a1) % 59.60/59.69 [2]P1(a2) % 59.60/59.69 [3]P1(a3) % 59.60/59.69 [4]P1(a4) % 59.60/59.70 [5]P4(a1,a2) % 59.60/59.70 [6]P4(a2,a3) % 59.60/59.70 [7]P4(a3,a4) % 59.60/59.70 [8]P2(a2,a1) % 59.60/59.70 [9]P2(a3,a1) % 59.60/59.70 [10]P2(a3,a2) % 59.60/59.70 [11]P2(a4,a1) % 59.60/59.70 [12]P2(a4,a2) % 59.60/59.70 [13]P2(a4,a3) % 59.60/59.70 [16]~P3(a1,a2) % 59.60/59.70 [17]~P3(a1,a3) % 59.60/59.70 [18]~P3(a1,a4) % 59.60/59.70 [19]~P3(a2,a1) % 59.60/59.70 [20]~P3(a2,a3) % 59.60/59.70 [21]~P3(a2,a4) % 59.60/59.70 [22]~P3(a3,a1) % 59.60/59.70 [23]~P3(a3,a2) % 59.60/59.70 [24]~P3(a3,a4) % 59.60/59.70 [25]~P3(a4,a1) % 59.60/59.70 [26]~P3(a4,a2) % 59.60/59.70 [27]~P3(a4,a3) % 59.60/59.70 [14]P5(x141,x141,x141) % 59.60/59.70 [15]P7(x151,x151,x151) % 59.60/59.70 [28]~P4(x281,x282)+~P2(x283,x282)+~P6(x281,a1,x283) % 59.60/59.70 [29]~P5(x293,x294,x291)+P3(x291,x292)+~P5(x293,x294,x292) % 59.60/59.70 [30]~P7(x303,x304,x301)+P3(x301,x302)+~P7(x303,x304,x302) % 59.60/59.70 [31]~P5(x313,x311,x314)+P3(x311,x312)+~P5(x313,x312,x314) % 59.60/59.70 [32]~P7(x323,x321,x324)+P3(x321,x322)+~P7(x323,x322,x324) % 59.60/59.70 [33]~P5(x331,x333,x334)+P3(x331,x332)+~P5(x332,x333,x334) % 59.60/59.70 [34]~P7(x341,x343,x344)+P3(x341,x342)+~P7(x342,x343,x344) % 59.60/59.70 [35]~P5(x353,x352,x354)+P7(x351,x352,x353)+~P5(x354,x353,x351) % 59.60/59.70 [36]~P1(x362)+~P1(x361)+P5(x361,x362,a2)+P5(x361,x362,a3)+P5(x361,x362,a4)+P5(x361,x362,a1) % 59.60/59.70 [37]~P1(x372)+~P1(x371)+P7(x371,x372,a2)+P7(x371,x372,a3)+P7(x371,x372,a4)+P7(x371,x372,a1) % 59.60/59.70 %EqnAxiom % 59.60/59.70 % 59.60/59.70 %------------------------------------------- % 59.74/59.76 cnf(131,plain, % 59.74/59.76 (~P5(x1311,a2,a1)+~P5(a2,a1,x1311)), % 59.74/59.76 inference(scs_inference,[],[15,16,30,35])). % 59.74/59.76 cnf(253,plain, % 59.74/59.76 (~P5(x2531,a4,a1)+~P5(a4,a1,x2531)), % 59.74/59.76 inference(scs_inference,[],[18,15,30,35])). % 59.74/59.76 cnf(314,plain, % 59.74/59.76 (~P5(x3141,a1,a2)+~P5(a1,a2,x3141)), % 59.74/59.76 inference(scs_inference,[],[19,15,30,35])). % 59.74/59.76 cnf(375,plain, % 59.74/59.76 (~P5(x3751,a2,a3)+~P5(a2,a3,x3751)), % 59.74/59.76 inference(scs_inference,[],[20,15,30,35])). % 59.74/59.76 cnf(436,plain, % 59.74/59.76 (~P5(x4361,a2,a4)+~P5(a2,a4,x4361)), % 59.74/59.76 inference(scs_inference,[],[21,15,30,35])). % 59.74/59.76 cnf(497,plain, % 59.74/59.76 (~P5(x4971,a3,a1)+~P5(a3,a1,x4971)), % 59.74/59.76 inference(scs_inference,[],[22,15,30,35])). % 59.74/59.76 cnf(558,plain, % 59.74/59.76 (~P5(x5581,a3,a2)+~P5(a3,a2,x5581)), % 59.74/59.76 inference(scs_inference,[],[23,15,30,35])). % 59.74/59.76 cnf(619,plain, % 59.74/59.76 (~P5(x6191,a4,a3)+~P5(a4,a3,x6191)), % 59.74/59.76 inference(scs_inference,[],[24,15,30,35])). % 59.74/59.76 cnf(741,plain, % 59.74/59.76 (~P5(x7411,a4,a2)+~P5(a4,a2,x7411)), % 59.74/59.76 inference(scs_inference,[],[26,15,30,35])). % 59.74/59.76 cnf(893,plain, % 59.74/59.76 (P5(a2,a1,a3)+P5(a2,a1,a4)+P5(a2,a1,a1)), % 59.74/59.76 inference(scs_inference,[],[14,19,1,2,31,36])). % 59.74/59.76 cnf(1077,plain, % 59.74/59.76 (~P5(a2,a3,a4)+P5(a2,a1,a3)+P5(a2,a1,a1)), % 59.74/59.76 inference(scs_inference,[],[17,31,893])). % 59.74/59.76 cnf(2480,plain, % 59.74/59.76 (~P5(a2,a4,a3)+~P5(a2,a3,a4)+P5(a2,a1,a1)), % 59.74/59.76 inference(scs_inference,[],[25,31,1077])). % 59.74/59.76 cnf(4767,plain, % 59.74/59.76 (~P5(a2,a3,a2)), % 59.74/59.76 inference(scs_inference,[],[15,20,14,32,35])). % 59.74/59.76 cnf(4770,plain, % 59.74/59.76 (P5(a2,a3,a4)+P5(a2,a3,a1)+P5(a2,a3,a3)), % 59.74/59.76 inference(scs_inference,[],[3,4767,14,2,33,36])). % 59.74/59.76 cnf(4813,plain, % 59.74/59.76 (P5(a2,a3,a1)+P5(a2,a3,a3)+~P5(a4,a2,a3)), % 59.74/59.76 inference(scs_inference,[],[4770,375])). % 59.74/59.76 cnf(4859,plain, % 59.74/59.76 (P5(a2,a3,a3)+~P5(a3,a1,a2)+~P5(a4,a2,a3)), % 59.74/59.76 inference(scs_inference,[],[4813,497])). % 59.74/59.76 cnf(4996,plain, % 59.74/59.76 (~P5(a4,a2,a4)), % 59.74/59.76 inference(scs_inference,[],[21,15,14,32,35])). % 59.74/59.76 cnf(5042,plain, % 59.74/59.76 (~P5(a3,a2,a3)), % 59.74/59.76 inference(scs_inference,[],[23,15,14,32,35])). % 59.74/59.76 cnf(5088,plain, % 59.74/59.76 (~P5(a4,a3,a4)), % 59.74/59.76 inference(scs_inference,[],[24,15,14,32,35])). % 59.74/59.76 cnf(5134,plain, % 59.74/59.76 (~P5(a2,a4,a2)), % 59.74/59.76 inference(scs_inference,[],[26,15,14,32,35])). % 59.74/59.76 cnf(5137,plain, % 59.74/59.76 (P5(a2,a4,a4)+P5(a2,a4,a1)+P5(a2,a4,a3)), % 59.74/59.76 inference(scs_inference,[],[4,5134,14,2,33,36])). % 59.74/59.76 cnf(5226,plain, % 59.74/59.76 (~P5(a3,a4,a3)), % 59.74/59.76 inference(scs_inference,[],[27,15,14,32,35])). % 59.74/59.76 cnf(5317,plain, % 59.74/59.76 (P5(a3,a2,a4)+P5(a3,a2,a1)), % 59.74/59.76 inference(scs_inference,[],[14,20,5042,2,3,33,36])). % 59.74/59.76 cnf(5501,plain, % 59.74/59.76 (~P5(a2,a1,a3)+P5(a3,a2,a4)), % 59.74/59.76 inference(scs_inference,[],[5317,131])). % 59.74/59.76 cnf(5547,plain, % 59.74/59.76 (P5(a3,a2,a4)+P5(a2,a1,a4)+P5(a2,a1,a1)), % 59.74/59.76 inference(scs_inference,[],[5501,893])). % 59.74/59.76 cnf(123130,plain, % 59.74/59.76 (P7(x1231301,x1231301,x1231301)), % 59.74/59.76 inference(rename_variables,[],[15])). % 59.74/59.76 cnf(123133,plain, % 59.74/59.76 (P7(x1231331,x1231331,x1231331)), % 59.74/59.76 inference(rename_variables,[],[15])). % 59.74/59.76 cnf(123139,plain, % 59.74/59.76 (P5(x1231391,x1231391,x1231391)), % 59.74/59.76 inference(rename_variables,[],[14])). % 59.74/59.76 cnf(123142,plain, % 59.74/59.76 (P5(x1231421,x1231421,x1231421)), % 59.74/59.76 inference(rename_variables,[],[14])). % 59.74/59.76 cnf(123147,plain, % 59.74/59.76 (P5(a4,a2,a1)+P5(a4,a2,a3)), % 59.74/59.76 inference(scs_inference,[],[4996,21,17,2,15,123130,123133,14,123139,123142,4,34,30,32,29,31,33,36])). % 59.74/59.76 cnf(123153,plain, % 59.74/59.76 (P7(x1231531,x1231531,x1231531)), % 59.74/59.76 inference(rename_variables,[],[15])). % 59.74/59.76 cnf(123156,plain, % 59.74/59.76 (P5(x1231561,x1231561,x1231561)), % 59.74/59.76 inference(rename_variables,[],[14])). % 59.74/59.76 cnf(123158,plain, % 59.74/59.76 (~P7(a3,a2,a3)), % 59.74/59.76 inference(scs_inference,[],[23,18,15,123153,14,34,31,32])). % 59.74/59.76 cnf(123159,plain, % 59.74/59.76 (P7(x1231591,x1231591,x1231591)), % 59.74/59.76 inference(rename_variables,[],[15])). % 59.74/59.76 cnf(123162,plain, % 59.74/59.76 (P5(x1231621,x1231621,x1231621)), % 59.74/59.76 inference(rename_variables,[],[14])). % 59.74/59.76 cnf(123171,plain, % 59.74/59.76 (P5(a2,a3,a1)+P5(a2,a3,a4)), % 59.74/59.76 inference(scs_inference,[],[23,18,2,15,123153,123159,14,123156,123162,4767,3,34,31,32,29,33,30,4859,36])). % 59.74/59.76 cnf(123175,plain, % 59.74/59.76 (P7(x1231751,x1231751,x1231751)), % 59.74/59.76 inference(rename_variables,[],[15])). % 59.74/59.76 cnf(123178,plain, % 59.74/59.76 (P7(x1231781,x1231781,x1231781)), % 59.74/59.76 inference(rename_variables,[],[15])). % 59.74/59.76 cnf(123181,plain, % 59.74/59.76 (P5(x1231811,x1231811,x1231811)), % 59.74/59.76 inference(rename_variables,[],[14])). % 59.74/59.76 cnf(123183,plain, % 59.74/59.76 (~P5(a4,a1,a4)), % 59.74/59.76 inference(scs_inference,[],[24,25,15,123175,14,123181,34,32,33,31])). % 59.74/59.76 cnf(123184,plain, % 59.74/59.76 (P5(x1231841,x1231841,x1231841)), % 59.74/59.76 inference(rename_variables,[],[14])). % 59.74/59.76 cnf(123192,plain, % 59.74/59.76 (P5(a4,a3,a1)+P5(a4,a3,a2)), % 59.74/59.76 inference(scs_inference,[],[5088,24,25,15,123175,123178,14,123181,123184,4,3,34,32,33,31,29,30,36])). % 59.74/59.76 cnf(123194,plain, % 59.74/59.76 (P5(a4,a3,a2)+~P5(a3,a1,a4)), % 59.74/59.76 inference(scs_inference,[],[5088,24,25,15,123175,123178,14,123181,123184,4,3,34,32,33,31,29,30,36,497])). % 59.74/59.76 cnf(123199,plain, % 59.74/59.76 (P7(x1231991,x1231991,x1231991)), % 59.74/59.76 inference(rename_variables,[],[15])). % 59.74/59.76 cnf(123201,plain, % 59.74/59.76 (~P5(a2,a4,a4)), % 59.74/59.76 inference(scs_inference,[],[26,15,14,34,33])). % 59.74/59.76 cnf(123202,plain, % 59.74/59.76 (P5(x1232021,x1232021,x1232021)), % 59.74/59.76 inference(rename_variables,[],[14])). % 59.74/59.76 cnf(123205,plain, % 59.74/59.76 (P5(x1232051,x1232051,x1232051)), % 59.74/59.76 inference(rename_variables,[],[14])). % 59.74/59.76 cnf(123210,plain, % 59.74/59.76 (~P5(a1,a2,a1)), % 59.74/59.76 inference(scs_inference,[],[26,16,15,123199,14,123202,123205,34,33,29,32,31])). % 59.74/59.76 cnf(123217,plain, % 59.74/59.76 (P5(a2,a4,a1)+P5(a2,a4,a3)), % 59.74/59.76 inference(scs_inference,[],[123201,5137])). % 59.74/59.76 cnf(123224,plain, % 59.74/59.76 (P5(x1232241,x1232241,x1232241)), % 59.74/59.76 inference(rename_variables,[],[14])). % 59.74/59.76 cnf(123227,plain, % 59.74/59.76 (P5(x1232271,x1232271,x1232271)), % 59.74/59.76 inference(rename_variables,[],[14])). % 59.74/59.76 cnf(123229,plain, % 59.74/59.76 (~P5(a3,a4,a4)), % 59.74/59.76 inference(scs_inference,[],[27,19,15,14,123224,123227,34,29,31,33])). % 59.74/59.76 cnf(123241,plain, % 59.74/59.76 (~P7(a3,a2,a2)), % 59.74/59.76 inference(scs_inference,[],[20,15,34])). % 59.74/59.76 cnf(123244,plain, % 59.74/59.76 (~P5(a3,a1,a3)), % 59.74/59.76 inference(scs_inference,[],[20,22,15,14,34,31])). % 59.74/59.76 cnf(123262,plain, % 59.74/59.76 (P5(x1232621,x1232621,x1232621)), % 59.74/59.76 inference(rename_variables,[],[14])). % 59.74/59.76 cnf(123268,plain, % 59.74/59.76 (P7(x1232681,x1232681,x1232681)), % 59.74/59.76 inference(rename_variables,[],[15])). % 59.74/59.76 cnf(123271,plain, % 59.74/59.76 (P7(x1232711,x1232711,x1232711)), % 59.74/59.76 inference(rename_variables,[],[15])). % 59.74/59.76 cnf(123278,plain, % 59.74/59.76 (P5(a3,a1,a4)+P5(a3,a1,a2)), % 59.74/59.76 inference(scs_inference,[],[1,123158,123241,123244,17,2,15,123268,123271,14,123262,3,33,29,34,32,30,37,36])). % 59.74/59.76 cnf(123281,plain, % 59.74/59.76 (P5(x1232811,x1232811,x1232811)), % 59.74/59.76 inference(rename_variables,[],[14])). % 59.74/59.76 cnf(123286,plain, % 59.74/59.76 (P5(a4,a1,a3)+P5(a4,a1,a2)), % 59.74/59.76 inference(scs_inference,[],[1,123183,18,14,123281,4,33,29,36])). % 59.74/59.76 cnf(123308,plain, % 59.74/59.76 (P7(x1233081,x1233081,x1233081)), % 59.74/59.76 inference(rename_variables,[],[15])). % 59.74/59.76 cnf(123311,plain, % 59.74/59.76 (P7(x1233111,x1233111,x1233111)), % 59.74/59.76 inference(rename_variables,[],[15])). % 59.74/59.76 cnf(123313,plain, % 59.74/59.76 (~P5(a1,a2,a2)), % 59.74/59.76 inference(scs_inference,[],[19,15,123308,14,34,32,33])). % 59.74/59.76 cnf(123314,plain, % 59.74/59.76 (P5(x1233141,x1233141,x1233141)), % 59.74/59.76 inference(rename_variables,[],[14])). % 59.74/59.76 cnf(123324,plain, % 59.74/59.76 (P5(a3,a4,a2)+~P5(a4,a1,a3)), % 59.74/59.76 inference(scs_inference,[],[5226,123229,19,15,123308,123311,14,123314,4,3,34,32,33,30,29,36,253])). % 59.74/59.76 cnf(123344,plain, % 59.74/59.76 (~P5(a2,a1,a1)), % 59.74/59.76 inference(scs_inference,[],[16,14,33])). % 59.74/59.76 cnf(123345,plain, % 59.74/59.76 (P5(x1233451,x1233451,x1233451)), % 59.74/59.76 inference(rename_variables,[],[14])). % 59.74/59.76 cnf(123350,plain, % 59.74/59.76 (P5(a3,a2,a4)+P5(a2,a1,a4)), % 59.74/59.76 inference(scs_inference,[],[16,14,123345,33,29,5547])). % 59.74/59.76 cnf(123359,plain, % 59.74/59.76 (~P5(a2,a3,a4)+~P5(a2,a4,a3)), % 59.74/59.76 inference(scs_inference,[],[123344,2480])). % 59.74/59.76 cnf(123381,plain, % 59.74/59.76 (P5(a1,a2,a3)+~P5(a2,a4,a1)), % 59.74/59.76 inference(scs_inference,[],[1,123210,123313,2,36,436])). % 59.74/59.76 cnf(123442,plain, % 59.74/59.76 (P5(a4,a3,a1)+~P5(a3,a2,a4)), % 59.74/59.76 inference(scs_inference,[],[123192,558])). % 59.74/59.76 cnf(123443,plain, % 59.74/59.76 (~P5(a2,a4,a3)+~P5(a3,a1,a4)), % 59.74/59.76 inference(scs_inference,[],[123194,619])). % 59.74/59.76 cnf(123455,plain, % 59.74/59.76 (~P5(a4,a2,a3)+~P5(a4,a1,a3)), % 59.74/59.76 inference(scs_inference,[],[123324,741])). % 59.74/59.76 cnf(123466,plain, % 59.74/59.76 (P5(a4,a3,a1)+P5(a2,a1,a4)), % 59.74/59.76 inference(scs_inference,[],[123350,123442])). % 59.74/59.76 cnf(123472,plain, % 59.74/59.76 (~P5(a2,a3,a4)+P5(a2,a4,a1)), % 59.74/59.76 inference(scs_inference,[],[123359,123217])). % 59.74/59.76 cnf(123492,plain, % 59.74/59.76 (P5(a2,a4,a1)+~P5(a3,a1,a4)), % 59.74/59.76 inference(scs_inference,[],[123443,123217])). % 59.74/59.76 cnf(123499,plain, % 59.74/59.76 (P5(a4,a2,a1)+~P5(a4,a1,a3)), % 59.74/59.76 inference(scs_inference,[],[123455,123147])). % 59.74/59.76 cnf(123505,plain, % 59.74/59.76 (P5(a2,a1,a4)+~P5(a3,a1,a4)), % 59.74/59.76 inference(scs_inference,[],[123466,497])). % 59.74/59.76 cnf(123509,plain, % 59.74/59.76 (P5(a2,a4,a1)+P5(a2,a3,a1)), % 59.74/59.76 inference(scs_inference,[],[123472,123171])). % 59.74/59.76 cnf(123524,plain, % 59.74/59.76 (~P5(a3,a1,a4)+~P5(a4,a1,a2)), % 59.74/59.76 inference(scs_inference,[],[123492,253])). % 59.74/59.76 cnf(123536,plain, % 59.74/59.76 (~P5(a3,a1,a4)+~P5(a4,a2,a1)), % 59.74/59.76 inference(scs_inference,[],[123505,131])). % 59.74/59.76 cnf(123540,plain, % 59.74/59.76 (P5(a2,a4,a1)+~P5(a3,a1,a2)), % 59.74/59.76 inference(scs_inference,[],[123509,497])). % 59.74/59.76 cnf(123553,plain, % 59.74/59.76 (P5(a4,a1,a3)+~P5(a3,a1,a4)), % 59.74/59.76 inference(scs_inference,[],[123524,123286])). % 59.74/59.76 cnf(123563,plain, % 59.74/59.76 (P5(a3,a1,a2)+~P5(a4,a2,a1)), % 59.74/59.76 inference(scs_inference,[],[123536,123278])). % 59.74/59.76 cnf(123567,plain, % 59.74/59.76 (P5(a1,a2,a3)+~P5(a3,a1,a2)), % 59.74/59.76 inference(scs_inference,[],[123540,123381])). % 59.74/59.76 cnf(123590,plain, % 59.74/59.76 (~P5(a3,a1,a2)), % 59.74/59.76 inference(scs_inference,[],[123567,314])). % 59.74/59.76 cnf(123591,plain, % 59.74/59.76 (P5(a3,a1,a4)), % 59.74/59.76 inference(scs_inference,[],[123590,123278])). % 59.74/59.76 cnf(123592,plain, % 59.74/59.76 (~P5(a4,a2,a1)), % 59.74/59.76 inference(scs_inference,[],[123590,123563])). % 59.74/59.76 cnf(123598,plain, % 59.74/59.76 (~P5(a4,a1,a3)), % 59.74/59.76 inference(scs_inference,[],[123592,123499])). % 59.74/59.76 cnf(123603,plain, % 59.74/59.76 (P5(a4,a1,a3)), % 59.74/59.76 inference(scs_inference,[],[123591,123553])). % 59.74/59.76 cnf(123605,plain, % 59.74/59.76 ($false), % 59.74/59.76 inference(scs_inference,[],[123603,123598]), % 59.74/59.76 ['proof']). % 59.74/59.81 % SZS output end Proof % 59.74/59.81 % Total time :59.080000s %------------------------------------------------------------------------------