%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS138+1 : TPTP v8.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n026.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 10:08:38 EDT 2024 % Result : Theorem 79.65s 79.86s % Output : CNFRefutation 79.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : KRS138+1 : TPTP v8.2.0. Released v3.1.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n026.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 : Wed Jun 19 13:13:09 EDT 2024 % 0.12/0.35 % CPUTime : % 0.21/0.53 start to proof:theBenchmark % 79.65/79.85 %------------------------------------------- % 79.65/79.85 % File :CSE---1.7 % 79.65/79.85 % Problem :theBenchmark % 79.65/79.85 % Transform :cnf % 79.65/79.85 % Format :tptp:raw % 79.65/79.85 % Command :java -jar mcs_scs.jar %d %s % 79.65/79.85 % 79.65/79.85 % Result :Theorem 79.110000s % 79.65/79.85 % Output :CNFRefutation 79.110000s % 79.65/79.85 %------------------------------------------- % 79.65/79.85 %------------------------------------------------------------------------------ % 79.65/79.85 % File : KRS138+1 : TPTP v8.2.0. Released v3.1.0. % 79.65/79.85 % Domain : Knowledge Representation (Semantic Web) % 79.65/79.85 % Problem : Extensional semantics of owl:SymmetricProperty % 79.65/79.85 % Version : Especial. % 79.65/79.85 % English : Test illustrating extensional semantics of owl:SymmetricProperty. % 79.65/79.85 % 79.65/79.85 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 79.65/79.85 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 79.65/79.85 % Source : [Bec03] % 79.65/79.85 % Names : positive_SymmetricProperty-Manifest002 [Bec03] % 79.65/79.85 % 79.65/79.85 % Status : Theorem % 79.65/79.85 % Rating : 0.00 v5.3.0, 0.09 v5.2.0, 0.00 v4.1.0, 0.13 v4.0.1, 0.17 v4.0.0, 0.21 v3.7.0, 0.00 v3.2.0, 0.11 v3.1.0 % 79.65/79.85 % Syntax : Number of formulae : 18 ( 5 unt; 0 def) % 79.65/79.85 % Number of atoms : 52 ( 13 equ) % 79.65/79.85 % Maximal formula atoms : 14 ( 2 avg) % 79.65/79.85 % Number of connectives : 38 ( 4 ~; 3 |; 17 &) % 79.65/79.85 % ( 3 <=>; 11 =>; 0 <=; 0 <~>) % 79.65/79.85 % Maximal formula depth : 9 ( 4 avg) % 79.65/79.85 % Maximal term depth : 1 ( 1 avg) % 79.65/79.85 % Number of predicates : 7 ( 6 usr; 0 prp; 1-2 aty) % 79.65/79.85 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 79.65/79.85 % Number of variables : 30 ( 30 !; 0 ?) % 79.65/79.85 % SPC : FOF_THM_EPR_SEQ % 79.65/79.85 % 79.65/79.85 % Comments : Sean Bechhofer says there are some errors in the encoding of % 79.65/79.85 % datatypes, so this problem may not be perfect. At least it's % 79.65/79.85 % still representative of the type of reasoning required for OWL. % 79.65/79.85 %------------------------------------------------------------------------------ % 79.65/79.85 fof(cA_substitution_1,axiom, % 79.65/79.85 ! [A,B] : % 79.65/79.85 ( ( A = B % 79.65/79.85 & cA(A) ) % 79.65/79.85 => cA(B) ) ). % 79.65/79.85 % 79.65/79.85 fof(cowlNothing_substitution_1,axiom, % 79.65/79.85 ! [A,B] : % 79.65/79.85 ( ( A = B % 79.65/79.85 & cowlNothing(A) ) % 79.65/79.85 => cowlNothing(B) ) ). % 79.65/79.85 % 79.65/79.85 fof(cowlThing_substitution_1,axiom, % 79.65/79.85 ! [A,B] : % 79.65/79.85 ( ( A = B % 79.65/79.85 & cowlThing(A) ) % 79.65/79.85 => cowlThing(B) ) ). % 79.65/79.85 % 79.65/79.85 fof(requalityOnA_substitution_1,axiom, % 79.65/79.85 ! [A,B,C] : % 79.65/79.85 ( ( A = B % 79.65/79.85 & requalityOnA(A,C) ) % 79.65/79.85 => requalityOnA(B,C) ) ). % 79.65/79.85 % 79.65/79.85 fof(requalityOnA_substitution_2,axiom, % 79.65/79.85 ! [A,B,C] : % 79.65/79.85 ( ( A = B % 79.65/79.86 & requalityOnA(C,A) ) % 79.65/79.86 => requalityOnA(C,B) ) ). % 79.65/79.86 % 79.65/79.86 fof(xsd_integer_substitution_1,axiom, % 79.65/79.86 ! [A,B] : % 79.65/79.86 ( ( A = B % 79.65/79.86 & xsd_integer(A) ) % 79.65/79.86 => xsd_integer(B) ) ). % 79.65/79.86 % 79.65/79.86 fof(xsd_string_substitution_1,axiom, % 79.65/79.86 ! [A,B] : % 79.65/79.86 ( ( A = B % 79.65/79.86 & xsd_string(A) ) % 79.65/79.86 => xsd_string(B) ) ). % 79.65/79.86 % 79.65/79.86 %----Thing and Nothing % 79.65/79.86 fof(axiom_0,axiom, % 79.65/79.86 ! [X] : % 79.65/79.86 ( cowlThing(X) % 79.65/79.86 & ~ cowlNothing(X) ) ). % 79.65/79.86 % 79.65/79.86 %----String and Integer disjoint % 79.65/79.86 fof(axiom_1,axiom, % 79.65/79.86 ! [X] : % 79.65/79.86 ( xsd_string(X) % 79.65/79.86 <=> ~ xsd_integer(X) ) ). % 79.65/79.86 % 79.65/79.86 %----Enumeration cA % 79.65/79.86 fof(axiom_2,axiom, % 79.65/79.86 ! [X] : % 79.65/79.86 ( cA(X) % 79.65/79.86 <=> ( X = ib % 79.65/79.86 | X = ia ) ) ). % 79.65/79.86 % 79.65/79.86 %----InverseFunctional: requalityOnA % 79.65/79.86 fof(axiom_3,axiom, % 79.65/79.86 ! [X,Y,Z] : % 79.65/79.86 ( ( requalityOnA(Y,X) % 79.65/79.86 & requalityOnA(Z,X) ) % 79.65/79.86 => Y = Z ) ). % 79.65/79.86 % 79.65/79.86 %----Range: requalityOnA % 79.65/79.86 fof(axiom_4,axiom, % 79.65/79.86 ! [X,Y] : % 79.65/79.86 ( requalityOnA(X,Y) % 79.65/79.86 => cA(Y) ) ). % 79.65/79.86 % 79.65/79.86 %----ia % 79.65/79.86 fof(axiom_5,axiom, % 79.65/79.86 cowlThing(ia) ). % 79.65/79.86 % 79.65/79.86 fof(axiom_6,axiom, % 79.65/79.86 requalityOnA(ia,ia) ). % 79.65/79.86 % 79.65/79.86 %----ib % 79.65/79.86 fof(axiom_7,axiom, % 79.65/79.86 cowlThing(ib) ). % 79.65/79.86 % 79.65/79.86 fof(axiom_8,axiom, % 79.65/79.86 requalityOnA(ib,ib) ). % 79.65/79.86 % 79.65/79.86 %----ic % 79.65/79.86 fof(axiom_9,axiom, % 79.65/79.86 cowlThing(ic) ). % 79.65/79.86 % 79.65/79.86 %----Thing and Nothing % 79.65/79.86 %----String and Integer disjoint % 79.65/79.86 %----Domain: requalityOnA % 79.65/79.86 %----Symmetric: requalityOnA % 79.65/79.86 %----ia % 79.65/79.86 %----ib % 79.65/79.86 %----ic % 79.65/79.86 fof(the_axiom,conjecture, % 79.65/79.86 ( ! [X] : % 79.65/79.86 ( cowlThing(X) % 79.65/79.86 & ~ cowlNothing(X) ) % 79.65/79.86 & ! [X] : % 79.65/79.86 ( xsd_string(X) % 79.65/79.86 <=> ~ xsd_integer(X) ) % 79.65/79.86 & ! [X,Y] : % 79.65/79.86 ( requalityOnA(X,Y) % 79.65/79.86 => ( X = ia % 79.65/79.86 | X = ib % 79.65/79.86 | X = ic ) ) % 79.65/79.86 & ! [X,Y] : % 79.65/79.86 ( requalityOnA(X,Y) % 79.65/79.86 => requalityOnA(Y,X) ) % 79.65/79.86 & cowlThing(ia) % 79.65/79.86 & requalityOnA(ia,ia) % 79.65/79.86 & cowlThing(ib) % 79.65/79.86 & cowlThing(ic) ) ). % 79.65/79.86 % 79.65/79.86 %------------------------------------------------------------------------------ % 79.65/79.86 %------------------------------------------- % 79.65/79.86 % Proof found % 79.65/79.86 % SZS status Theorem for theBenchmark % 79.65/79.86 % SZS output start Proof % 79.65/79.86 %ClaNum:35(EqnAxiom:9) % 79.65/79.86 %VarNum:21(SingletonVarNum:11) % 79.65/79.86 %MaxLitNum:6 % 79.65/79.86 %MaxfuncDepth:0 % 79.65/79.86 %SharedTerms:23 % 79.65/79.86 %goalClause: 19 20 21 22 23 24 26 27 28 29 30 31 32 33 34 35 % 79.65/79.86 [10]P1(a1,a1) % 79.65/79.86 [11]P1(a2,a2) % 79.65/79.86 [12]~P2(x121) % 79.65/79.86 [13]P3(x131)+~E(x131,a1) % 79.65/79.86 [14]P3(x141)+~E(x141,a2) % 79.65/79.86 [15]P5(x151)+P4(x151) % 79.65/79.86 [17]~P5(x171)+~P4(x171) % 79.65/79.86 [18]P3(x181)+~P1(x182,x181) % 79.65/79.86 [16]~P3(x161)+E(x161,a2)+E(x161,a1) % 79.65/79.86 [25]~P1(x251,x253)+E(x251,x252)+~P1(x252,x253) % 79.65/79.86 [19]P2(a3)+P4(a4)+P1(a5,a8)+~E(a6,a1)+~P5(a4)+~P1(a2,a2) % 79.65/79.86 [20]P1(a5,a8)+~P1(a2,a2)+P2(a3)+P4(a4)+~E(a6,a2)+~P5(a4) % 79.65/79.86 [21]P1(a5,a8)+~P1(a2,a2)+P2(a3)+P4(a4)+~E(a9,a6)+~P5(a4) % 79.65/79.86 [22]P1(a5,a8)+~P1(a2,a2)+~E(a6,a1)+P2(a3)+P5(a4)+~P4(a4) % 79.65/79.86 [23]P1(a5,a8)+~P1(a2,a2)+~E(a6,a2)+P2(a3)+P5(a4)+~P4(a4) % 79.65/79.86 [24]P1(a5,a8)+~P1(a2,a2)+~E(a9,a6)+P2(a3)+P5(a4)+~P4(a4) % 79.65/79.86 [26]~P1(a2,a2)+~E(a6,a1)+P2(a3)+P4(a4)+~P5(a4)+~P1(a8,a5) % 79.65/79.86 [27]~P1(a2,a2)+~E(a6,a2)+~P1(a8,a5)+P2(a3)+P4(a4)+~P5(a4) % 79.65/79.86 [28]~P1(a2,a2)+~E(a9,a6)+~P1(a8,a5)+P2(a3)+P4(a4)+~P5(a4) % 79.65/79.86 [29]~P1(a2,a2)+~E(a6,a1)+~P1(a8,a5)+P2(a3)+P5(a4)+~P4(a4) % 79.65/79.86 [30]~P1(a2,a2)+~P1(a8,a5)+~E(a6,a2)+P2(a3)+P5(a4)+~P4(a4) % 79.65/79.86 [31]~P1(a2,a2)+~P1(a8,a5)+~E(a9,a6)+P2(a3)+P5(a4)+~P4(a4) % 79.65/79.86 [32]~P1(a2,a2)+P1(a5,a8)+P2(a3)+P4(a4)+P1(a6,a7)+~P5(a4) % 79.65/79.86 [33]~P1(a2,a2)+P1(a5,a8)+P1(a6,a7)+P2(a3)+P5(a4)+~P4(a4) % 79.65/79.86 [34]~P1(a2,a2)+~P1(a8,a5)+P1(a6,a7)+P2(a3)+P4(a4)+~P5(a4) % 79.65/79.86 [35]~P1(a2,a2)+~P1(a8,a5)+P1(a6,a7)+P2(a3)+P5(a4)+~P4(a4) % 79.65/79.86 %EqnAxiom % 79.65/79.86 [1]E(x11,x11) % 79.65/79.86 [2]E(x22,x21)+~E(x21,x22) % 79.65/79.86 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 79.65/79.86 [4]P1(x42,x43)+~E(x41,x42)+~P1(x41,x43) % 79.65/79.86 [5]P1(x53,x52)+~E(x51,x52)+~P1(x53,x51) % 79.65/79.86 [6]~P4(x61)+P4(x62)+~E(x61,x62) % 79.65/79.86 [7]~P2(x71)+P2(x72)+~E(x71,x72) % 79.65/79.86 [8]~P3(x81)+P3(x82)+~E(x81,x82) % 79.65/79.86 [9]~P5(x91)+P5(x92)+~E(x91,x92) % 79.65/79.86 % 79.65/79.86 %------------------------------------------- % 79.65/79.87 cnf(38,plain, % 79.65/79.87 (P1(x381,a1)+~E(a1,x381)), % 79.65/79.87 inference(scs_inference,[],[10,4])). % 79.65/79.87 cnf(41,plain, % 79.65/79.87 (P1(a1,x411)+~E(a1,x411)), % 79.65/79.87 inference(scs_inference,[],[10,4,25,6,5])). % 79.65/79.87 cnf(48,plain, % 79.65/79.87 (P1(a5,a8)+~E(a6,a1)+P4(a4)+~P5(a4)), % 79.65/79.87 inference(scs_inference,[],[12,11,19])). % 79.65/79.87 cnf(49,plain, % 79.65/79.87 (P1(a5,a8)+~E(a6,a2)+P4(a4)+~P5(a4)), % 79.65/79.87 inference(scs_inference,[],[12,11,20])). % 79.65/79.87 cnf(50,plain, % 79.65/79.87 (P1(a5,a8)+~E(a9,a6)+P4(a4)+~P5(a4)), % 79.65/79.87 inference(scs_inference,[],[12,11,21])). % 79.65/79.87 cnf(51,plain, % 79.65/79.87 (P1(a5,a8)+~E(a6,a1)+P5(a4)+~P4(a4)), % 79.65/79.87 inference(scs_inference,[],[12,11,22])). % 79.65/79.87 cnf(52,plain, % 79.65/79.87 (P1(a5,a8)+~E(a6,a2)+P5(a4)+~P4(a4)), % 79.65/79.87 inference(scs_inference,[],[12,11,23])). % 79.65/79.87 cnf(53,plain, % 79.65/79.87 (P1(a5,a8)+~E(a9,a6)+P5(a4)+~P4(a4)), % 79.65/79.87 inference(scs_inference,[],[12,11,24])). % 79.65/79.87 cnf(54,plain, % 79.65/79.87 (~P1(a8,a5)+~E(a6,a1)+P4(a4)+~P5(a4)), % 79.65/79.87 inference(scs_inference,[],[12,11,26])). % 79.65/79.87 cnf(55,plain, % 79.65/79.87 (~P1(a8,a5)+~E(a6,a2)+P4(a4)+~P5(a4)), % 79.65/79.87 inference(scs_inference,[],[12,11,27])). % 79.65/79.87 cnf(57,plain, % 79.65/79.87 (~P1(a8,a5)+~E(a6,a1)+P5(a4)+~P4(a4)), % 79.65/79.87 inference(scs_inference,[],[12,11,29])). % 79.65/79.87 cnf(58,plain, % 79.65/79.87 (~P1(a8,a5)+~E(a6,a2)+P5(a4)+~P4(a4)), % 79.65/79.87 inference(scs_inference,[],[12,11,30])). % 79.65/79.87 cnf(60,plain, % 79.65/79.87 (P1(a5,a8)+P1(a6,a7)+P4(a4)+~P5(a4)), % 79.65/79.87 inference(scs_inference,[],[12,11,32])). % 79.65/79.87 cnf(61,plain, % 79.65/79.87 (P1(a5,a8)+P1(a6,a7)+P5(a4)+~P4(a4)), % 79.65/79.87 inference(scs_inference,[],[12,11,33])). % 79.65/79.87 cnf(62,plain, % 79.65/79.87 (~P1(a8,a5)+P1(a6,a7)+P4(a4)+~P5(a4)), % 79.65/79.87 inference(scs_inference,[],[12,11,34])). % 79.65/79.87 cnf(63,plain, % 79.65/79.87 (~P1(a8,a5)+P1(a6,a7)+P5(a4)+~P4(a4)), % 79.65/79.87 inference(scs_inference,[],[12,11,35])). % 79.65/79.87 cnf(64,plain, % 79.65/79.87 (P1(a2,x641)+~E(a2,x641)), % 79.65/79.87 inference(scs_inference,[],[11,5])). % 79.65/79.87 cnf(65,plain, % 79.65/79.87 (P1(x651,a2)+~E(a2,x651)), % 79.65/79.87 inference(scs_inference,[],[11,5,4])). % 79.65/79.87 cnf(71,plain, % 79.65/79.87 (~E(x711,x712)+E(x712,x713)+~E(x713,x711)), % 79.65/79.87 inference(scs_inference,[],[2,3])). % 79.65/79.87 cnf(73,plain, % 79.65/79.87 (~E(x731,x732)+~E(x732,a1)+P1(x731,a1)), % 79.65/79.87 inference(scs_inference,[],[10,71,4])). % 79.65/79.87 cnf(81,plain, % 79.65/79.87 (P1(a5,a8)+~E(a6,a1)+P5(a4)), % 79.65/79.87 inference(scs_inference,[],[15,51])). % 79.65/79.87 cnf(82,plain, % 79.65/79.87 (P3(a8)+~E(a6,a1)+P5(a4)), % 79.65/79.87 inference(scs_inference,[],[81,18])). % 79.65/79.87 cnf(83,plain, % 79.65/79.87 (~P1(a6,a1)+P3(a8)+P5(a4)), % 79.65/79.87 inference(scs_inference,[],[10,82,25])). % 79.65/79.87 cnf(85,plain, % 79.65/79.87 (P1(a5,a8)+~E(a6,a1)+P4(a4)), % 79.65/79.87 inference(scs_inference,[],[15,48])). % 79.65/79.87 cnf(89,plain, % 79.65/79.87 (P1(a5,a8)+~E(a6,a2)+P5(a4)), % 79.65/79.87 inference(scs_inference,[],[15,52])). % 79.65/79.87 cnf(90,plain, % 79.65/79.87 (P3(a8)+~E(a6,a2)+P5(a4)), % 79.65/79.87 inference(scs_inference,[],[89,18])). % 79.65/79.87 cnf(91,plain, % 79.65/79.87 (~P1(a6,a2)+P3(a8)+P5(a4)), % 79.65/79.87 inference(scs_inference,[],[11,90,25])). % 79.65/79.87 cnf(93,plain, % 79.65/79.87 (P1(a5,a8)+~E(a6,a2)+P4(a4)), % 79.65/79.87 inference(scs_inference,[],[15,49])). % 79.65/79.87 cnf(97,plain, % 79.65/79.87 (P1(a5,a8)+~E(a9,a6)+P5(a4)), % 79.65/79.87 inference(scs_inference,[],[15,53])). % 79.65/79.87 cnf(100,plain, % 79.65/79.87 (P1(a5,a8)+~E(a9,a6)+P4(a4)), % 79.65/79.87 inference(scs_inference,[],[15,50])). % 79.65/79.87 cnf(103,plain, % 79.65/79.87 (~P1(a8,a5)+~E(a6,a1)+P5(a4)), % 79.65/79.87 inference(scs_inference,[],[15,57])). % 79.65/79.87 cnf(104,plain, % 79.65/79.87 (~P1(a8,a5)+~E(a6,a1)+P4(a4)), % 79.65/79.87 inference(scs_inference,[],[15,54])). % 79.65/79.87 cnf(105,plain, % 79.65/79.87 (~P1(a8,a5)+~E(a6,a2)+P5(a4)), % 79.65/79.87 inference(scs_inference,[],[15,58])). % 79.65/79.87 cnf(106,plain, % 79.65/79.87 (~P1(a8,a5)+~E(a6,a2)+P4(a4)), % 79.65/79.87 inference(scs_inference,[],[15,55])). % 79.65/79.87 cnf(109,plain, % 79.65/79.87 (P1(a5,a8)+P1(a6,a7)+P5(a4)), % 79.65/79.87 inference(scs_inference,[],[15,61])). % 79.65/79.87 cnf(112,plain, % 79.65/79.87 (P1(a5,a8)+P1(a6,a7)+P4(a4)), % 79.65/79.87 inference(scs_inference,[],[15,60])). % 79.65/79.87 cnf(113,plain, % 79.65/79.87 (P3(a8)+P1(a6,a7)+P4(a4)), % 79.65/79.87 inference(scs_inference,[],[112,18])). % 79.65/79.87 cnf(114,plain, % 79.65/79.87 (P3(a7)+P3(a8)+P4(a4)), % 79.65/79.87 inference(scs_inference,[],[113,18])). % 79.65/79.87 cnf(115,plain, % 79.65/79.87 (~P1(a8,a5)+P1(a6,a7)+P5(a4)), % 79.65/79.87 inference(scs_inference,[],[15,63])). % 79.65/79.87 cnf(116,plain, % 79.65/79.87 (~P1(a8,a5)+P1(a6,a7)+P4(a4)), % 79.65/79.87 inference(scs_inference,[],[15,62])). % 79.65/79.87 cnf(123,plain, % 79.65/79.87 (~P5(a4)+P1(a5,a8)+~E(a6,a1)), % 79.65/79.87 inference(scs_inference,[],[17,85])). % 79.65/79.87 cnf(137,plain, % 79.65/79.87 (~P5(a4)+P1(a5,a8)+~E(a6,a2)), % 79.65/79.87 inference(scs_inference,[],[17,93])). % 79.65/79.87 cnf(149,plain, % 79.65/79.87 (~P5(a4)+P1(a5,a8)+~E(a9,a6)), % 79.65/79.87 inference(scs_inference,[],[17,100])). % 79.65/79.87 cnf(158,plain, % 79.65/79.87 (~P5(a4)+~P1(a8,a5)+~E(a6,a1)), % 79.65/79.87 inference(scs_inference,[],[17,104])). % 79.65/79.87 cnf(159,plain, % 79.65/79.87 (~P1(a8,a5)+~E(a6,a1)), % 79.65/79.87 inference(scs_inference,[],[158,103])). % 79.65/79.87 cnf(160,plain, % 79.65/79.87 (~P1(x1601,a5)+~E(x1601,a8)+~E(a6,a1)), % 79.65/79.87 inference(scs_inference,[],[159,4])). % 79.65/79.87 cnf(161,plain, % 79.65/79.87 (~P1(a6,a1)+~E(x1611,a8)+~P1(x1611,a5)), % 79.65/79.87 inference(scs_inference,[],[10,160,25])). % 79.65/79.87 cnf(162,plain, % 79.65/79.87 (~P1(a6,a1)+~P1(a8,a5)), % 79.65/79.87 inference(equality_inference,[],[161])). % 79.65/79.87 cnf(167,plain, % 79.65/79.87 (~P4(a4)+~P1(a8,a5)+~E(a6,a2)), % 79.65/79.87 inference(scs_inference,[],[17,105])). % 79.65/79.87 cnf(168,plain, % 79.65/79.87 (~P1(a8,a5)+~E(a6,a2)), % 79.65/79.87 inference(scs_inference,[],[167,106])). % 79.65/79.87 cnf(169,plain, % 79.65/79.87 (~P1(x1691,a5)+~E(x1691,a8)+~E(a6,a2)), % 79.65/79.87 inference(scs_inference,[],[168,4])). % 79.65/79.87 cnf(170,plain, % 79.65/79.87 (~P1(a6,a2)+~E(x1701,a8)+~P1(x1701,a5)), % 79.65/79.87 inference(scs_inference,[],[11,169,25])). % 79.65/79.87 cnf(171,plain, % 79.65/79.87 (~P1(a6,a2)+~P1(a8,a5)), % 79.65/79.87 inference(equality_inference,[],[170])). % 79.65/79.87 cnf(180,plain, % 79.65/79.87 (~P4(a4)+P1(a5,a8)+P1(a6,a7)), % 79.65/79.87 inference(scs_inference,[],[17,109])). % 79.65/79.87 cnf(181,plain, % 79.65/79.87 (P3(a8)+P1(a6,a7)+~P4(a4)), % 79.65/79.87 inference(scs_inference,[],[180,18])). % 79.65/79.87 cnf(182,plain, % 79.65/79.87 (P3(a7)+P3(a8)+~P4(a4)), % 79.65/79.87 inference(scs_inference,[],[181,18])). % 79.65/79.87 cnf(183,plain, % 79.65/79.87 (P3(a7)+P3(a8)), % 79.65/79.87 inference(scs_inference,[],[182,114])). % 79.65/79.87 cnf(186,plain, % 79.65/79.87 (~P5(a4)+P1(a5,a8)+P1(a6,a7)), % 79.65/79.87 inference(scs_inference,[],[17,112])). % 79.65/79.87 cnf(187,plain, % 79.65/79.87 (P3(a8)+P1(a6,a7)+~P5(a4)), % 79.65/79.87 inference(scs_inference,[],[186,18])). % 79.65/79.87 cnf(188,plain, % 79.65/79.87 (P1(a5,a8)+P1(a6,a7)+P3(a8)), % 79.65/79.87 inference(scs_inference,[],[187,109])). % 79.65/79.87 cnf(189,plain, % 79.65/79.87 (P3(a8)+P1(a6,a7)), % 79.65/79.87 inference(scs_inference,[],[188,18])). % 79.65/79.87 cnf(192,plain, % 79.65/79.87 (~P4(a4)+~P1(a8,a5)+P1(a6,a7)), % 79.65/79.87 inference(scs_inference,[],[17,115])). % 79.65/79.87 cnf(193,plain, % 79.65/79.87 (~P1(a8,a5)+P1(a6,a7)), % 79.65/79.87 inference(scs_inference,[],[192,116])). % 79.65/79.87 cnf(198,plain, % 79.65/79.87 (E(a7,a2)+E(a7,a1)+P3(a8)), % 79.65/79.87 inference(scs_inference,[],[183,16])). % 79.65/79.87 cnf(206,plain, % 79.65/79.87 (P3(a7)+~P1(a8,a5)), % 79.65/79.87 inference(scs_inference,[],[18,193])). % 79.65/79.87 cnf(213,plain, % 79.65/79.87 (P1(a6,x2131)+~E(a7,x2131)+P3(a8)), % 79.65/79.87 inference(scs_inference,[],[189,5])). % 79.65/79.87 cnf(220,plain, % 79.65/79.87 (~P1(a8,a5)+E(a7,a2)+E(a7,a1)), % 79.65/79.87 inference(scs_inference,[],[206,16])). % 79.65/79.87 cnf(221,plain, % 79.65/79.87 (~E(x2211,a1)+P1(x2211,a1)), % 79.65/79.87 inference(scs_inference,[],[2,38])). % 79.65/79.87 cnf(223,plain, % 79.65/79.87 (E(a2,a7)+E(a7,a1)+P3(a8)), % 79.65/79.87 inference(scs_inference,[],[2,198])). % 79.65/79.87 cnf(224,plain, % 79.65/79.87 (P1(a6,a1)+E(a2,a7)+P3(a8)), % 79.65/79.87 inference(scs_inference,[],[223,213])). % 79.65/79.87 cnf(227,plain, % 79.65/79.87 (~E(x2271,a1)+P1(a1,x2271)), % 79.65/79.87 inference(scs_inference,[],[2,41])). % 79.65/79.87 cnf(231,plain, % 79.65/79.87 (~E(x2311,a2)+P1(a2,x2311)), % 79.65/79.87 inference(scs_inference,[],[2,64])). % 79.65/79.87 cnf(235,plain, % 79.65/79.87 (~E(x2351,a2)+P1(x2351,a2)), % 79.65/79.87 inference(scs_inference,[],[2,65])). % 79.65/79.87 cnf(245,plain, % 79.65/79.87 (E(a2,a7)+~P1(a8,a5)+E(a7,a1)), % 79.65/79.87 inference(scs_inference,[],[2,220])). % 79.65/79.87 cnf(247,plain, % 79.65/79.87 (E(a1,a7)+E(a2,a7)+P3(a8)), % 79.65/79.87 inference(scs_inference,[],[2,223])). % 79.65/79.87 cnf(248,plain, % 79.65/79.87 (P1(a7,a2)+E(a1,a7)+P3(a8)), % 79.65/79.87 inference(scs_inference,[],[11,247,4])). % 79.65/79.87 cnf(251,plain, % 79.65/79.87 (E(a7,a2)+P1(a6,a1)+P3(a8)), % 79.65/79.87 inference(scs_inference,[],[2,224])). % 79.65/79.87 cnf(252,plain, % 79.65/79.87 (P1(a6,a2)+P1(a6,a1)+P3(a8)), % 79.65/79.87 inference(scs_inference,[],[251,213])). % 79.65/79.87 cnf(253,plain, % 79.65/79.87 (P1(a6,a1)+P3(a8)+P5(a4)), % 79.65/79.87 inference(scs_inference,[],[252,91])). % 79.65/79.87 cnf(254,plain, % 79.65/79.87 (P3(a8)+P5(a4)), % 79.65/79.87 inference(scs_inference,[],[253,83])). % 79.65/79.87 cnf(267,plain, % 79.65/79.87 (~E(a6,a1)+P1(a5,a8)+P3(a8)), % 79.65/79.87 inference(scs_inference,[],[254,123])). % 79.65/79.87 cnf(268,plain, % 79.65/79.87 (~P1(a6,a1)+P1(a5,a8)+P3(a8)), % 79.65/79.87 inference(scs_inference,[],[10,267,25])). % 79.65/79.87 cnf(269,plain, % 79.65/79.87 (P1(a5,a8)+~E(a7,a1)+P3(a8)), % 79.65/79.87 inference(scs_inference,[],[268,213])). % 79.65/79.87 cnf(270,plain, % 79.65/79.88 (P3(a8)+~E(a7,a1)), % 79.65/79.88 inference(scs_inference,[],[269,18])). % 79.65/79.88 cnf(277,plain, % 79.65/79.88 (~E(a6,a2)+P1(a5,a8)+P3(a8)), % 79.65/79.88 inference(scs_inference,[],[254,137])). % 79.65/79.88 cnf(278,plain, % 79.65/79.88 (~P1(a6,a2)+P1(a5,a8)+P3(a8)), % 79.65/79.88 inference(scs_inference,[],[11,277,25])). % 79.65/79.88 cnf(279,plain, % 79.65/79.88 (P1(a5,a8)+~E(a2,a6)+P3(a8)), % 79.65/79.88 inference(scs_inference,[],[278,65])). % 79.65/79.88 cnf(280,plain, % 79.65/79.88 (P3(a8)+~E(a2,a6)), % 79.65/79.88 inference(scs_inference,[],[279,18])). % 79.65/79.88 cnf(281,plain, % 79.65/79.88 (~E(a6,a2)+P3(a8)), % 79.65/79.88 inference(scs_inference,[],[280,2])). % 79.65/79.88 cnf(282,plain, % 79.65/79.88 (~P1(a6,a2)+P3(a8)), % 79.65/79.88 inference(scs_inference,[],[11,281,25])). % 79.65/79.88 cnf(283,plain, % 79.65/79.88 (~E(a7,a2)+P3(a8)), % 79.65/79.88 inference(scs_inference,[],[282,213])). % 79.65/79.88 cnf(284,plain, % 79.65/79.88 (~E(a2,a7)+P3(a8)), % 79.65/79.88 inference(scs_inference,[],[283,2])). % 79.65/79.88 cnf(285,plain, % 79.65/79.88 (~P1(a7,a2)+P3(a8)), % 79.65/79.88 inference(scs_inference,[],[11,284,25])). % 79.65/79.88 cnf(286,plain, % 79.65/79.88 (E(a1,a7)+P3(a8)), % 79.65/79.88 inference(scs_inference,[],[285,248])). % 79.65/79.88 cnf(297,plain, % 79.65/79.88 (~E(a1,a7)+P3(a8)), % 79.65/79.88 inference(scs_inference,[],[270,2])). % 79.65/79.88 cnf(298,plain, % 79.65/79.88 (P3(a8)), % 79.65/79.88 inference(scs_inference,[],[297,286])). % 79.65/79.88 cnf(299,plain, % 79.65/79.88 (~E(x2991,a8)+P3(x2991)), % 79.65/79.88 inference(scs_inference,[],[298,2,8])). % 79.65/79.88 cnf(301,plain, % 79.65/79.88 (E(x3011,a2)+E(x3011,a1)+~E(x3011,a8)), % 79.65/79.88 inference(scs_inference,[],[299,16])). % 79.65/79.88 cnf(302,plain, % 79.65/79.88 (E(a8,a1)+E(a8,a2)), % 79.65/79.88 inference(equality_inference,[],[301])). % 79.65/79.88 cnf(303,plain, % 79.65/79.88 (E(a8,a2)+P1(a8,a1)), % 79.65/79.88 inference(scs_inference,[],[302,221])). % 79.65/79.88 cnf(308,plain, % 79.65/79.88 (E(a2,a8)+E(a8,a1)), % 79.65/79.88 inference(scs_inference,[],[2,302])). % 79.65/79.88 cnf(319,plain, % 79.65/79.88 (E(a1,a8)+E(a8,a2)), % 79.65/79.88 inference(scs_inference,[],[2,302])). % 79.65/79.88 cnf(328,plain, % 79.65/79.88 (E(a2,a8)+P1(a8,a1)), % 79.65/79.88 inference(scs_inference,[],[2,303])). % 79.65/79.88 cnf(341,plain, % 79.65/79.88 (E(a1,a8)+E(a2,a8)), % 79.65/79.88 inference(scs_inference,[],[2,308])). % 79.65/79.88 cnf(345,plain, % 79.65/79.88 (~E(a8,x3451)+E(x3451,a1)+E(x3451,a2)), % 79.65/79.88 inference(scs_inference,[],[2,301])). % 79.65/79.88 cnf(347,plain, % 79.65/79.88 (E(a2,x3471)+E(x3471,a1)+~E(x3471,a8)), % 79.65/79.88 inference(scs_inference,[],[2,301])). % 79.65/79.88 cnf(385,plain, % 79.65/79.88 (~P1(a1,a2)+P1(a2,a1)), % 79.65/79.88 inference(scs_inference,[],[11,38,25])). % 79.65/79.88 cnf(386,plain, % 79.65/79.88 (P1(x3861,a1)+~E(a2,x3861)+~P1(a1,a2)), % 79.65/79.88 inference(scs_inference,[],[385,4])). % 79.65/79.88 cnf(418,plain, % 79.65/79.88 (~E(a1,a2)+~E(a2,x4181)+P1(x4181,a1)), % 79.65/79.88 inference(scs_inference,[],[41,386])). % 79.65/79.88 cnf(419,plain, % 79.65/79.88 (~E(a1,a2)+P1(a8,a1)), % 79.65/79.88 inference(scs_inference,[],[418,328])). % 79.65/79.88 cnf(420,plain, % 79.65/79.88 (~E(a2,a1)+P1(a8,a1)), % 79.65/79.88 inference(scs_inference,[],[419,2])). % 79.65/79.88 cnf(421,plain, % 79.65/79.88 (~P1(a2,a1)+P1(a8,a1)), % 79.65/79.88 inference(scs_inference,[],[10,420,25])). % 79.65/79.88 cnf(424,plain, % 79.65/79.88 (E(a2,a8)+P1(a1,a8)), % 79.65/79.88 inference(scs_inference,[],[41,341])). % 79.65/79.88 cnf(428,plain, % 79.65/79.88 (P1(x4281,x4282)+~E(a1,x4281)+~E(a1,x4282)), % 79.65/79.88 inference(scs_inference,[],[41,4])). % 79.65/79.88 cnf(429,plain, % 79.65/79.88 (~E(x4291,x4292)+~E(x4292,a2)+P1(a2,x4291)), % 79.65/79.88 inference(scs_inference,[],[64,71])). % 79.65/79.88 cnf(454,plain, % 79.65/79.88 (E(a1,a8)+P1(a2,a8)), % 79.65/79.88 inference(scs_inference,[],[64,341])). % 79.65/79.88 cnf(455,plain, % 79.65/79.88 (P1(a8,a8)+P1(a2,a8)), % 79.65/79.88 inference(scs_inference,[],[454,428])). % 79.65/79.88 cnf(456,plain, % 79.65/79.88 (P1(x4561,a8)+~E(a2,x4561)+P1(a8,a8)), % 79.65/79.88 inference(scs_inference,[],[455,4])). % 79.65/79.88 cnf(533,plain, % 79.65/79.88 (~P1(a2,a1)+P1(a1,a2)), % 79.65/79.88 inference(scs_inference,[],[10,65,25])). % 79.65/79.88 cnf(536,plain, % 79.65/79.88 (~P1(a8,a5)+E(a7,a1)+P1(a7,a2)), % 79.65/79.88 inference(scs_inference,[],[65,245])). % 79.65/79.88 cnf(540,plain, % 79.65/79.88 (~E(a2,a1)+~E(a2,x5401)+P1(x5401,a1)), % 79.65/79.88 inference(scs_inference,[],[65,386])). % 79.65/79.88 cnf(541,plain, % 79.65/79.88 (E(x5411,a1)+~E(a2,a1)+~E(a2,x5411)), % 79.65/79.88 inference(scs_inference,[],[10,540,25])). % 79.65/79.88 cnf(573,plain, % 79.65/79.88 (~P1(a6,x5731)+~E(x5731,a1)+~P1(a8,a5)), % 79.65/79.88 inference(scs_inference,[],[162,5])). % 79.65/79.88 cnf(578,plain, % 79.65/79.88 (~P1(a6,x5781)+~E(x5781,a2)+~P1(a8,a5)), % 79.65/79.88 inference(scs_inference,[],[171,5])). % 79.65/79.88 cnf(595,plain, % 79.65/79.88 (~P1(a8,a5)+~E(a7,a1)), % 79.65/79.88 inference(scs_inference,[],[193,573])). % 79.65/79.88 cnf(612,plain, % 79.65/79.88 (~P1(a8,a5)+~E(a7,a2)), % 79.65/79.88 inference(scs_inference,[],[193,578])). % 79.65/79.88 cnf(613,plain, % 79.65/79.88 (~P1(a8,x6131)+~E(x6131,a5)+~E(a7,a2)), % 79.65/79.88 inference(scs_inference,[],[612,5])). % 79.65/79.88 cnf(614,plain, % 79.65/79.88 (~P1(a7,a2)+~E(x6141,a5)+~P1(a8,x6141)), % 79.65/79.88 inference(scs_inference,[],[11,613,25])). % 79.65/79.88 cnf(615,plain, % 79.65/79.88 (~P1(a7,a2)+~P1(a8,a5)), % 79.65/79.88 inference(equality_inference,[],[614])). % 79.65/79.88 cnf(650,plain, % 79.65/79.88 (P1(x6501,a1)+E(x6501,a2)+~E(a8,x6501)), % 79.65/79.88 inference(scs_inference,[],[221,345])). % 79.65/79.88 cnf(678,plain, % 79.65/79.88 (~P1(a8,a5)+P1(a7,a2)+P1(a7,a1)), % 79.65/79.88 inference(scs_inference,[],[221,536])). % 79.65/79.88 cnf(679,plain, % 79.65/79.88 (P1(a7,a1)+~P1(a8,a5)), % 79.65/79.88 inference(scs_inference,[],[678,615])). % 79.65/79.88 cnf(818,plain, % 79.65/79.88 (P1(a1,x8181)+~E(x8181,a8)+E(a2,x8181)), % 79.65/79.88 inference(scs_inference,[],[227,347])). % 79.65/79.88 cnf(833,plain, % 79.65/79.88 (P1(x8331,x8332)+~E(a1,x8331)+~E(x8332,a1)), % 79.65/79.88 inference(scs_inference,[],[227,4])). % 79.65/79.88 cnf(844,plain, % 79.65/79.88 (~E(a2,a1)+P1(a1,x8441)+~E(a2,x8441)), % 79.65/79.88 inference(scs_inference,[],[227,541])). % 79.65/79.88 cnf(845,plain, % 79.65/79.88 (~E(a2,a1)+~E(x8451,a8)+P1(a1,x8451)), % 79.65/79.88 inference(scs_inference,[],[844,818])). % 79.65/79.88 cnf(846,plain, % 79.65/79.88 (~P1(a2,a1)+P1(a1,x8461)+~E(x8461,a8)), % 79.65/79.88 inference(scs_inference,[],[10,845,25])). % 79.65/79.88 cnf(954,plain, % 79.65/79.88 (P1(x9541,a2)+~E(a8,x9541)+P1(x9541,a1)), % 79.65/79.88 inference(scs_inference,[],[235,650])). % 79.65/79.88 cnf(1463,plain, % 79.65/79.88 (E(a8,a1)+P1(a8,a8)), % 79.65/79.88 inference(scs_inference,[],[308,456])). % 79.65/79.88 cnf(1472,plain, % 79.65/79.88 (~E(a2,a1)+E(a8,a1)), % 79.65/79.88 inference(scs_inference,[],[308,541])). % 79.65/79.88 cnf(1473,plain, % 79.65/79.88 (~E(a1,a2)+E(a8,a1)), % 79.65/79.88 inference(scs_inference,[],[1472,2])). % 79.65/79.88 cnf(1474,plain, % 79.65/79.88 (~P1(a1,a2)+E(a8,a1)), % 79.65/79.88 inference(scs_inference,[],[11,1473,25])). % 79.65/79.88 cnf(1475,plain, % 79.65/79.88 (E(a8,a1)+~P1(a2,a1)), % 79.65/79.88 inference(scs_inference,[],[1474,533])). % 79.65/79.88 cnf(1476,plain, % 79.65/79.88 (~E(a1,x14761)+E(a8,a1)+~E(x14761,a2)), % 79.65/79.88 inference(scs_inference,[],[1475,429])). % 79.65/79.88 cnf(1490,plain, % 79.65/79.88 (P1(a8,a8)+E(a8,a2)), % 79.65/79.88 inference(scs_inference,[],[319,428])). % 79.65/79.88 cnf(1616,plain, % 79.65/79.88 (P1(a8,x16161)+E(a8,a2)+~E(x16161,a1)), % 79.65/79.88 inference(scs_inference,[],[319,833])). % 79.65/79.88 cnf(1982,plain, % 79.65/79.88 (P1(a8,a1)+~P1(a1,a2)), % 79.65/79.88 inference(scs_inference,[],[385,421])). % 79.65/79.88 cnf(2303,plain, % 79.65/79.88 (P1(a1,a8)+P1(a8,a8)), % 79.65/79.88 inference(scs_inference,[],[424,456])). % 79.65/79.88 cnf(2320,plain, % 79.65/79.88 (P1(a2,x23201)+~E(a8,x23201)+P1(a8,a8)), % 79.65/79.88 inference(scs_inference,[],[455,5])). % 79.65/79.88 cnf(2474,plain, % 79.65/79.88 (~E(a1,a7)+~P1(a8,a5)), % 79.65/79.88 inference(scs_inference,[],[595,2])). % 79.65/79.88 cnf(2475,plain, % 79.65/79.88 (~P1(x24751,a5)+~E(x24751,a8)+~E(a1,a7)), % 79.65/79.88 inference(scs_inference,[],[2474,4])). % 79.65/79.88 cnf(2476,plain, % 79.65/79.88 (~P1(a7,a1)+~E(x24761,a8)+~P1(x24761,a5)), % 79.65/79.88 inference(scs_inference,[],[10,2475,25])). % 79.65/79.88 cnf(2477,plain, % 79.65/79.88 (~P1(a7,a1)+~P1(a8,a5)), % 79.65/79.88 inference(equality_inference,[],[2476])). % 79.65/79.88 cnf(2478,plain, % 79.65/79.88 (~P1(a8,a5)), % 79.65/79.88 inference(scs_inference,[],[2477,679])). % 79.65/79.88 cnf(2479,plain, % 79.65/79.88 (~E(a1,a5)+~E(a1,a8)), % 79.65/79.88 inference(scs_inference,[],[2478,428])). % 79.65/79.88 cnf(2480,plain, % 79.65/79.88 (~P1(a5,a1)+~E(a1,a8)), % 79.65/79.88 inference(scs_inference,[],[2478,10,428,25])). % 79.65/79.88 cnf(2488,plain, % 79.65/79.88 (P1(a8,a2)+~E(a5,a1)), % 79.65/79.88 inference(scs_inference,[],[2478,1616,231,235])). % 79.65/79.88 cnf(2491,plain, % 79.65/79.88 (~P1(a8,x24911)+~E(x24911,a5)), % 79.65/79.88 inference(scs_inference,[],[2478,5])). % 79.65/79.88 cnf(2500,plain, % 79.65/79.88 (~E(a5,a1)+~E(a2,a5)), % 79.65/79.88 inference(scs_inference,[],[2488,2491])). % 79.65/79.88 cnf(2507,plain, % 79.65/79.88 (~E(a5,a1)+~E(a5,a2)), % 79.65/79.88 inference(scs_inference,[],[2500,2])). % 79.65/79.88 cnf(2511,plain, % 79.65/79.88 (~E(a5,a2)+~E(a1,a5)), % 79.65/79.88 inference(scs_inference,[],[2507,2])). % 79.65/79.88 cnf(2515,plain, % 79.65/79.88 (~E(a1,a5)+~P1(a5,a2)), % 79.65/79.88 inference(scs_inference,[],[11,2511,25])). % 79.65/79.88 cnf(2518,plain, % 79.65/79.88 (~P1(a5,a2)+~E(a5,a1)), % 79.65/79.88 inference(scs_inference,[],[2515,2])). % 79.65/79.88 cnf(2521,plain, % 79.65/79.88 (~E(a5,a1)+~E(a1,a2)+~E(a1,a5)), % 79.65/79.88 inference(scs_inference,[],[2518,428])). % 79.65/79.88 cnf(2535,plain, % 79.65/79.88 (~E(a1,a2)+~E(a1,a5)+~P1(a5,a1)), % 79.65/79.88 inference(scs_inference,[],[10,2521,25])). % 79.65/79.88 cnf(2537,plain, % 79.65/79.88 (~E(a1,a2)+~E(a1,a5)), % 79.65/79.88 inference(scs_inference,[],[2535,428])). % 79.65/79.88 cnf(2538,plain, % 79.65/79.88 (~E(a1,a2)+~E(a5,a1)), % 79.65/79.88 inference(scs_inference,[],[2537,2])). % 79.65/79.88 cnf(2539,plain, % 79.65/79.88 (~E(a1,a2)+~P1(a5,a1)), % 79.65/79.88 inference(scs_inference,[],[10,2538,25])). % 79.65/79.88 cnf(2540,plain, % 79.65/79.88 (~E(a1,a2)+~P1(a5,x25401)+~E(x25401,a1)), % 79.65/79.88 inference(scs_inference,[],[2539,5])). % 79.65/79.88 cnf(2569,plain, % 79.65/79.88 (E(a8,a1)+~E(a8,a5)), % 79.65/79.88 inference(scs_inference,[],[1463,2491])). % 79.65/79.88 cnf(2570,plain, % 79.65/79.88 (E(a8,a1)+~E(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[2569,2])). % 79.65/79.88 cnf(2577,plain, % 79.65/79.88 (P1(a8,a8)+P1(a2,a1)), % 79.65/79.88 inference(scs_inference,[],[1463,2320])). % 79.65/79.88 cnf(2578,plain, % 79.65/79.88 (P1(a1,a2)+P1(a8,a8)), % 79.65/79.88 inference(scs_inference,[],[2577,533])). % 79.65/79.88 cnf(2587,plain, % 79.65/79.88 (~E(a1,a2)+P1(a8,a8)+~P1(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[1463,2540])). % 79.65/79.88 cnf(2588,plain, % 79.65/79.88 (~P1(a2,a1)+P1(a8,a8)+~P1(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[10,2587,25])). % 79.65/79.88 cnf(2589,plain, % 79.65/79.88 (P1(a8,a8)+~P1(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[2588,2577])). % 79.65/79.88 cnf(2590,plain, % 79.65/79.88 (P1(a8,a8)+~E(a2,a5)), % 79.65/79.88 inference(scs_inference,[],[2589,456])). % 79.65/79.88 cnf(2591,plain, % 79.65/79.88 (~E(a5,a2)+P1(a8,a8)), % 79.65/79.88 inference(scs_inference,[],[2590,2])). % 79.65/79.88 cnf(2629,plain, % 79.65/79.88 (~E(a2,a1)+~E(a1,a2)+~P1(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[1472,2540])). % 79.65/79.88 cnf(2630,plain, % 79.65/79.88 (~E(a2,a1)+~P1(a2,a1)+~P1(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[10,2629,25])). % 79.65/79.88 cnf(2631,plain, % 79.65/79.88 (~P1(a1,a2)+~P1(a2,a1)+~P1(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[11,2630,25])). % 79.65/79.88 cnf(2632,plain, % 79.65/79.88 (~P1(a2,a1)+~P1(a5,a8)+~E(a2,a8)), % 79.65/79.88 inference(scs_inference,[],[2631,846])). % 79.65/79.88 cnf(2633,plain, % 79.65/79.88 (~P1(a8,a2)+~P1(a2,a1)+~P1(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[11,2632,25])). % 79.65/79.88 cnf(2634,plain, % 79.65/79.88 (~P1(a8,a2)+~P1(a5,a8)+~E(a1,a2)), % 79.65/79.88 inference(scs_inference,[],[2633,38])). % 79.65/79.88 cnf(2635,plain, % 79.65/79.88 (~P1(a5,a8)+~E(a1,a2)+~E(a1,a8)), % 79.65/79.88 inference(scs_inference,[],[2634,428])). % 79.65/79.88 cnf(2636,plain, % 79.65/79.88 (~E(a1,a2)+~P1(a8,a1)+~P1(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[10,2635,25])). % 79.65/79.88 cnf(2637,plain, % 79.65/79.88 (~P1(a2,a1)+~P1(a8,a1)+~P1(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[10,2636,25])). % 79.65/79.88 cnf(2638,plain, % 79.65/79.88 (~P1(a8,a1)+~P1(a5,a8)+~E(a2,a1)), % 79.65/79.88 inference(scs_inference,[],[2637,64])). % 79.65/79.88 cnf(2639,plain, % 79.65/79.88 (~P1(a1,a2)+~P1(a8,a1)+~P1(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[11,2638,25])). % 79.65/79.88 cnf(2640,plain, % 79.65/79.88 (~P1(a1,a2)+~P1(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[2639,1982])). % 79.65/79.88 cnf(2669,plain, % 79.65/79.88 (E(a8,a2)+~E(a8,a5)), % 79.65/79.88 inference(scs_inference,[],[1490,2491])). % 79.65/79.88 cnf(2795,plain, % 79.65/79.88 (~E(a1,a5)+~E(a8,x27951)+~E(x27951,a1)), % 79.65/79.88 inference(scs_inference,[],[2479,71])). % 79.65/79.88 cnf(2796,plain, % 79.65/79.88 (~P1(a5,a1)+~E(x27961,a1)+~E(a8,x27961)), % 79.65/79.88 inference(scs_inference,[],[10,2795,25])). % 79.65/79.88 cnf(2797,plain, % 79.65/79.88 (~E(a8,x27971)+~E(x27971,a1)+~E(a5,a1)), % 79.65/79.88 inference(scs_inference,[],[2796,221])). % 79.65/79.88 cnf(2798,plain, % 79.65/79.88 (~E(a1,x27981)+~E(x27981,a5)+~E(a8,a5)), % 79.65/79.88 inference(scs_inference,[],[2797,71])). % 79.65/79.88 cnf(2799,plain, % 79.65/79.88 (~E(a5,a8)+~E(a1,a8)), % 79.65/79.88 inference(scs_inference,[],[2798,2])). % 79.65/79.88 cnf(2800,plain, % 79.65/79.88 (~E(a5,a8)+E(a2,a8)), % 79.65/79.88 inference(scs_inference,[],[2799,341])). % 79.65/79.88 cnf(2801,plain, % 79.65/79.88 (~E(a8,a5)+E(a2,a8)), % 79.65/79.88 inference(scs_inference,[],[2800,2])). % 79.65/79.88 cnf(2802,plain, % 79.65/79.88 (~P1(a5,x28021)+~P1(a8,x28021)+E(a2,a8)), % 79.65/79.88 inference(scs_inference,[],[2801,25])). % 79.65/79.88 cnf(2803,plain, % 79.65/79.88 (~P1(a2,a5)+~P1(a8,x28031)+~P1(a5,x28031)), % 79.65/79.88 inference(scs_inference,[],[2478,2802,4])). % 79.65/79.88 cnf(2804,plain, % 79.65/79.88 (~P1(a5,x28041)+~E(a2,a5)+~P1(a8,x28041)), % 79.65/79.88 inference(scs_inference,[],[2803,64])). % 79.65/79.88 cnf(2805,plain, % 79.65/79.88 (~P1(a5,a2)+~P1(a8,x28051)+~P1(a5,x28051)), % 79.65/79.88 inference(scs_inference,[],[11,2804,25])). % 79.65/79.88 cnf(2806,plain, % 79.65/79.88 (~P1(a8,a2)+~E(a5,a2)), % 79.65/79.88 inference(scs_inference,[],[2805,235])). % 79.65/79.88 cnf(2807,plain, % 79.65/79.88 (~P1(a5,a2)+~P1(a8,a2)), % 79.65/79.88 inference(scs_inference,[],[11,2806,25])). % 79.65/79.88 cnf(2808,plain, % 79.65/79.88 (~P1(a5,a2)+~E(a2,a8)), % 79.65/79.88 inference(scs_inference,[],[2807,65])). % 79.65/79.88 cnf(2809,plain, % 79.65/79.88 (~P1(a5,a2)+E(a1,a8)), % 79.65/79.88 inference(scs_inference,[],[2808,341])). % 79.65/79.88 cnf(2824,plain, % 79.65/79.88 (~P1(a5,a1)+~E(a8,a1)), % 79.65/79.88 inference(scs_inference,[],[2480,2])). % 79.65/79.88 cnf(2825,plain, % 79.65/79.88 (~P1(a5,a1)+~E(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[2824,2570])). % 79.65/79.88 cnf(2826,plain, % 79.65/79.88 (~E(a5,a8)+~E(a5,x28261)+~E(x28261,a1)), % 79.65/79.88 inference(scs_inference,[],[2825,73])). % 79.65/79.88 cnf(2844,plain, % 79.65/79.88 (~E(x28441,a2)+~E(a1,x28441)+~E(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[1476,2826])). % 79.65/79.88 cnf(2869,plain, % 79.65/79.88 (~E(a8,a5)+~E(a1,x28691)+~E(x28691,a2)), % 79.65/79.88 inference(scs_inference,[],[2844,2])). % 79.65/79.88 cnf(2892,plain, % 79.65/79.88 (~E(a8,a5)+~E(a1,a8)), % 79.65/79.88 inference(scs_inference,[],[2869,2669])). % 79.65/79.88 cnf(2893,plain, % 79.65/79.88 (~E(a8,a5)+~P1(a5,a2)), % 79.65/79.88 inference(scs_inference,[],[2892,2809])). % 79.65/79.88 cnf(2894,plain, % 79.65/79.88 (~E(a8,a5)+~E(a2,a5)), % 79.65/79.88 inference(scs_inference,[],[2893,65])). % 79.65/79.88 cnf(2895,plain, % 79.65/79.88 (~E(a8,a5)+~E(a5,a2)), % 79.65/79.88 inference(scs_inference,[],[2894,2])). % 79.65/79.88 cnf(2896,plain, % 79.65/79.88 (~E(a8,a5)+~E(a2,x28961)+~E(x28961,a5)), % 79.65/79.88 inference(scs_inference,[],[2895,71])). % 79.65/79.88 cnf(2919,plain, % 79.65/79.88 (~E(a5,a8)+~E(a2,a8)), % 79.65/79.88 inference(scs_inference,[],[2896,2])). % 79.65/79.88 cnf(2920,plain, % 79.65/79.88 (~E(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[2919,2800])). % 79.65/79.88 cnf(2921,plain, % 79.65/79.88 (~E(a8,a5)), % 79.65/79.88 inference(scs_inference,[],[2920,2])). % 79.65/79.88 cnf(2932,plain, % 79.65/79.88 (~P1(a5,a8)), % 79.65/79.88 inference(scs_inference,[],[2921,25,1463,1490,2303,2578,2591,2640])). % 79.65/79.88 cnf(2935,plain, % 79.65/79.88 (~E(a6,a1)+P5(a4)), % 79.65/79.88 inference(scs_inference,[],[2932,81])). % 79.65/79.88 cnf(2937,plain, % 79.65/79.88 (~E(a6,a2)+P5(a4)), % 79.65/79.88 inference(scs_inference,[],[2932,89])). % 79.65/79.88 cnf(2939,plain, % 79.65/79.88 (~E(a9,a6)+P5(a4)), % 79.65/79.88 inference(scs_inference,[],[2932,97])). % 79.65/79.88 cnf(2941,plain, % 79.65/79.88 (P1(a6,a7)+P5(a4)), % 79.65/79.88 inference(scs_inference,[],[2932,109])). % 79.65/79.88 cnf(2943,plain, % 79.65/79.88 (~E(a6,a1)+~P5(a4)), % 79.65/79.88 inference(scs_inference,[],[2932,123])). % 79.65/79.88 cnf(2945,plain, % 79.65/79.88 (~E(a6,a2)+~P5(a4)), % 79.65/79.88 inference(scs_inference,[],[2932,137])). % 79.65/79.88 cnf(2947,plain, % 79.65/79.88 (~E(a9,a6)+~P5(a4)), % 79.65/79.88 inference(scs_inference,[],[2932,149])). % 79.65/79.88 cnf(2950,plain, % 79.65/79.88 (P1(a6,a7)+~P5(a4)), % 79.65/79.88 inference(scs_inference,[],[2932,186])). % 79.65/79.88 cnf(2967,plain, % 79.65/79.88 (~E(a2,a6)+P5(a4)), % 79.65/79.88 inference(scs_inference,[],[2937,2])). % 79.65/79.88 cnf(2971,plain, % 79.65/79.88 (P3(a7)+P5(a4)), % 79.65/79.88 inference(scs_inference,[],[2941,18])). % 79.65/79.88 cnf(2978,plain, % 79.65/79.88 (~E(a2,a6)+~P5(a4)), % 79.65/79.88 inference(scs_inference,[],[2945,2])). % 79.65/79.88 cnf(2980,plain, % 79.65/79.88 (~E(a6,a9)+~P5(a4)), % 79.65/79.88 inference(scs_inference,[],[2947,2])). % 79.65/79.88 cnf(2987,plain, % 79.65/79.88 (~P1(a6,a2)+P5(a4)), % 79.65/79.88 inference(scs_inference,[],[11,2967,25])). % 79.65/79.88 cnf(2993,plain, % 79.65/79.88 (~P1(a6,a2)+~P5(a4)), % 79.65/79.88 inference(scs_inference,[],[11,2978,25])). % 79.65/79.88 cnf(2995,plain, % 79.65/79.88 (~E(x29951,a9)+~E(a6,x29951)+~P5(a4)), % 79.65/79.88 inference(scs_inference,[],[2980,3])). % 79.65/79.88 cnf(3008,plain, % 79.65/79.88 (~P1(a6,x30081)+~E(x30081,a2)+~P5(a4)), % 79.65/79.88 inference(scs_inference,[],[2993,5])). % 79.65/79.88 cnf(3120,plain, % 79.65/79.88 (P1(a6,a7)+P3(a7)), % 79.65/79.88 inference(scs_inference,[],[2971,2950])). % 79.65/79.88 cnf(3121,plain, % 79.65/79.88 (P3(a7)), % 79.65/79.88 inference(scs_inference,[],[3120,18])). % 79.65/79.88 cnf(3135,plain, % 79.65/79.88 (~E(a6,a1)), % 79.65/79.88 inference(scs_inference,[],[2935,2943])). % 79.65/79.88 cnf(3137,plain, % 79.65/79.88 (~P1(a6,a1)), % 79.65/79.88 inference(scs_inference,[],[3135,10,2,25])). % 79.65/79.88 cnf(3183,plain, % 79.65/79.88 (~E(a8,a6)), % 79.65/79.88 inference(scs_inference,[],[3137,954,5,2987,2993,2995,3008])). % 79.65/79.88 cnf(3214,plain, % 79.65/79.88 (~P1(a6,x32141)+~E(x32141,a1)), % 79.65/79.88 inference(scs_inference,[],[3137,5])). % 79.65/79.88 cnf(3230,plain, % 79.65/79.88 (~E(a7,a6)+E(a6,a2)), % 79.65/79.88 inference(scs_inference,[],[3121,3135,16,8])). % 79.65/79.88 cnf(3357,plain, % 79.65/79.88 (~E(a6,a2)), % 79.65/79.88 inference(scs_inference,[],[2937,2945])). % 79.65/79.88 cnf(3359,plain, % 79.65/79.88 (~E(a7,a6)), % 79.65/79.88 inference(scs_inference,[],[3357,3230])). % 79.65/79.88 cnf(3361,plain, % 79.65/79.88 (~P1(a6,a2)), % 79.65/79.89 inference(scs_inference,[],[3357,11,2,25])). % 79.65/79.89 cnf(3378,plain, % 79.65/79.89 (~P1(a6,x33781)+~P1(a7,x33781)), % 79.65/79.89 inference(scs_inference,[],[3359,25])). % 79.65/79.89 cnf(3388,plain, % 79.65/79.89 (~E(a9,a6)), % 79.65/79.89 inference(scs_inference,[],[2939,2947])). % 79.65/79.89 cnf(3389,plain, % 79.65/79.89 (~E(a6,a9)), % 79.65/79.89 inference(scs_inference,[],[3388,2])). % 79.65/79.89 cnf(3394,plain, % 79.65/79.89 (~P1(a9,x33941)+~P1(a6,x33941)), % 79.65/79.89 inference(scs_inference,[],[3389,25])). % 79.65/79.89 cnf(3408,plain, % 79.65/79.89 (P1(a6,a7)), % 79.65/79.89 inference(scs_inference,[],[2941,2950])). % 79.65/79.89 cnf(3421,plain, % 79.65/79.89 ($false), % 79.65/79.89 inference(scs_inference,[],[3408,3361,3183,3121,3214,3378,3394,2,16,71,25,5]), % 79.65/79.89 ['proof']). % 79.65/79.89 % SZS output end Proof % 79.65/79.89 % Total time :79.110000s %------------------------------------------------------------------------------