%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ALG203+1 : TPTP v8.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n007.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 03:40:59 EDT 2024 % Result : Theorem 190.30s 190.73s % Output : CNFRefutation 190.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.10 % Problem : ALG203+1 : TPTP v8.2.0. Released v2.7.0. % 0.03/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.10/0.30 % Computer : n007.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 300 % 0.10/0.30 % DateTime : Wed Jun 19 17:22:53 EDT 2024 % 0.10/0.30 % CPUTime : % 0.15/0.55 start to proof:theBenchmark % 190.30/190.71 %------------------------------------------- % 190.30/190.71 % File :CSE---1.7 % 190.30/190.71 % Problem :theBenchmark % 190.30/190.71 % Transform :cnf % 190.30/190.71 % Format :tptp:raw % 190.30/190.71 % Command :java -jar mcs_scs.jar %d %s % 190.30/190.71 % 190.30/190.71 % Result :Theorem 189.730000s % 190.30/190.71 % Output :CNFRefutation 189.730000s % 190.30/190.71 %------------------------------------------- % 190.30/190.72 %-------------------------------------------------------------------------- % 190.30/190.72 % File : ALG203+1 : TPTP v8.2.0. Released v2.7.0. % 190.30/190.72 % Domain : General Algebra % 190.30/190.72 % Problem : Quasigroups 7 QG5: CPROPS-SORTED-DISCRIMINANT-PROBLEM-3 % 190.30/190.72 % Version : Especial. % 190.30/190.72 % English : % 190.30/190.72 % 190.30/190.72 % Refs : [Mei03] Meier (2003), Email to G.Sutcliffe % 190.30/190.72 % : [CM+04] Colton et al. (2004), Automatic Generation of Classifi % 190.30/190.72 % Source : [Mei03] % 190.30/190.72 % Names : % 190.30/190.72 % 190.30/190.72 % Status : Theorem % 190.30/190.72 % Rating : 0.25 v7.5.0, 0.28 v7.4.0, 0.20 v7.3.0, 0.17 v7.1.0, 0.22 v7.0.0, 0.17 v6.4.0, 0.19 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.30 v6.0.0, 0.22 v5.5.0, 0.33 v5.4.0, 0.32 v5.3.0, 0.44 v5.2.0, 0.25 v5.1.0, 0.29 v5.0.0, 0.33 v4.1.0, 0.35 v4.0.0, 0.33 v3.7.0, 0.15 v3.5.0, 0.11 v3.4.0, 0.16 v3.3.0, 0.07 v3.2.0, 0.18 v3.1.0, 0.11 v2.7.0 % 190.30/190.72 % Syntax : Number of formulae : 5 ( 0 unt; 0 def) % 190.30/190.72 % Number of atoms : 28 ( 8 equ) % 190.30/190.72 % Maximal formula atoms : 14 ( 5 avg) % 190.30/190.72 % Number of connectives : 27 ( 4 ~; 0 |; 10 &) % 190.30/190.72 % ( 0 <=>; 13 =>; 0 <=; 0 <~>) % 190.30/190.72 % Maximal formula depth : 9 ( 6 avg) % 190.30/190.72 % Maximal term depth : 3 ( 1 avg) % 190.30/190.72 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty) % 190.30/190.72 % Number of functors : 4 ( 4 usr; 0 con; 1-2 aty) % 190.30/190.72 % Number of variables : 16 ( 12 !; 4 ?) % 190.30/190.72 % SPC : FOF_THM_RFO_SEQ % 190.30/190.72 % 190.30/190.72 % Comments : % 190.30/190.72 %-------------------------------------------------------------------------- % 190.30/190.72 fof(ax1,axiom, % 190.30/190.72 ! [U] : % 190.30/190.72 ( sorti1(U) % 190.30/190.72 => ! [V] : % 190.30/190.72 ( sorti1(V) % 190.30/190.72 => sorti1(op1(U,V)) ) ) ). % 190.30/190.72 % 190.30/190.72 fof(ax2,axiom, % 190.30/190.72 ! [U] : % 190.30/190.72 ( sorti2(U) % 190.30/190.72 => ! [V] : % 190.30/190.72 ( sorti2(V) % 190.30/190.72 => sorti2(op2(U,V)) ) ) ). % 190.30/190.72 % 190.30/190.72 fof(ax3,axiom, % 190.30/190.72 ( ? [U] : % 190.30/190.72 ( sorti1(U) % 190.30/190.72 & op1(U,U) = U ) % 190.30/190.72 & ? [V] : % 190.30/190.72 ( sorti1(V) % 190.30/190.72 & op1(V,V) != V ) ) ). % 190.30/190.72 % 190.30/190.72 fof(ax4,axiom, % 190.30/190.72 ~ ( ? [U] : % 190.30/190.72 ( sorti2(U) % 190.30/190.72 & op2(U,U) = U ) % 190.30/190.72 & ? [V] : % 190.30/190.72 ( sorti2(V) % 190.30/190.72 & op2(V,V) != V ) ) ). % 190.30/190.72 % 190.30/190.72 fof(co1,conjecture, % 190.30/190.72 ( ( ! [U] : % 190.30/190.72 ( sorti1(U) % 190.30/190.72 => sorti2(h(U)) ) % 190.30/190.72 & ! [V] : % 190.30/190.72 ( sorti2(V) % 190.30/190.72 => sorti1(j(V)) ) ) % 190.30/190.72 => ~ ( ! [W] : % 190.30/190.72 ( sorti1(W) % 190.30/190.72 => ! [X] : % 190.30/190.72 ( sorti1(X) % 190.30/190.72 => h(op1(W,X)) = op2(h(W),h(X)) ) ) % 190.30/190.72 & ! [Y] : % 190.30/190.72 ( sorti2(Y) % 190.30/190.72 => ! [Z] : % 190.30/190.72 ( sorti2(Z) % 190.30/190.72 => j(op2(Y,Z)) = op1(j(Y),j(Z)) ) ) % 190.30/190.73 & ! [X1] : % 190.30/190.73 ( sorti2(X1) % 190.30/190.73 => h(j(X1)) = X1 ) % 190.30/190.73 & ! [X2] : % 190.30/190.73 ( sorti1(X2) % 190.30/190.73 => j(h(X2)) = X2 ) ) ) ). % 190.30/190.73 % 190.30/190.73 %-------------------------------------------------------------------------- % 190.30/190.73 %------------------------------------------- % 190.30/190.73 % Proof found % 190.30/190.73 % SZS status Theorem for theBenchmark % 190.30/190.73 % SZS output start Proof % 190.30/190.73 %ClaNum:24(EqnAxiom:11) % 190.30/190.73 %VarNum:38(SingletonVarNum:14) % 190.30/190.73 %MaxLitNum:4 % 190.30/190.73 %MaxfuncDepth:2 % 190.30/190.73 %SharedTerms:8 % 190.30/190.73 %goalClause: 16 17 18 19 23 24 % 190.30/190.73 [12]P1(a1) % 190.30/190.73 [13]P1(a2) % 190.30/190.73 [14]E(f3(a1,a1),a1) % 190.30/190.73 [15]~E(f3(a2,a2),a2) % 190.30/190.73 [16]~P2(x161)+P1(f4(x161)) % 190.30/190.73 [17]~P1(x171)+P2(f5(x171)) % 190.30/190.73 [18]~P2(x181)+E(f5(f4(x181)),x181) % 190.30/190.73 [19]~P1(x191)+E(f4(f5(x191)),x191) % 190.30/190.73 [20]~P1(x202)+~P1(x201)+P1(f3(x201,x202)) % 190.30/190.73 [21]~P2(x212)+~P2(x211)+P2(f6(x211,x212)) % 190.30/190.73 [23]~P1(x232)+~P1(x231)+E(f6(f5(x231),f5(x232)),f5(f3(x231,x232))) % 190.30/190.73 [24]~P2(x242)+~P2(x241)+E(f3(f4(x241),f4(x242)),f4(f6(x241,x242))) % 190.30/190.73 [22]~P2(x221)+~P2(x222)+E(f6(x221,x221),x221)+~E(f6(x222,x222),x222) % 190.30/190.73 %EqnAxiom % 190.30/190.73 [1]E(x11,x11) % 190.30/190.73 [2]E(x22,x21)+~E(x21,x22) % 190.30/190.73 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 190.30/190.73 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43)) % 190.30/190.73 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52)) % 190.30/190.73 [6]~E(x61,x62)+E(f4(x61),f4(x62)) % 190.30/190.73 [7]~E(x71,x72)+E(f5(x71),f5(x72)) % 190.30/190.73 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83)) % 190.30/190.73 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92)) % 190.30/190.73 [10]~P1(x101)+P1(x102)+~E(x101,x102) % 190.30/190.73 [11]~P2(x111)+P2(x112)+~E(x111,x112) % 190.30/190.73 % 190.30/190.73 %------------------------------------------- % 190.30/190.75 cnf(25,plain, % 190.30/190.75 (E(a1,f3(a1,a1))), % 190.30/190.75 inference(scs_inference,[],[14,2])). % 190.30/190.75 cnf(32,plain, % 190.30/190.75 (E(f4(f5(f3(a1,a1))),f3(a1,a1))), % 190.30/190.75 inference(scs_inference,[],[25,12,19,10])). % 190.30/190.75 cnf(33,plain, % 190.30/190.75 (E(f3(a1,a1),f4(f5(f3(a1,a1))))), % 190.30/190.75 inference(scs_inference,[],[32,2])). % 190.30/190.75 cnf(34,plain, % 190.30/190.75 (E(f4(f5(f3(a1,a1))),a1)), % 190.30/190.75 inference(scs_inference,[],[32,14,2,3])). % 190.30/190.75 cnf(38,plain, % 190.30/190.75 (E(a1,f4(f5(f3(a1,a1))))), % 190.30/190.75 inference(scs_inference,[],[34,2])). % 190.30/190.75 cnf(39,plain, % 190.30/190.75 (~P2(f3(a1,a1))+P2(f4(f5(f3(a1,a1))))), % 190.30/190.75 inference(scs_inference,[],[33,34,2,11])). % 190.30/190.75 cnf(43,plain, % 190.30/190.75 (~P2(f4(f5(f3(a1,a1))))+P2(a1)), % 190.30/190.75 inference(scs_inference,[],[34,11])). % 190.30/190.75 cnf(56,plain, % 190.30/190.75 (~P2(x561)+P2(f5(f4(x561)))), % 190.30/190.75 inference(scs_inference,[],[16,17])). % 190.30/190.75 cnf(67,plain, % 190.30/190.75 (~P2(x671)+P1(f3(f4(x671),f4(x671)))), % 190.30/190.75 inference(scs_inference,[],[16,20])). % 190.30/190.75 cnf(83,plain, % 190.30/190.75 (~P2(x831)+~P2(x832)+P1(f4(f6(x832,x831)))), % 190.30/190.75 inference(scs_inference,[],[16,21])). % 190.30/190.75 cnf(89,plain, % 190.30/190.75 (P2(f5(f4(f5(a2))))), % 190.30/190.75 inference(scs_inference,[],[13,17,56])). % 190.30/190.75 cnf(111,plain, % 190.30/190.75 (P2(f5(f4(f5(a1))))), % 190.30/190.75 inference(scs_inference,[],[12,17,56])). % 190.30/190.75 cnf(119,plain, % 190.30/190.75 (E(f5(f4(f5(a1))),f5(a1))), % 190.30/190.75 inference(scs_inference,[],[12,17,18])). % 190.30/190.75 cnf(121,plain, % 190.30/190.75 (P2(f5(a1))), % 190.30/190.75 inference(scs_inference,[],[111,119,2,11])). % 190.30/190.75 cnf(143,plain, % 190.30/190.75 (E(f5(f4(f5(a2))),f5(a2))), % 190.30/190.75 inference(scs_inference,[],[13,17,18])). % 190.30/190.75 cnf(145,plain, % 190.30/190.75 (P2(f5(a2))), % 190.30/190.75 inference(scs_inference,[],[143,89,2,11])). % 190.30/190.75 cnf(178,plain, % 190.30/190.75 (E(a1,f4(f5(a1)))), % 190.30/190.75 inference(scs_inference,[],[12,2,19])). % 190.30/190.75 cnf(179,plain, % 190.30/190.75 (E(f4(f5(a1)),a1)), % 190.30/190.75 inference(scs_inference,[],[178,2])). % 190.30/190.75 cnf(180,plain, % 190.30/190.75 (E(f3(a1,a1),f4(f5(a1)))), % 190.30/190.75 inference(scs_inference,[],[178,14,2,3])). % 190.30/190.75 cnf(181,plain, % 190.30/190.75 (~P2(a1)+P2(f4(f5(a1)))), % 190.30/190.75 inference(scs_inference,[],[178,14,2,3,11])). % 190.30/190.75 cnf(186,plain, % 190.30/190.75 (E(f4(f5(a1)),f3(a1,a1))), % 190.30/190.75 inference(scs_inference,[],[180,2])). % 190.30/190.75 cnf(187,plain, % 190.30/190.75 (~P2(f4(f5(a1)))+P2(a1)), % 190.30/190.75 inference(scs_inference,[],[179,180,2,11])). % 190.30/190.75 cnf(188,plain, % 190.30/190.75 (~P2(f4(f5(a1)))+P2(f3(a1,a1))), % 190.30/190.75 inference(scs_inference,[],[186,11])). % 190.30/190.75 cnf(206,plain, % 190.30/190.75 (E(a2,f4(f5(a2)))), % 190.30/190.75 inference(scs_inference,[],[13,2,19])). % 190.30/190.75 cnf(207,plain, % 190.30/190.75 (E(f4(f5(a2)),a2)), % 190.30/190.75 inference(scs_inference,[],[206,2])). % 190.30/190.75 cnf(208,plain, % 190.30/190.75 (~E(f3(a2,a2),f4(f5(a2)))), % 190.30/190.75 inference(scs_inference,[],[206,15,2,3])). % 190.30/190.75 cnf(216,plain, % 190.30/190.75 (~E(a2,f3(a2,a2))), % 190.30/190.75 inference(scs_inference,[],[208,207,2,3])). % 190.30/190.75 cnf(231,plain, % 190.30/190.75 (E(f5(f3(a1,a1)),f6(f5(a1),f5(a1)))), % 190.30/190.75 inference(scs_inference,[],[12,2,23])). % 190.30/190.75 cnf(232,plain, % 190.30/190.75 (E(f6(f5(a1),f5(a1)),f5(f3(a1,a1)))), % 190.30/190.75 inference(scs_inference,[],[231,2])). % 190.30/190.75 cnf(421,plain, % 190.30/190.75 (E(f3(x4211,f4(f5(a2))),f3(x4211,a2))), % 190.30/190.75 inference(scs_inference,[],[13,19,5])). % 190.30/190.75 cnf(423,plain, % 190.30/190.75 (~E(a2,f3(a2,f4(f5(a2))))), % 190.30/190.75 inference(scs_inference,[],[421,216,2,3])). % 190.30/190.75 cnf(424,plain, % 190.30/190.75 (E(f3(x4241,f4(f5(a2))),f3(x4241,a2))), % 190.30/190.75 inference(rename_variables,[],[421])). % 190.30/190.75 cnf(425,plain, % 190.37/190.75 (~P1(f3(x4251,f4(f5(a2))))+P1(f3(x4251,a2))), % 190.37/190.75 inference(scs_inference,[],[421,424,216,2,3,10])). % 190.37/190.75 cnf(427,plain, % 190.37/190.75 (P1(f3(f4(f5(a2)),a2))), % 190.37/190.75 inference(scs_inference,[],[145,425,67])). % 190.37/190.75 cnf(648,plain, % 190.37/190.75 (E(f5(a1),f5(f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[14,7,2])). % 190.37/190.75 cnf(650,plain, % 190.37/190.75 (E(f6(f5(a1),f5(a1)),f5(a1))), % 190.37/190.75 inference(scs_inference,[],[232,648,2,3])). % 190.37/190.75 cnf(800,plain, % 190.37/190.75 (~P2(f4(f5(f3(a1,a1))))+E(f6(a1,a1),a1)), % 190.37/190.75 inference(scs_inference,[],[650,121,43,22])). % 190.37/190.75 cnf(801,plain, % 190.37/190.75 (E(a1,f6(a1,a1))+~P2(f4(f5(f3(a1,a1))))), % 190.37/190.75 inference(scs_inference,[],[800,2])). % 190.37/190.75 cnf(802,plain, % 190.37/190.75 (E(a1,f6(a1,a1))+~P2(f3(a1,a1))), % 190.37/190.75 inference(scs_inference,[],[801,39])). % 190.37/190.75 cnf(878,plain, % 190.37/190.75 (~P2(f4(f5(a1)))+E(a1,f6(a1,a1))), % 190.37/190.75 inference(scs_inference,[],[188,802])). % 190.37/190.75 cnf(879,plain, % 190.37/190.75 (E(a1,f6(a1,a1))+~P2(a1)), % 190.37/190.75 inference(scs_inference,[],[878,181])). % 190.37/190.75 cnf(880,plain, % 190.37/190.75 (E(f6(a1,a1),a1)+~P2(a1)), % 190.37/190.75 inference(scs_inference,[],[879,2])). % 190.37/190.75 cnf(933,plain, % 190.37/190.75 (E(f6(a1,a1),a1)+~P2(f4(f5(a1)))), % 190.37/190.75 inference(scs_inference,[],[880,187])). % 190.37/190.75 cnf(1528,plain, % 190.37/190.75 (E(x15281,a1)+~E(x15281,f6(a1,a1))+~P2(f4(f5(a1)))), % 190.37/190.75 inference(scs_inference,[],[933,3])). % 190.37/190.75 cnf(1581,plain, % 190.37/190.75 (E(f3(f4(f5(a2)),x15811),f3(a2,x15811))), % 190.37/190.75 inference(scs_inference,[],[13,4,19])). % 190.37/190.75 cnf(1583,plain, % 190.37/190.75 (P1(f3(a2,a2))), % 190.37/190.75 inference(scs_inference,[],[427,1581,2,10])). % 190.37/190.75 cnf(1599,plain, % 190.37/190.75 (E(f3(a1,x15991),f3(f3(a1,a1),x15991))), % 190.37/190.75 inference(scs_inference,[],[32,38,4,3])). % 190.37/190.75 cnf(1600,plain, % 190.37/190.75 (E(f3(f3(a1,a1),x16001),f3(a1,x16001))), % 190.37/190.75 inference(scs_inference,[],[1599,2])). % 190.37/190.75 cnf(1700,plain, % 190.37/190.75 (E(f4(f5(a1)),f3(f3(a1,a1),a1))), % 190.37/190.75 inference(scs_inference,[],[186,1599,3])). % 190.37/190.75 cnf(1705,plain, % 190.37/190.75 (E(a1,f3(f3(a1,a1),a1))), % 190.37/190.75 inference(scs_inference,[],[178,1700,3])). % 190.37/190.75 cnf(1706,plain, % 190.37/190.75 (E(f3(f3(a1,a1),a1),a1)), % 190.37/190.75 inference(scs_inference,[],[178,1700,3,2])). % 190.37/190.75 cnf(1737,plain, % 190.37/190.75 (E(f3(f3(a1,a1),f4(f5(a2))),f3(a1,a2))), % 190.37/190.75 inference(scs_inference,[],[421,1600,3])). % 190.37/190.75 cnf(1741,plain, % 190.37/190.75 (E(f3(a1,a2),f3(f3(a1,a1),f4(f5(a2))))), % 190.37/190.75 inference(scs_inference,[],[1737,2])). % 190.37/190.75 cnf(1742,plain, % 190.37/190.75 (~P1(f3(f3(a1,a1),f4(f5(a2))))+P1(f3(a1,a2))), % 190.37/190.75 inference(scs_inference,[],[1737,2,10])). % 190.37/190.75 cnf(1745,plain, % 190.37/190.75 (~P1(f3(a1,a2))+P1(f3(f3(a1,a1),f4(f5(a2))))), % 190.37/190.75 inference(scs_inference,[],[1741,10])). % 190.37/190.75 cnf(1750,plain, % 190.37/190.75 (~P1(f3(f3(a1,a1),f4(f5(a2))))+P2(f5(f3(a1,a2)))), % 190.37/190.75 inference(scs_inference,[],[1742,17])). % 190.37/190.75 cnf(1751,plain, % 190.37/190.75 (P1(f3(f3(a1,a1),f4(f5(a2))))), % 190.37/190.75 inference(scs_inference,[],[13,12,1745,20])). % 190.37/190.75 cnf(1753,plain, % 190.37/190.75 (P2(f5(f3(a1,a2)))), % 190.37/190.75 inference(scs_inference,[],[1751,1750])). % 190.37/190.75 cnf(1773,plain, % 190.37/190.75 (P1(f3(f3(a1,a1),a2))), % 190.37/190.75 inference(scs_inference,[],[1751,421,10])). % 190.37/190.75 cnf(1927,plain, % 190.37/190.75 (E(f3(f4(f5(a1)),x19271),f3(a1,x19271))), % 190.37/190.75 inference(scs_inference,[],[12,4,19])). % 190.37/190.75 cnf(1928,plain, % 190.37/190.75 (E(f3(a1,x19281),f3(f4(f5(a1)),x19281))), % 190.37/190.75 inference(scs_inference,[],[1927,2])). % 190.37/190.75 cnf(2038,plain, % 190.37/190.75 (E(a1,f3(f4(f5(a1)),a1))), % 190.37/190.75 inference(scs_inference,[],[25,1928,3])). % 190.37/190.75 cnf(2040,plain, % 190.37/190.75 (P1(f3(f4(f5(a1)),a1))), % 190.37/190.75 inference(scs_inference,[],[25,1928,12,3,10])). % 190.37/190.75 cnf(2165,plain, % 190.37/190.75 (E(f4(f5(f3(a2,a2))),f3(a2,a2))), % 190.37/190.75 inference(scs_inference,[],[1773,1583,1753,16,17,19])). % 190.37/190.75 cnf(2178,plain, % 190.37/190.75 (E(f6(f5(a2),f5(a2)),f5(f3(a2,a2)))), % 190.37/190.75 inference(scs_inference,[],[13,1773,423,1705,1583,1753,145,16,17,19,6,7,4,5,8,9,2,21,83,23])). % 190.37/190.75 cnf(2265,plain, % 190.37/190.75 (E(f3(x22651,f3(a1,a1)),f3(x22651,a1))), % 190.37/190.75 inference(scs_inference,[],[178,14,9,5])). % 190.37/190.75 cnf(2268,plain, % 190.37/190.75 (E(f3(x22681,a1),f3(x22681,f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[179,25,9,5])). % 190.37/190.75 cnf(2269,plain, % 190.37/190.75 (E(f6(f4(f5(a1)),x22691),f6(a1,x22691))), % 190.37/190.75 inference(scs_inference,[],[179,25,9,5,8])). % 190.37/190.75 cnf(2280,plain, % 190.37/190.75 (P1(f3(f4(f5(a1)),f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[2268,2040,14,8,9,10])). % 190.37/190.75 cnf(2324,plain, % 190.37/190.75 (E(f6(f5(a2),f5(a2)),f5(a2))), % 190.37/190.75 inference(scs_inference,[],[2269,650,145,121,1528,22])). % 190.37/190.75 cnf(2472,plain, % 190.37/190.75 (P1(f3(a1,f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[2280,1927,10])). % 190.37/190.75 cnf(2503,plain, % 190.37/190.75 (E(a1,f3(f4(f5(a1)),f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[2038,2268,3])). % 190.37/190.75 cnf(2569,plain, % 190.37/190.75 (E(f3(f3(a1,a1),a1),f3(f4(f5(a1)),f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[2503,1706,3])). % 190.37/190.75 cnf(2587,plain, % 190.37/190.75 (E(a1,f3(a1,f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[2503,1927,3])). % 190.37/190.75 cnf(2590,plain, % 190.37/190.75 (E(f3(a1,x25901),f3(f3(a1,f3(a1,a1)),x25901))), % 190.37/190.75 inference(scs_inference,[],[2503,1927,3,7,4])). % 190.37/190.75 cnf(2596,plain, % 190.37/190.75 (P1(f3(f3(a1,f3(a1,a1)),f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[2590,2472,10])). % 190.37/190.75 cnf(2647,plain, % 190.37/190.75 (E(f3(f3(a1,a1),a1),f3(a1,f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[2569,1927,3])). % 190.37/190.75 cnf(2656,plain, % 190.37/190.75 (E(f4(f5(a1)),f3(a1,f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[2647,1700,3])). % 190.37/190.75 cnf(2662,plain, % 190.37/190.75 (E(f4(f5(a1)),f3(f3(a1,a1),f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[1599,2656,3])). % 190.37/190.75 cnf(2685,plain, % 190.37/190.75 (E(f3(f4(f5(a1)),f3(a1,a1)),f3(a1,a1))), % 190.37/190.75 inference(scs_inference,[],[1927,2265,3])). % 190.37/190.75 cnf(2720,plain, % 190.37/190.75 (E(f3(a1,a1),f3(f3(a1,a1),f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[2662,180,3])). % 190.37/190.75 cnf(2725,plain, % 190.37/190.75 (E(f3(f4(f5(a1)),f3(a1,a1)),f3(f3(a1,a1),f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[2720,2685,3])). % 190.37/190.75 cnf(2732,plain, % 190.37/190.75 (E(f3(a1,x27321),f3(f3(f3(a1,a1),f3(a1,a1)),x27321))), % 190.37/190.75 inference(scs_inference,[],[2725,2503,3,7,4])). % 190.37/190.75 cnf(2849,plain, % 190.37/190.75 (E(a1,f3(f3(f3(a1,a1),f3(a1,a1)),f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[2587,2732,3])). % 190.37/190.75 cnf(3096,plain, % 190.37/190.75 (E(f4(f5(f3(a1,a1))),f3(a1,f3(a1,a1)))), % 190.37/190.75 inference(scs_inference,[],[32,2268,2587,2,3])). % 190.37/190.75 cnf(3151,plain, % 190.37/190.75 (E(f3(f3(f3(a1,a1),f3(a1,a1)),f3(a1,a1)),a1)), % 190.37/190.75 inference(scs_inference,[],[2849,2])). % 190.37/190.75 cnf(3199,plain, % 190.37/190.75 (E(f5(a2),f6(f5(a2),f5(a2)))), % 190.37/190.75 inference(scs_inference,[],[2324,2])). % 190.37/190.75 cnf(3780,plain, % 190.37/190.75 (E(f3(a2,a2),f4(f5(f3(a2,a2))))), % 190.37/190.75 inference(scs_inference,[],[2165,2])). % 190.37/190.75 cnf(4905,plain, % 190.37/190.75 (E(f5(a2),f5(f3(a2,a2)))), % 190.37/190.75 inference(scs_inference,[],[2178,3096,3199,2,3])). % 190.37/190.75 cnf(5135,plain, % 190.37/190.75 (~E(a2,f4(f5(f3(a2,a2))))), % 190.37/190.75 inference(scs_inference,[],[15,3780,3,2])). % 190.37/190.75 cnf(5230,plain, % 190.37/190.75 (~E(f4(f5(a2)),f4(f5(f3(a2,a2))))), % 190.37/190.75 inference(scs_inference,[],[3151,2596,5135,1773,206,1753,17,8,6,5,9,7,21,4,20,3])). % 190.37/190.75 cnf(5434,plain, % 190.37/190.75 ($false), % 190.37/190.75 inference(scs_inference,[],[2268,5230,4905,5,7,6]), % 190.37/190.75 ['proof']). % 190.37/190.75 % SZS output end Proof % 190.37/190.75 % Total time :189.730000s %------------------------------------------------------------------------------