%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS140+1 : TPTP v8.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n019.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 1.86s 1.96s % Output : CNFRefutation 1.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS140+1 : TPTP v8.2.0. Released v3.1.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n019.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Jun 19 13:55:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.48/0.57 start to proof:theBenchmark % 1.86/1.94 %------------------------------------------- % 1.86/1.94 % File :CSE---1.7 % 1.86/1.94 % Problem :theBenchmark % 1.86/1.94 % Transform :cnf % 1.86/1.94 % Format :tptp:raw % 1.86/1.94 % Command :java -jar mcs_scs.jar %d %s % 1.86/1.94 % 1.86/1.94 % Result :Theorem 1.340000s % 1.86/1.94 % Output :CNFRefutation 1.340000s % 1.86/1.94 %------------------------------------------- % 1.86/1.95 %------------------------------------------------------------------------------ % 1.86/1.95 % File : KRS140+1 : TPTP v8.2.0. Released v3.1.0. % 1.86/1.95 % Domain : Knowledge Representation (Semantic Web) % 1.86/1.95 % Problem : Test illustrating extensional semantics of owl:TransitiveProperty % 1.86/1.95 % Version : Especial. % 1.86/1.95 % English : % 1.86/1.95 % 1.86/1.95 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 1.86/1.95 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 1.86/1.95 % Source : [Bec03] % 1.86/1.95 % Names : positive_TransitiveProperty-Manifest002 [Bec03] % 1.86/1.95 % 1.86/1.95 % Status : Theorem % 1.86/1.95 % Rating : 0.00 v6.1.0, 0.17 v6.0.0, 0.00 v5.5.0, 0.11 v5.4.0, 0.00 v5.3.0, 0.09 v5.2.0, 0.00 v4.1.0, 0.04 v4.0.1, 0.09 v4.0.0, 0.12 v3.7.0, 0.00 v3.1.0 % 1.86/1.95 % Syntax : Number of formulae : 15 ( 4 unt; 0 def) % 1.86/1.95 % Number of atoms : 40 ( 8 equ) % 1.86/1.95 % Maximal formula atoms : 9 ( 2 avg) % 1.86/1.95 % Number of connectives : 29 ( 4 ~; 1 |; 13 &) % 1.86/1.95 % ( 2 <=>; 9 =>; 0 <=; 0 <~>) % 1.86/1.95 % Maximal formula depth : 9 ( 4 avg) % 1.86/1.95 % Maximal term depth : 1 ( 1 avg) % 1.86/1.95 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty) % 1.86/1.95 % Number of functors : 2 ( 2 usr; 2 con; 0-0 aty) % 1.86/1.95 % Number of variables : 26 ( 25 !; 1 ?) % 1.86/1.95 % SPC : FOF_THM_EPR_SEQ % 1.86/1.95 % 1.86/1.95 % Comments : Sean Bechhofer says there are some errors in the encoding of % 1.86/1.95 % datatypes, so this problem may not be perfect. At least it's % 1.86/1.95 % still representative of the type of reasoning required for OWL. % 1.86/1.95 %------------------------------------------------------------------------------ % 1.86/1.95 fof(cowlNothing_substitution_1,axiom, % 1.86/1.95 ! [A,B] : % 1.86/1.95 ( ( A = B % 1.86/1.95 & cowlNothing(A) ) % 1.86/1.95 => cowlNothing(B) ) ). % 1.86/1.95 % 1.86/1.95 fof(cowlThing_substitution_1,axiom, % 1.86/1.95 ! [A,B] : % 1.86/1.95 ( ( A = B % 1.86/1.95 & cowlThing(A) ) % 1.86/1.95 => cowlThing(B) ) ). % 1.86/1.95 % 1.86/1.95 fof(rsymProp_substitution_1,axiom, % 1.86/1.95 ! [A,B,C] : % 1.86/1.95 ( ( A = B % 1.86/1.95 & rsymProp(A,C) ) % 1.86/1.95 => rsymProp(B,C) ) ). % 1.86/1.95 % 1.86/1.95 fof(rsymProp_substitution_2,axiom, % 1.86/1.95 ! [A,B,C] : % 1.86/1.95 ( ( A = B % 1.86/1.95 & rsymProp(C,A) ) % 1.86/1.95 => rsymProp(C,B) ) ). % 1.86/1.95 % 1.86/1.95 fof(xsd_integer_substitution_1,axiom, % 1.86/1.95 ! [A,B] : % 1.86/1.95 ( ( A = B % 1.86/1.95 & xsd_integer(A) ) % 1.86/1.95 => xsd_integer(B) ) ). % 1.86/1.95 % 1.86/1.95 fof(xsd_string_substitution_1,axiom, % 1.86/1.95 ! [A,B] : % 1.86/1.95 ( ( A = B % 1.86/1.95 & xsd_string(A) ) % 1.86/1.95 => xsd_string(B) ) ). % 1.86/1.95 % 1.86/1.95 %----Thing and Nothing % 1.86/1.95 fof(axiom_0,axiom, % 1.86/1.95 ! [X] : % 1.86/1.95 ( cowlThing(X) % 1.86/1.95 & ~ cowlNothing(X) ) ). % 1.86/1.95 % 1.86/1.95 %----String and Integer disjoint % 1.86/1.95 fof(axiom_1,axiom, % 1.86/1.95 ! [X] : % 1.86/1.95 ( xsd_string(X) % 1.86/1.95 <=> ~ xsd_integer(X) ) ). % 1.86/1.95 % 1.86/1.95 %----Range: rsymProp % 1.86/1.95 fof(axiom_2,axiom, % 1.86/1.95 ! [X,Y] : % 1.86/1.95 ( rsymProp(X,Y) % 1.86/1.95 => ( Y = ia % 1.86/1.95 | Y = ib ) ) ). % 1.86/1.95 % 1.86/1.95 %----Symmetric: rsymProp % 1.86/1.95 fof(axiom_3,axiom, % 1.86/1.95 ! [X,Y] : % 1.86/1.95 ( rsymProp(X,Y) % 1.86/1.95 => rsymProp(Y,X) ) ). % 1.86/1.95 % 1.86/1.95 %----ia % 1.86/1.95 fof(axiom_4,axiom, % 1.86/1.95 cowlThing(ia) ). % 1.86/1.95 % 1.86/1.95 fof(axiom_5,axiom, % 1.86/1.95 rsymProp(ia,ia) ). % 1.86/1.95 % 1.86/1.95 %----ib % 1.86/1.95 fof(axiom_6,axiom, % 1.86/1.95 cowlThing(ib) ). % 1.86/1.95 % 1.86/1.95 fof(axiom_7,axiom, % 1.86/1.95 rsymProp(ib,ib) ). % 1.86/1.95 % 1.86/1.95 %----Thing and Nothing % 1.86/1.95 %----String and Integer disjoint % 1.86/1.95 %----Transitive: rsymProp % 1.86/1.95 %----ia % 1.86/1.95 fof(the_axiom,conjecture, % 1.86/1.95 ( ! [X] : % 1.86/1.95 ( cowlThing(X) % 1.86/1.95 & ~ cowlNothing(X) ) % 1.86/1.95 & ! [X] : % 1.86/1.95 ( xsd_string(X) % 1.86/1.95 <=> ~ xsd_integer(X) ) % 1.86/1.95 & ! [X,Y,Z] : % 1.86/1.95 ( ( rsymProp(X,Y) % 1.86/1.96 & rsymProp(Y,Z) ) % 1.86/1.96 => rsymProp(X,Z) ) % 1.86/1.96 & ? [X] : % 1.86/1.96 ( rsymProp(ia,X) % 1.86/1.96 & cowlThing(X) ) ) ). % 1.86/1.96 % 1.86/1.96 %------------------------------------------------------------------------------ % 1.86/1.96 %------------------------------------------- % 1.86/1.96 % Proof found % 1.86/1.96 % SZS status Theorem for theBenchmark % 1.86/1.96 % SZS output start Proof % 1.86/1.96 %ClaNum:21(EqnAxiom:8) % 1.86/1.96 %VarNum:19(SingletonVarNum:13) % 1.86/1.96 %MaxLitNum:5 % 1.86/1.96 %MaxfuncDepth:0 % 1.86/1.96 %SharedTerms:17 % 1.86/1.96 %goalClause: 16 17 18 19 20 21 % 1.86/1.96 [9]P1(a1,a1) % 1.86/1.96 [10]P1(a7,a7) % 1.86/1.96 [11]~P2(x111) % 1.86/1.96 [12]P4(x121)+P3(x121) % 1.86/1.96 [13]~P4(x131)+~P3(x131) % 1.86/1.96 [15]~P1(x152,x151)+P1(x151,x152) % 1.86/1.96 [14]~P1(x142,x141)+E(x141,a7)+E(x141,a1) % 1.86/1.96 [16]~P1(a1,x161)+P2(a2)+P3(a3)+P1(a4,a5)+~P4(a3) % 1.86/1.96 [17]~P1(a1,x171)+P2(a2)+P3(a3)+P1(a5,a6)+~P4(a3) % 1.86/1.96 [18]P1(a4,a5)+~P1(a1,x181)+P2(a2)+P4(a3)+~P3(a3) % 1.86/1.96 [19]P1(a5,a6)+~P1(a1,x191)+P2(a2)+P4(a3)+~P3(a3) % 1.86/1.96 [20]~P1(a1,x201)+P2(a2)+P3(a3)+~P4(a3)+~P1(a4,a6) % 1.86/1.96 [21]~P1(a1,x211)+~P1(a4,a6)+P2(a2)+P4(a3)+~P3(a3) % 1.86/1.96 %EqnAxiom % 1.86/1.96 [1]E(x11,x11) % 1.86/1.96 [2]E(x22,x21)+~E(x21,x22) % 1.86/1.96 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.86/1.96 [4]P1(x42,x43)+~E(x41,x42)+~P1(x41,x43) % 1.86/1.96 [5]P1(x53,x52)+~E(x51,x52)+~P1(x53,x51) % 1.86/1.96 [6]~P3(x61)+P3(x62)+~E(x61,x62) % 1.86/1.96 [7]~P2(x71)+P2(x72)+~E(x71,x72) % 1.86/1.96 [8]~P4(x81)+P4(x82)+~E(x81,x82) % 1.86/1.96 % 1.86/1.96 %------------------------------------------- % 1.86/1.96 cnf(24,plain, % 1.86/1.96 (~P2(x241)), % 1.86/1.96 inference(rename_variables,[],[11])). % 1.86/1.96 cnf(27,plain, % 1.86/1.96 (P1(a5,a6)+P3(a3)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[9,11,24,17])). % 1.86/1.96 cnf(30,plain, % 1.86/1.96 (P1(a4,a5)+P3(a3)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[11,9,16])). % 1.86/1.96 cnf(31,plain, % 1.86/1.96 (P1(a4,a5)+P4(a3)+~P3(a3)), % 1.86/1.96 inference(scs_inference,[],[11,9,18])). % 1.86/1.96 cnf(32,plain, % 1.86/1.96 (P1(a5,a6)+P4(a3)+~P3(a3)), % 1.86/1.96 inference(scs_inference,[],[11,9,19])). % 1.86/1.96 cnf(33,plain, % 1.86/1.96 (~P1(a4,a6)+P3(a3)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[11,9,20])). % 1.86/1.96 cnf(34,plain, % 1.86/1.96 (~P1(a4,a6)+P4(a3)+~P3(a3)), % 1.86/1.96 inference(scs_inference,[],[11,9,21])). % 1.86/1.96 cnf(35,plain, % 1.86/1.96 (P1(x351,a7)+~E(a7,x351)), % 1.86/1.96 inference(scs_inference,[],[10,4])). % 1.86/1.96 cnf(40,plain, % 1.86/1.96 (~E(x401,x402)+E(x402,x403)+~E(x403,x401)), % 1.86/1.96 inference(scs_inference,[],[2,3])). % 1.86/1.96 cnf(41,plain, % 1.86/1.96 (~P1(a6,a4)+P3(a3)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[15,33])). % 1.86/1.96 cnf(43,plain, % 1.86/1.96 (P1(a6,a5)+P3(a3)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[27,15])). % 1.86/1.96 cnf(44,plain, % 1.86/1.96 (P1(a5,a4)+P3(a3)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[30,15])). % 1.86/1.96 cnf(45,plain, % 1.86/1.96 (P1(a5,a4)+P4(a3)+~P3(a3)), % 1.86/1.96 inference(scs_inference,[],[31,15])). % 1.86/1.96 cnf(46,plain, % 1.86/1.96 (P1(a6,a5)+P4(a3)+~P3(a3)), % 1.86/1.96 inference(scs_inference,[],[32,15])). % 1.86/1.96 cnf(47,plain, % 1.86/1.96 (~P1(a6,a4)+P4(a3)+~P3(a3)), % 1.86/1.96 inference(scs_inference,[],[34,15])). % 1.86/1.96 cnf(48,plain, % 1.86/1.96 (~P4(a3)+~P1(a6,a4)), % 1.86/1.96 inference(scs_inference,[],[41,13])). % 1.86/1.96 cnf(49,plain, % 1.86/1.96 (~P1(a4,a6)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[48,15])). % 1.86/1.96 cnf(50,plain, % 1.86/1.96 (~P1(x501,a6)+~E(x501,a4)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[49,4])). % 1.86/1.96 cnf(53,plain, % 1.86/1.96 (~P4(a3)+P1(a6,a5)), % 1.86/1.96 inference(scs_inference,[],[43,13])). % 1.86/1.96 cnf(54,plain, % 1.86/1.96 (P1(a5,a6)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[53,15])). % 1.86/1.96 cnf(55,plain, % 1.86/1.96 (E(a6,a7)+E(a6,a1)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[54,14])). % 1.86/1.96 cnf(56,plain, % 1.86/1.96 (~P4(a3)+P1(a5,a4)), % 1.86/1.96 inference(scs_inference,[],[44,13])). % 1.86/1.96 cnf(57,plain, % 1.86/1.96 (P1(a4,a5)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[56,15])). % 1.86/1.96 cnf(60,plain, % 1.86/1.96 (P1(a5,a4)+~P3(a3)), % 1.86/1.96 inference(scs_inference,[],[45,56])). % 1.86/1.96 cnf(61,plain, % 1.86/1.96 (P1(a4,a5)+~P3(a3)), % 1.86/1.96 inference(scs_inference,[],[60,15])). % 1.86/1.96 cnf(62,plain, % 1.86/1.96 (P1(a4,x621)+~E(a5,x621)+~P3(a3)), % 1.86/1.96 inference(scs_inference,[],[61,5])). % 1.86/1.96 cnf(64,plain, % 1.86/1.96 (P1(a6,a5)+~P3(a3)), % 1.86/1.96 inference(scs_inference,[],[46,53])). % 1.86/1.96 cnf(67,plain, % 1.86/1.96 (~P1(a6,a4)+~P3(a3)), % 1.86/1.96 inference(scs_inference,[],[47,48])). % 1.86/1.96 cnf(68,plain, % 1.86/1.96 (~P1(a4,a6)+~P3(a3)), % 1.86/1.96 inference(scs_inference,[],[67,15])). % 1.86/1.96 cnf(69,plain, % 1.86/1.96 (~E(a5,a6)+~P3(a3)), % 1.86/1.96 inference(scs_inference,[],[68,62])). % 1.86/1.96 cnf(70,plain, % 1.86/1.96 (~E(a6,a5)+~P3(a3)), % 1.86/1.96 inference(scs_inference,[],[69,2])). % 1.86/1.96 cnf(73,plain, % 1.86/1.96 (E(a7,a6)+E(a6,a1)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[55,2])). % 1.86/1.96 cnf(75,plain, % 1.86/1.96 (E(a1,a6)+E(a7,a6)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[73,2])). % 1.86/1.96 cnf(77,plain, % 1.86/1.96 (P1(a6,a1)+E(a7,a6)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[9,75,4])). % 1.86/1.96 cnf(79,plain, % 1.86/1.96 (P1(a1,a6)+E(a7,a6)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[77,15])). % 1.86/1.96 cnf(80,plain, % 1.86/1.96 (~E(a1,a4)+E(a7,a6)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[79,50])). % 1.86/1.96 cnf(83,plain, % 1.86/1.96 (P4(a3)+P1(a5,a4)), % 1.86/1.96 inference(scs_inference,[],[12,60])). % 1.86/1.96 cnf(84,plain, % 1.86/1.96 (P1(a4,a5)+P4(a3)), % 1.86/1.96 inference(scs_inference,[],[83,15])). % 1.86/1.96 cnf(87,plain, % 1.86/1.96 (P3(a3)+~P1(a6,a4)), % 1.86/1.96 inference(scs_inference,[],[12,48])). % 1.86/1.96 cnf(88,plain, % 1.86/1.96 (~P1(a4,a6)+P3(a3)), % 1.86/1.96 inference(scs_inference,[],[87,15])). % 1.86/1.96 cnf(89,plain, % 1.86/1.96 (~P1(a4,x891)+~E(x891,a6)+P3(a3)), % 1.86/1.96 inference(scs_inference,[],[88,5])). % 1.86/1.96 cnf(91,plain, % 1.86/1.96 (P4(a3)+P1(a6,a5)), % 1.86/1.96 inference(scs_inference,[],[12,64])). % 1.86/1.96 cnf(92,plain, % 1.86/1.96 (P1(a5,a6)+P4(a3)), % 1.86/1.96 inference(scs_inference,[],[91,15])). % 1.86/1.96 cnf(93,plain, % 1.86/1.96 (E(a6,a7)+E(a6,a1)+P4(a3)), % 1.86/1.96 inference(scs_inference,[],[92,14])). % 1.86/1.96 cnf(94,plain, % 1.86/1.96 (E(a7,a6)+E(a6,a1)+P4(a3)), % 1.86/1.96 inference(scs_inference,[],[93,2])). % 1.86/1.96 cnf(95,plain, % 1.86/1.96 (E(a1,a6)+E(a7,a6)+P4(a3)), % 1.86/1.96 inference(scs_inference,[],[94,2])). % 1.86/1.96 cnf(96,plain, % 1.86/1.96 (P1(a6,a1)+E(a7,a6)+P4(a3)), % 1.86/1.96 inference(scs_inference,[],[9,95,4])). % 1.86/1.96 cnf(97,plain, % 1.86/1.96 (P1(a1,a6)+E(a7,a6)+P4(a3)), % 1.86/1.96 inference(scs_inference,[],[96,15])). % 1.86/1.96 cnf(98,plain, % 1.86/1.96 (P1(a1,a6)+E(a7,a6)), % 1.86/1.96 inference(scs_inference,[],[97,79])). % 1.86/1.96 cnf(99,plain, % 1.86/1.96 (P1(a6,a1)+E(a7,a6)), % 1.86/1.96 inference(scs_inference,[],[98,15])). % 1.86/1.96 cnf(100,plain, % 1.86/1.96 (P1(a6,x1001)+~E(a1,x1001)+E(a7,a6)), % 1.86/1.96 inference(scs_inference,[],[99,5])). % 1.86/1.96 cnf(102,plain, % 1.86/1.96 (P3(a3)+P1(a6,a5)), % 1.86/1.96 inference(scs_inference,[],[12,53])). % 1.86/1.96 cnf(103,plain, % 1.86/1.96 (P1(a5,a6)+P3(a3)), % 1.86/1.96 inference(scs_inference,[],[102,15])). % 1.86/1.96 cnf(104,plain, % 1.86/1.96 (~E(a5,a4)+P3(a3)+~P4(a3)), % 1.86/1.96 inference(scs_inference,[],[103,50])). % 1.86/1.96 cnf(118,plain, % 1.86/1.96 (P4(a3)+~P1(a6,a4)), % 1.86/1.96 inference(scs_inference,[],[12,67])). % 1.86/1.96 cnf(119,plain, % 1.86/1.96 (~P1(a4,a6)+P4(a3)), % 1.86/1.96 inference(scs_inference,[],[118,15])). % 1.86/1.96 cnf(120,plain, % 1.86/1.96 (~P1(x1201,a6)+~E(x1201,a4)+P4(a3)), % 1.86/1.96 inference(scs_inference,[],[119,4])). % 1.86/1.96 cnf(122,plain, % 1.86/1.96 (P3(a3)+P1(a5,a4)), % 1.86/1.96 inference(scs_inference,[],[12,56])). % 1.86/1.96 cnf(123,plain, % 1.86/1.96 (P1(a4,a5)+P3(a3)), % 1.86/1.96 inference(scs_inference,[],[122,15])). % 1.86/1.96 cnf(124,plain, % 1.86/1.96 (P1(a4,x1241)+~E(a5,x1241)+P3(a3)), % 1.86/1.96 inference(scs_inference,[],[123,5])). % 1.86/1.96 cnf(153,plain, % 1.86/1.96 (P3(a3)+~E(x1531,a4)+~P1(x1531,a6)), % 1.86/1.96 inference(scs_inference,[],[12,50])). % 1.86/1.96 cnf(157,plain, % 1.86/1.96 (P3(a3)+E(a6,a7)+E(a6,a1)), % 1.86/1.96 inference(scs_inference,[],[12,55])). % 1.86/1.96 cnf(158,plain, % 1.86/1.96 (E(a7,a6)+E(a6,a1)+P3(a3)), % 1.86/1.96 inference(scs_inference,[],[157,2])). % 1.86/1.96 cnf(159,plain, % 1.86/1.96 (P1(a6,a7)+E(a6,a1)+P3(a3)), % 1.86/1.96 inference(scs_inference,[],[10,158,4])). % 1.86/1.96 cnf(168,plain, % 1.86/1.96 (P3(a3)+E(a1,a6)+E(a7,a6)), % 1.86/1.96 inference(scs_inference,[],[12,75])). % 1.86/1.96 cnf(169,plain, % 1.86/1.96 (E(a7,a6)+~P1(a4,a1)+P3(a3)), % 1.86/1.96 inference(scs_inference,[],[168,89])). % 1.86/1.96 cnf(170,plain, % 1.86/1.96 (P1(a6,a7)+~P1(a4,a1)+P3(a3)), % 1.86/1.96 inference(scs_inference,[],[10,169,4])). % 1.86/1.96 cnf(171,plain, % 1.86/1.96 (P1(a7,a6)+~P1(a4,a1)+P3(a3)), % 1.86/1.96 inference(scs_inference,[],[170,15])). % 1.86/1.96 cnf(172,plain, % 1.86/1.96 (~E(a7,a4)+~P1(a4,a1)+P3(a3)), % 1.86/1.96 inference(scs_inference,[],[171,153])). % 1.86/1.96 cnf(173,plain, % 1.86/1.96 (~E(a4,a7)+~P1(a4,a1)+P3(a3)), % 1.86/1.96 inference(scs_inference,[],[172,2])). % 1.86/1.96 cnf(174,plain, % 1.86/1.96 (P3(a3)+E(a7,a6)+~E(a1,a4)), % 1.86/1.96 inference(scs_inference,[],[12,80])). % 1.86/1.96 cnf(175,plain, % 1.86/1.96 (~E(a1,a4)+~P1(a4,a7)+P3(a3)), % 1.86/1.96 inference(scs_inference,[],[174,89])). % 1.86/1.96 cnf(178,plain, % 1.86/1.96 (~E(a5,a4)+P3(a3)), % 1.86/1.96 inference(scs_inference,[],[12,104])). % 1.86/1.97 cnf(179,plain, % 1.86/1.97 (~E(x1791,a4)+~E(a5,x1791)+P3(a3)), % 1.86/1.97 inference(scs_inference,[],[178,3])). % 1.86/1.97 cnf(180,plain, % 1.86/1.97 (~E(x1801,a5)+~E(x1801,a4)+P3(a3)), % 1.86/1.97 inference(scs_inference,[],[179,2])). % 1.86/1.97 cnf(181,plain, % 1.86/1.97 (~E(a4,x1811)+~E(x1811,a5)+P3(a3)), % 1.86/1.97 inference(scs_inference,[],[180,2])). % 1.86/1.97 cnf(182,plain, % 1.86/1.97 (~E(a5,x1821)+~E(a4,x1821)+P3(a3)), % 1.86/1.97 inference(scs_inference,[],[181,2])). % 1.86/1.97 cnf(196,plain, % 1.86/1.97 (~P3(a3)+E(a7,a6)+E(a6,a1)), % 1.86/1.97 inference(scs_inference,[],[13,94])). % 1.86/1.97 cnf(197,plain, % 1.86/1.97 (P1(a6,a7)+E(a6,a1)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[10,196,4])). % 1.86/1.97 cnf(201,plain, % 1.86/1.97 (~P4(a3)+~E(a5,x2011)+P1(a4,x2011)), % 1.86/1.97 inference(scs_inference,[],[13,124])). % 1.86/1.97 cnf(208,plain, % 1.86/1.97 (~P3(a3)+~E(x2081,a4)+~P1(x2081,a6)), % 1.86/1.97 inference(scs_inference,[],[13,120])). % 1.86/1.97 cnf(210,plain, % 1.86/1.97 (~P4(a3)+P1(a6,a7)+E(a6,a1)), % 1.86/1.97 inference(scs_inference,[],[13,159])). % 1.86/1.97 cnf(211,plain, % 1.86/1.97 (P1(a7,a6)+E(a6,a1)+~P4(a3)), % 1.86/1.97 inference(scs_inference,[],[210,15])). % 1.86/1.97 cnf(212,plain, % 1.86/1.97 (E(a6,a1)+~E(a7,a4)+~P4(a3)), % 1.86/1.97 inference(scs_inference,[],[211,50])). % 1.86/1.97 cnf(213,plain, % 1.86/1.97 (E(a1,a6)+~E(a7,a4)+~P4(a3)), % 1.86/1.97 inference(scs_inference,[],[212,2])). % 1.86/1.97 cnf(234,plain, % 1.86/1.97 (~P4(a3)+~E(a1,a4)+~P1(a4,a7)), % 1.86/1.97 inference(scs_inference,[],[13,175])). % 1.86/1.97 cnf(235,plain, % 1.86/1.97 (~E(a4,a1)+~P4(a3)+~P1(a4,a7)), % 1.86/1.97 inference(scs_inference,[],[234,2])). % 1.86/1.97 cnf(257,plain, % 1.86/1.97 (~P1(a6,a4)), % 1.86/1.97 inference(scs_inference,[],[48,118])). % 1.86/1.97 cnf(271,plain, % 1.86/1.97 (E(a5,a7)+E(a5,a1)+~P4(a3)), % 1.86/1.97 inference(scs_inference,[],[53,14])). % 1.86/1.97 cnf(279,plain, % 1.86/1.97 (P1(a6,a5)), % 1.86/1.97 inference(scs_inference,[],[53,91])). % 1.86/1.97 cnf(280,plain, % 1.86/1.97 (~E(a5,a4)), % 1.86/1.97 inference(scs_inference,[],[257,279,5])). % 1.86/1.97 cnf(281,plain, % 1.86/1.97 (P1(x2811,a5)+~E(a6,x2811)), % 1.86/1.97 inference(scs_inference,[],[257,279,5,4])). % 1.86/1.97 cnf(289,plain, % 1.86/1.97 (P1(a5,a6)), % 1.86/1.97 inference(scs_inference,[],[54,92])). % 1.86/1.97 cnf(290,plain, % 1.86/1.97 (P1(a5,x2901)+~E(a6,x2901)), % 1.86/1.97 inference(scs_inference,[],[289,5])). % 1.86/1.97 cnf(292,plain, % 1.86/1.97 (P1(a5,a4)), % 1.86/1.97 inference(scs_inference,[],[56,83])). % 1.86/1.97 cnf(293,plain, % 1.86/1.97 (~E(a5,a6)), % 1.86/1.97 inference(scs_inference,[],[257,292,4])). % 1.86/1.97 cnf(294,plain, % 1.86/1.97 (P1(a5,x2941)+~E(a4,x2941)), % 1.86/1.97 inference(scs_inference,[],[257,292,4,5])). % 1.86/1.97 cnf(296,plain, % 1.86/1.97 (P1(a4,a5)), % 1.86/1.97 inference(scs_inference,[],[57,84])). % 1.86/1.97 cnf(298,plain, % 1.86/1.97 (P1(a7,a5)+E(a4,a1)), % 1.86/1.97 inference(scs_inference,[],[296,292,4,14])). % 1.86/1.97 cnf(315,plain, % 1.86/1.97 (~E(a5,x3151)+~E(x3151,a6)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[70,40])). % 1.86/1.97 cnf(316,plain, % 1.86/1.97 (~E(a1,a4)+~E(a5,a7)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[257,315,100])). % 1.86/1.97 cnf(317,plain, % 1.86/1.97 (~E(a4,a1)+~E(a5,a7)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[316,2])). % 1.86/1.97 cnf(318,plain, % 1.86/1.97 (~E(a5,a7)+E(a4,a7)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[292,317,14])). % 1.86/1.97 cnf(319,plain, % 1.86/1.97 (E(a5,a1)+E(a4,a7)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[279,318,14])). % 1.86/1.97 cnf(320,plain, % 1.86/1.97 (P1(a1,a6)+E(a4,a7)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[289,319,4])). % 1.86/1.97 cnf(321,plain, % 1.86/1.97 (~E(a1,a4)+E(a4,a7)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[320,208])). % 1.86/1.97 cnf(322,plain, % 1.86/1.97 (~E(a4,a1)+E(a4,a7)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[321,2])). % 1.86/1.97 cnf(323,plain, % 1.86/1.97 (E(a4,a7)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[292,322,14])). % 1.86/1.97 cnf(375,plain, % 1.86/1.97 (P4(a3)+E(a4,a7)), % 1.86/1.97 inference(scs_inference,[],[323,12])). % 1.86/1.97 cnf(376,plain, % 1.86/1.97 (E(a7,a4)+P4(a3)), % 1.86/1.97 inference(scs_inference,[],[375,2])). % 1.86/1.97 cnf(444,plain, % 1.86/1.97 (~E(x4441,a4)+E(a7,x4441)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[323,40])). % 1.86/1.97 cnf(471,plain, % 1.86/1.97 (~E(a1,a4)+E(a4,a7)+E(a7,a6)), % 1.86/1.97 inference(scs_inference,[],[323,174])). % 1.86/1.97 cnf(472,plain, % 1.86/1.97 (~E(a4,a1)+E(a4,a7)+E(a7,a6)), % 1.86/1.97 inference(scs_inference,[],[471,2])). % 1.86/1.97 cnf(473,plain, % 1.86/1.97 (E(a7,a6)+E(a4,a7)), % 1.86/1.97 inference(scs_inference,[],[292,472,14])). % 1.86/1.97 cnf(474,plain, % 1.86/1.97 (E(a7,a6)+P1(a5,a7)), % 1.86/1.97 inference(scs_inference,[],[473,294])). % 1.86/1.97 cnf(475,plain, % 1.86/1.97 (P1(a7,a5)+E(a7,a6)), % 1.86/1.97 inference(scs_inference,[],[474,15])). % 1.86/1.97 cnf(476,plain, % 1.86/1.97 (P1(x4761,a5)+~E(a7,x4761)+E(a7,a6)), % 1.86/1.97 inference(scs_inference,[],[475,4])). % 1.86/1.97 cnf(478,plain, % 1.86/1.97 (~E(a1,a4)+E(a4,a7)+~P1(a4,a7)), % 1.86/1.97 inference(scs_inference,[],[323,175])). % 1.86/1.97 cnf(479,plain, % 1.86/1.97 (~E(a4,a1)+E(a4,a7)+~P1(a4,a7)), % 1.86/1.97 inference(scs_inference,[],[478,2])). % 1.86/1.97 cnf(480,plain, % 1.86/1.97 (E(a4,a7)+~P1(a4,a7)), % 1.86/1.97 inference(scs_inference,[],[292,479,14])). % 1.86/1.97 cnf(485,plain, % 1.86/1.97 (E(a4,a7)+~E(a5,x4851)+~E(x4851,a4)), % 1.86/1.97 inference(scs_inference,[],[323,179])). % 1.86/1.97 cnf(486,plain, % 1.86/1.97 (~E(a7,a5)+~E(x4861,a4)+~E(a5,x4861)), % 1.86/1.97 inference(scs_inference,[],[280,485,40])). % 1.86/1.97 cnf(498,plain, % 1.86/1.97 (E(a4,a7)+~E(x4981,a5)+~E(a4,x4981)), % 1.86/1.97 inference(scs_inference,[],[323,181])). % 1.86/1.97 cnf(499,plain, % 1.86/1.97 (~E(a7,a5)+~E(a4,x4991)+~E(x4991,a5)), % 1.86/1.97 inference(scs_inference,[],[280,498,40])). % 1.86/1.97 cnf(500,plain, % 1.86/1.97 (~E(a5,a7)+~E(a4,a7)), % 1.86/1.97 inference(scs_inference,[],[499,2])). % 1.86/1.97 cnf(501,plain, % 1.86/1.97 (~E(a4,a7)+E(a5,a1)), % 1.86/1.97 inference(scs_inference,[],[279,500,14])). % 1.86/1.97 cnf(542,plain, % 1.86/1.97 (~P1(a7,a6)+P4(a3)), % 1.86/1.97 inference(scs_inference,[],[376,120])). % 1.86/1.97 cnf(543,plain, % 1.86/1.97 (~P1(a6,a7)+P4(a3)), % 1.86/1.97 inference(scs_inference,[],[542,15])). % 1.86/1.97 cnf(544,plain, % 1.86/1.97 (E(a6,a1)+P4(a3)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[543,197])). % 1.86/1.97 cnf(545,plain, % 1.86/1.97 (~E(a1,a5)+P4(a3)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[293,544,40])). % 1.86/1.97 cnf(546,plain, % 1.86/1.97 (~E(a5,a1)+P4(a3)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[545,2])). % 1.86/1.97 cnf(547,plain, % 1.86/1.97 (E(a5,a7)+P4(a3)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[279,546,14])). % 1.86/1.97 cnf(548,plain, % 1.86/1.97 (P1(a7,a6)+P4(a3)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[289,547,4])). % 1.86/1.97 cnf(549,plain, % 1.86/1.97 (~E(a7,a4)+P4(a3)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[548,208])). % 1.86/1.97 cnf(550,plain, % 1.86/1.97 (P4(a3)+~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[549,444])). % 1.86/1.97 cnf(551,plain, % 1.86/1.97 (~P3(a3)), % 1.86/1.97 inference(scs_inference,[],[550,13])). % 1.86/1.97 cnf(552,plain, % 1.86/1.97 (~E(x5521,a6)+~P1(a4,x5521)), % 1.86/1.97 inference(scs_inference,[],[551,89])). % 1.86/1.97 cnf(553,plain, % 1.86/1.97 (~E(a5,x5531)+P1(a4,x5531)), % 1.86/1.97 inference(scs_inference,[],[551,124])). % 1.86/1.97 cnf(561,plain, % 1.86/1.97 (E(a7,a6)+~P1(a4,a1)), % 1.86/1.97 inference(scs_inference,[],[551,169])). % 1.86/1.97 cnf(565,plain, % 1.86/1.97 (~E(a4,a7)+~P1(a4,a1)), % 1.86/1.97 inference(scs_inference,[],[551,173])). % 1.86/1.97 cnf(566,plain, % 1.86/1.97 (~E(a1,a4)+E(a7,a6)), % 1.86/1.97 inference(scs_inference,[],[551,174])). % 1.86/1.97 cnf(567,plain, % 1.86/1.97 (~E(a1,a4)+~P1(a4,a7)), % 1.86/1.97 inference(scs_inference,[],[551,175])). % 1.86/1.97 cnf(573,plain, % 1.86/1.97 (~E(a4,x5731)+~E(a5,x5731)), % 1.86/1.97 inference(scs_inference,[],[551,182])). % 1.86/1.97 cnf(574,plain, % 1.86/1.97 (P4(a3)), % 1.86/1.97 inference(scs_inference,[],[551,12])). % 1.86/1.97 cnf(594,plain, % 1.86/1.97 (P1(a4,x5941)+~E(a5,x5941)), % 1.86/1.97 inference(scs_inference,[],[574,201])). % 1.86/1.97 cnf(596,plain, % 1.86/1.97 (~E(a7,a4)+E(a6,a1)), % 1.86/1.97 inference(scs_inference,[],[574,212])). % 1.86/1.97 cnf(597,plain, % 1.86/1.97 (~E(a7,a4)+E(a1,a6)), % 1.86/1.97 inference(scs_inference,[],[574,213])). % 1.86/1.97 cnf(615,plain, % 1.86/1.97 (~E(a4,a1)+~P1(a4,a7)), % 1.86/1.97 inference(scs_inference,[],[574,235])). % 1.86/1.97 cnf(618,plain, % 1.86/1.97 (E(a5,a1)+E(a5,a7)), % 1.86/1.97 inference(scs_inference,[],[574,271])). % 1.86/1.97 cnf(648,plain, % 1.86/1.97 (~P1(a4,a1)+~P1(a4,a7)), % 1.86/1.97 inference(scs_inference,[],[561,552])). % 1.86/1.97 cnf(653,plain, % 1.86/1.97 (~P1(a4,a1)+E(a4,a1)), % 1.86/1.97 inference(scs_inference,[],[292,565,14])). % 1.86/1.97 cnf(654,plain, % 1.86/1.97 (~E(a4,x6541)+~E(x6541,a1)+E(a7,a6)), % 1.86/1.97 inference(scs_inference,[],[566,40])). % 1.86/1.97 cnf(655,plain, % 1.86/1.97 (~E(x6551,a4)+~E(a1,x6551)+~P1(a4,a7)), % 1.86/1.97 inference(scs_inference,[],[567,3])). % 1.86/1.97 cnf(661,plain, % 1.86/1.97 (E(a5,a7)+~E(a4,a1)), % 1.86/1.97 inference(scs_inference,[],[279,573,14])). % 1.86/1.97 cnf(674,plain, % 1.86/1.97 (~E(a4,a7)+E(a6,a1)), % 1.86/1.97 inference(scs_inference,[],[596,2])). % 1.86/1.97 cnf(675,plain, % 1.86/1.97 (~E(a4,a7)+E(a1,a6)), % 1.86/1.97 inference(scs_inference,[],[597,2])). % 1.86/1.97 cnf(700,plain, % 1.86/1.97 (~P1(a4,a7)+~E(a5,a1)), % 1.86/1.97 inference(scs_inference,[],[648,553])). % 1.86/1.97 cnf(702,plain, % 1.86/1.97 (E(a4,a1)+~E(a5,a1)), % 1.86/1.97 inference(scs_inference,[],[653,594])). % 1.86/1.97 cnf(704,plain, % 1.86/1.97 (~E(a5,a1)+E(a5,a7)), % 1.86/1.97 inference(scs_inference,[],[661,702])). % 1.86/1.97 cnf(715,plain, % 1.86/1.97 (E(a6,a1)+~P1(a4,a7)), % 1.86/1.97 inference(scs_inference,[],[674,480])). % 1.86/1.97 cnf(716,plain, % 1.86/1.97 (E(a1,a6)+~P1(a4,a7)), % 1.86/1.97 inference(scs_inference,[],[675,480])). % 1.86/1.97 cnf(731,plain, % 1.86/1.97 (E(a5,a7)), % 1.86/1.97 inference(scs_inference,[],[704,618])). % 1.86/1.97 cnf(767,plain, % 1.86/1.97 ($false), % 1.86/1.97 inference(scs_inference,[],[9,293,731,594,615,648,700,715,716,552,15,2,476,486,654,655,100,40,4,5,35,281,298,566,290,473,501]), % 1.86/1.97 ['proof']). % 1.86/1.97 % SZS output end Proof % 1.86/1.97 % Total time :1.340000s %------------------------------------------------------------------------------