%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS162+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 : n014.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:44 EDT 2024 % Result : Theorem 58.73s 58.92s % Output : CNFRefutation 58.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : KRS162+1 : TPTP v8.2.0. Released v3.1.0. % 0.00/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.31 % Computer : n014.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Wed Jun 19 14:30:54 EDT 2024 % 0.10/0.31 % CPUTime : % 0.16/0.52 start to proof:theBenchmark % 58.73/58.91 %------------------------------------------- % 58.73/58.91 % File :CSE---1.7 % 58.73/58.91 % Problem :theBenchmark % 58.73/58.91 % Transform :cnf % 58.73/58.91 % Format :tptp:raw % 58.73/58.91 % Command :java -jar mcs_scs.jar %d %s % 58.73/58.91 % 58.73/58.91 % Result :Theorem 58.210000s % 58.73/58.91 % Output :CNFRefutation 58.210000s % 58.73/58.91 %------------------------------------------- % 58.73/58.91 %------------------------------------------------------------------------------ % 58.73/58.92 % File : KRS162+1 : TPTP v8.2.0. Released v3.1.0. % 58.73/58.92 % Domain : Knowledge Representation (Semantic Web) % 58.73/58.92 % Problem : Entailment for three natural numbers % 58.73/58.92 % Version : Especial. % 58.73/58.92 % English : This entailment can be replicated for any three natural numbers % 58.73/58.92 % i, j, k such that i+j >= k. In this example, they are chosen as % 58.73/58.92 % 2, 3 and 5. % 58.73/58.92 % 58.73/58.92 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 58.73/58.92 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 58.73/58.92 % Source : [Bec03] % 58.73/58.92 % Names : positive_description-logic-Manifest901 [Bec03] % 58.73/58.92 % 58.73/58.92 % Status : Theorem % 58.73/58.92 % Rating : 0.00 v5.3.0, 0.27 v5.2.0, 0.00 v4.1.0, 0.30 v4.0.0, 0.33 v3.7.0, 0.14 v3.5.0, 0.11 v3.4.0, 0.08 v3.3.0, 0.22 v3.2.0, 0.33 v3.1.0 % 58.73/58.92 % Syntax : Number of formulae : 20 ( 0 unt; 0 def) % 58.73/58.92 % Number of atoms : 78 ( 26 equ) % 58.73/58.92 % Maximal formula atoms : 28 ( 3 avg) % 58.73/58.92 % Number of connectives : 77 ( 19 ~; 0 |; 39 &) % 58.73/58.92 % ( 2 <=>; 17 =>; 0 <=; 0 <~>) % 58.73/58.92 % Maximal formula depth : 25 ( 6 avg) % 58.73/58.92 % Maximal term depth : 1 ( 1 avg) % 58.73/58.92 % Number of predicates : 10 ( 9 usr; 0 prp; 1-2 aty) % 58.73/58.92 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 58.73/58.92 % Number of variables : 54 ( 44 !; 10 ?) % 58.73/58.92 % SPC : FOF_THM_EPR_SEQ % 58.73/58.92 % 58.73/58.92 % Comments : Sean Bechhofer says there are some errors in the encoding of % 58.73/58.92 % datatypes, so this problem may not be perfect. At least it's % 58.73/58.92 % still representative of the type of reasoning required for OWL. % 58.73/58.92 %------------------------------------------------------------------------------ % 58.73/58.92 fof(cA_substitution_1,axiom, % 58.73/58.92 ! [A,B] : % 58.73/58.92 ( ( A = B % 58.73/58.92 & cA(A) ) % 58.73/58.92 => cA(B) ) ). % 58.73/58.92 % 58.73/58.92 fof(cB_substitution_1,axiom, % 58.73/58.92 ! [A,B] : % 58.73/58.92 ( ( A = B % 58.73/58.92 & cB(A) ) % 58.73/58.92 => cB(B) ) ). % 58.73/58.92 % 58.73/58.92 fof(cowlNothing_substitution_1,axiom, % 58.73/58.92 ! [A,B] : % 58.73/58.92 ( ( A = B % 58.73/58.92 & cowlNothing(A) ) % 58.73/58.92 => cowlNothing(B) ) ). % 58.73/58.92 % 58.73/58.92 fof(cowlThing_substitution_1,axiom, % 58.73/58.92 ! [A,B] : % 58.73/58.92 ( ( A = B % 58.73/58.92 & cowlThing(A) ) % 58.73/58.92 => cowlThing(B) ) ). % 58.73/58.92 % 58.73/58.92 fof(rp_substitution_1,axiom, % 58.73/58.92 ! [A,B,C] : % 58.73/58.92 ( ( A = B % 58.73/58.92 & rp(A,C) ) % 58.73/58.92 => rp(B,C) ) ). % 58.73/58.92 % 58.73/58.92 fof(rp_substitution_2,axiom, % 58.73/58.92 ! [A,B,C] : % 58.73/58.92 ( ( A = B % 58.73/58.92 & rp(C,A) ) % 58.73/58.92 => rp(C,B) ) ). % 58.73/58.92 % 58.73/58.92 fof(rq_substitution_1,axiom, % 58.73/58.92 ! [A,B,C] : % 58.73/58.92 ( ( A = B % 58.73/58.92 & rq(A,C) ) % 58.73/58.92 => rq(B,C) ) ). % 58.73/58.92 % 58.73/58.92 fof(rq_substitution_2,axiom, % 58.73/58.92 ! [A,B,C] : % 58.73/58.92 ( ( A = B % 58.73/58.92 & rq(C,A) ) % 58.73/58.92 => rq(C,B) ) ). % 58.73/58.92 % 58.73/58.92 fof(rr_substitution_1,axiom, % 58.73/58.92 ! [A,B,C] : % 58.73/58.92 ( ( A = B % 58.73/58.92 & rr(A,C) ) % 58.73/58.92 => rr(B,C) ) ). % 58.73/58.92 % 58.73/58.92 fof(rr_substitution_2,axiom, % 58.73/58.92 ! [A,B,C] : % 58.73/58.92 ( ( A = B % 58.73/58.92 & rr(C,A) ) % 58.73/58.92 => rr(C,B) ) ). % 58.73/58.92 % 58.73/58.92 fof(xsd_integer_substitution_1,axiom, % 58.73/58.92 ! [A,B] : % 58.73/58.92 ( ( A = B % 58.73/58.92 & xsd_integer(A) ) % 58.73/58.92 => xsd_integer(B) ) ). % 58.73/58.92 % 58.73/58.92 fof(xsd_string_substitution_1,axiom, % 58.73/58.92 ! [A,B] : % 58.73/58.92 ( ( A = B % 58.73/58.92 & xsd_string(A) ) % 58.73/58.92 => xsd_string(B) ) ). % 58.73/58.92 % 58.73/58.92 %----Thing and Nothing % 58.73/58.92 fof(axiom_0,axiom, % 58.73/58.92 ! [X] : % 58.73/58.92 ( cowlThing(X) % 58.73/58.92 & ~ cowlNothing(X) ) ). % 58.73/58.92 % 58.73/58.92 %----String and Integer disjoint % 58.73/58.92 fof(axiom_1,axiom, % 58.73/58.92 ! [X] : % 58.73/58.92 ( xsd_string(X) % 58.73/58.92 <=> ~ xsd_integer(X) ) ). % 58.73/58.92 % 58.73/58.92 %----Range: rp % 58.73/58.92 fof(axiom_2,axiom, % 58.73/58.92 ! [X,Y] : % 58.73/58.92 ( rp(X,Y) % 58.73/58.92 => cA(Y) ) ). % 58.73/58.92 % 58.73/58.92 %----Range: rq % 58.73/58.92 fof(axiom_3,axiom, % 58.73/58.92 ! [X,Y] : % 58.73/58.92 ( rq(X,Y) % 58.73/58.92 => cB(Y) ) ). % 58.73/58.92 % 58.73/58.92 fof(axiom_4,axiom, % 58.73/58.92 ! [X] : % 58.73/58.92 ~ ( cB(X) % 58.73/58.92 & cA(X) ) ). % 58.73/58.92 % 58.73/58.92 fof(axiom_5,axiom, % 58.73/58.92 ! [X,Y] : % 58.73/58.92 ( rq(X,Y) % 58.73/58.92 => rr(X,Y) ) ). % 58.73/58.92 % 58.73/58.92 fof(axiom_6,axiom, % 58.73/58.92 ! [X,Y] : % 58.73/58.92 ( rp(X,Y) % 58.73/58.92 => rr(X,Y) ) ). % 58.73/58.92 % 58.73/58.92 %----Thing and Nothing % 58.73/58.92 %----String and Integer disjoint % 58.73/58.92 fof(the_axiom,conjecture, % 58.73/58.92 ( ! [X] : % 58.73/58.92 ( cowlThing(X) % 58.73/58.92 & ~ cowlNothing(X) ) % 58.73/58.92 & ! [X] : % 58.73/58.92 ( xsd_string(X) % 58.73/58.92 <=> ~ xsd_integer(X) ) % 58.73/58.92 & ! [X] : % 58.73/58.92 ( ( ? [Y0,Y1] : % 58.73/58.92 ( rp(X,Y0) % 58.73/58.92 & rp(X,Y1) % 58.73/58.92 & Y0 != Y1 ) % 58.73/58.92 & ? [Y0,Y1,Y2] : % 58.73/58.92 ( rq(X,Y0) % 58.73/58.92 & rq(X,Y1) % 58.73/58.92 & rq(X,Y2) % 58.73/58.92 & Y0 != Y1 % 58.73/58.92 & Y0 != Y2 % 58.73/58.92 & Y1 != Y2 ) ) % 58.73/58.92 => ? [Y0,Y1,Y2,Y3,Y4] : % 58.73/58.92 ( rr(X,Y0) % 58.73/58.92 & rr(X,Y1) % 58.73/58.92 & rr(X,Y2) % 58.73/58.92 & rr(X,Y3) % 58.73/58.92 & rr(X,Y4) % 58.73/58.92 & Y0 != Y1 % 58.73/58.92 & Y0 != Y2 % 58.73/58.92 & Y0 != Y3 % 58.73/58.92 & Y0 != Y4 % 58.73/58.92 & Y1 != Y2 % 58.73/58.92 & Y1 != Y3 % 58.73/58.92 & Y1 != Y4 % 58.73/58.92 & Y2 != Y3 % 58.73/58.92 & Y2 != Y4 % 58.73/58.92 & Y3 != Y4 ) ) ) ). % 58.73/58.92 % 58.73/58.92 %------------------------------------------------------------------------------ % 58.73/58.92 %------------------------------------------- % 58.73/58.92 % Proof found % 58.73/58.92 % SZS status Theorem for theBenchmark % 58.73/58.92 % SZS output start Proof % 58.73/58.92 %ClaNum:42(EqnAxiom:14) % 58.73/58.92 %VarNum:71(SingletonVarNum:22) % 58.73/58.92 %MaxLitNum:18 % 58.73/58.92 %MaxfuncDepth:0 % 58.73/58.92 %SharedTerms:22 % 58.73/58.92 %goalClause: 17 18 19 20 21 22 23 24 27 28 29 30 31 32 33 34 35 36 41 42 % 58.73/58.92 [15]~P1(x151) % 58.73/58.92 [16]P8(x161)+P4(x161) % 58.73/58.92 [25]~P3(x251)+~P2(x251) % 58.73/58.92 [26]~P8(x261)+~P4(x261) % 58.73/58.92 [37]P2(x371)+~P5(x372,x371) % 58.73/58.92 [38]P3(x381)+~P6(x382,x381) % 58.73/58.92 [39]~P5(x391,x392)+P7(x391,x392) % 58.73/58.92 [40]~P6(x401,x402)+P7(x401,x402) % 58.73/58.92 [17]P1(a1)+P4(a2)+~E(a3,a4)+~P8(a2) % 58.73/58.92 [18]P1(a1)+P4(a2)+~E(a6,a7)+~P8(a2) % 58.73/58.92 [19]P1(a1)+P4(a2)+~E(a8,a7)+~P8(a2) % 58.73/58.92 [20]P1(a1)+P4(a2)+~E(a8,a6)+~P8(a2) % 58.73/58.92 [21]~E(a3,a4)+P1(a1)+P8(a2)+~P4(a2) % 58.73/58.92 [22]~E(a6,a7)+P1(a1)+P8(a2)+~P4(a2) % 58.73/58.92 [23]~E(a8,a7)+P1(a1)+P8(a2)+~P4(a2) % 58.73/58.92 [24]~E(a8,a6)+P1(a1)+P8(a2)+~P4(a2) % 58.73/58.92 [27]P1(a1)+P4(a2)+P5(a5,a4)+~P8(a2) % 58.73/58.92 [28]P1(a1)+P4(a2)+P5(a5,a3)+~P8(a2) % 58.73/58.92 [29]P1(a1)+P4(a2)+P6(a5,a7)+~P8(a2) % 58.73/58.92 [30]P1(a1)+P4(a2)+P6(a5,a6)+~P8(a2) % 58.73/58.92 [31]P1(a1)+P4(a2)+P6(a5,a8)+~P8(a2) % 58.73/58.92 [32]P5(a5,a4)+P1(a1)+P8(a2)+~P4(a2) % 58.73/58.92 [33]P5(a5,a3)+P1(a1)+P8(a2)+~P4(a2) % 58.73/58.92 [34]P6(a5,a7)+P1(a1)+P8(a2)+~P4(a2) % 58.73/58.92 [35]P6(a5,a6)+P1(a1)+P8(a2)+~P4(a2) % 58.73/58.92 [36]P6(a5,a8)+P1(a1)+P8(a2)+~P4(a2) % 58.73/58.92 [41]E(x413,x411)+E(x415,x414)+E(x414,x411)+E(x414,x413)+E(x415,x413)+E(x415,x411)+E(x411,x412)+E(x413,x412)+E(x414,x412)+E(x415,x412)+~P7(a5,x412)+~P7(a5,x411)+~P7(a5,x413)+~P7(a5,x414)+~P7(a5,x415)+P1(a1)+P4(a2)+~P8(a2) % 58.73/58.92 [42]E(x423,x421)+E(x425,x424)+E(x424,x421)+E(x424,x423)+E(x425,x423)+E(x425,x421)+E(x421,x422)+E(x423,x422)+E(x424,x422)+E(x425,x422)+~P7(a5,x422)+~P7(a5,x421)+~P7(a5,x423)+~P7(a5,x424)+~P7(a5,x425)+P1(a1)+P8(a2)+~P4(a2) % 58.73/58.92 %EqnAxiom % 58.73/58.92 [1]E(x11,x11) % 58.73/58.92 [2]E(x22,x21)+~E(x21,x22) % 58.73/58.92 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.73/58.92 [4]~P1(x41)+P1(x42)+~E(x41,x42) % 58.73/58.92 [5]~P4(x51)+P4(x52)+~E(x51,x52) % 58.73/58.92 [6]~P8(x61)+P8(x62)+~E(x61,x62) % 58.73/58.92 [7]P7(x72,x73)+~E(x71,x72)+~P7(x71,x73) % 58.73/58.92 [8]P7(x83,x82)+~E(x81,x82)+~P7(x83,x81) % 58.73/58.92 [9]P6(x92,x93)+~E(x91,x92)+~P6(x91,x93) % 58.73/58.92 [10]P6(x103,x102)+~E(x101,x102)+~P6(x103,x101) % 58.73/58.92 [11]P5(x112,x113)+~E(x111,x112)+~P5(x111,x113) % 58.73/58.92 [12]P5(x123,x122)+~E(x121,x122)+~P5(x123,x121) % 58.73/58.92 [13]~P3(x131)+P3(x132)+~E(x131,x132) % 58.73/58.92 [14]~P2(x141)+P2(x142)+~E(x141,x142) % 58.73/58.92 % 58.73/58.92 %------------------------------------------- % 58.78/58.93 cnf(43,plain, % 58.78/58.93 (~P1(x431)), % 58.78/58.93 inference(rename_variables,[],[15])). % 58.78/58.93 cnf(44,plain, % 58.78/58.93 (~P1(x441)), % 58.78/58.93 inference(rename_variables,[],[15])). % 58.78/58.93 cnf(46,plain, % 58.78/58.93 (~E(a8,a7)+P4(a2)+~P8(a2)), % 58.78/58.93 inference(scs_inference,[],[15,43,44,19])). % 58.78/58.93 cnf(47,plain, % 58.78/58.93 (~E(a3,a4)+P4(a2)+~P8(a2)), % 58.78/58.93 inference(scs_inference,[],[15,17])). % 58.78/58.93 cnf(48,plain, % 58.78/58.93 (~E(a6,a7)+P4(a2)+~P8(a2)), % 58.78/58.93 inference(scs_inference,[],[15,18])). % 58.78/58.93 cnf(49,plain, % 58.78/58.93 (~E(a8,a6)+P4(a2)+~P8(a2)), % 58.78/58.93 inference(scs_inference,[],[15,20])). % 58.78/58.93 cnf(50,plain, % 58.78/58.93 (~E(a3,a4)+P8(a2)+~P4(a2)), % 58.78/58.93 inference(scs_inference,[],[15,21])). % 58.78/58.93 cnf(51,plain, % 58.78/58.93 (~E(a6,a7)+P8(a2)+~P4(a2)), % 58.78/58.93 inference(scs_inference,[],[15,22])). % 58.78/58.93 cnf(52,plain, % 58.78/58.93 (~E(a8,a7)+P8(a2)+~P4(a2)), % 58.78/58.93 inference(scs_inference,[],[15,23])). % 58.78/58.93 cnf(53,plain, % 58.78/58.93 (~E(a8,a6)+P8(a2)+~P4(a2)), % 58.78/58.93 inference(scs_inference,[],[15,24])). % 58.78/58.93 cnf(54,plain, % 58.78/58.93 (P5(a5,a4)+P4(a2)+~P8(a2)), % 58.78/58.93 inference(scs_inference,[],[15,27])). % 58.78/58.93 cnf(55,plain, % 58.78/58.93 (P5(a5,a3)+P4(a2)+~P8(a2)), % 58.78/58.93 inference(scs_inference,[],[15,28])). % 58.78/58.93 cnf(56,plain, % 58.78/58.93 (P6(a5,a7)+P4(a2)+~P8(a2)), % 58.78/58.93 inference(scs_inference,[],[15,29])). % 58.78/58.93 cnf(57,plain, % 58.78/58.93 (P6(a5,a6)+P4(a2)+~P8(a2)), % 58.78/58.93 inference(scs_inference,[],[15,30])). % 58.78/58.93 cnf(58,plain, % 58.78/58.93 (P6(a5,a8)+P4(a2)+~P8(a2)), % 58.78/58.93 inference(scs_inference,[],[15,31])). % 58.78/58.93 cnf(59,plain, % 58.78/58.93 (P5(a5,a4)+P8(a2)+~P4(a2)), % 58.78/58.93 inference(scs_inference,[],[15,32])). % 58.78/58.93 cnf(60,plain, % 58.78/58.93 (P5(a5,a3)+P8(a2)+~P4(a2)), % 58.78/58.93 inference(scs_inference,[],[15,33])). % 58.78/58.93 cnf(61,plain, % 58.78/58.93 (P6(a5,a7)+P8(a2)+~P4(a2)), % 58.78/58.93 inference(scs_inference,[],[15,34])). % 58.78/58.93 cnf(62,plain, % 58.78/58.93 (P6(a5,a6)+P8(a2)+~P4(a2)), % 58.78/58.93 inference(scs_inference,[],[15,35])). % 58.78/58.93 cnf(63,plain, % 58.78/58.93 (P6(a5,a8)+P8(a2)+~P4(a2)), % 58.78/58.93 inference(scs_inference,[],[15,36])). % 58.78/58.93 cnf(64,plain, % 58.78/58.93 (E(x641,x642)+E(x641,x643)+E(x644,x643)+E(x644,x642)+E(x643,x645)+E(x641,x645)+E(x644,x645)+E(x643,x642)+E(x644,x641)+E(x642,x645)+~P7(a5,x645)+~P7(a5,x642)+~P7(a5,x643)+~P7(a5,x641)+~P7(a5,x644)+P4(a2)+~P8(a2)), % 58.78/58.93 inference(scs_inference,[],[15,41])). % 58.78/58.93 cnf(65,plain, % 58.78/58.93 (E(x651,x652)+E(x651,x653)+E(x654,x653)+E(x654,x652)+E(x653,x655)+E(x651,x655)+E(x654,x655)+E(x653,x652)+E(x654,x651)+E(x652,x655)+~P7(a5,x655)+~P7(a5,x652)+~P7(a5,x653)+~P7(a5,x651)+~P7(a5,x654)+P8(a2)+~P4(a2)), % 58.78/58.94 inference(scs_inference,[],[15,42])). % 58.78/58.94 cnf(67,plain, % 58.78/58.94 (~P3(x671)+~P5(x672,x671)), % 58.78/58.94 inference(scs_inference,[],[25,37])). % 58.78/58.94 cnf(83,plain, % 58.78/58.94 (~E(x831,x832)+~P3(x832)+P3(x831)), % 58.78/58.94 inference(scs_inference,[],[13,2])). % 58.78/58.94 cnf(85,plain, % 58.78/58.94 (~E(a7,a8)+P4(a2)+~P8(a2)), % 58.78/58.94 inference(scs_inference,[],[46,2])). % 58.78/58.94 cnf(86,plain, % 58.78/58.94 (~E(a4,a3)+P4(a2)+~P8(a2)), % 58.78/58.94 inference(scs_inference,[],[47,2])). % 58.78/58.94 cnf(87,plain, % 58.78/58.94 (~E(a7,a6)+P4(a2)+~P8(a2)), % 58.78/58.94 inference(scs_inference,[],[48,2])). % 58.78/58.94 cnf(88,plain, % 58.78/58.94 (~E(a6,a8)+P4(a2)+~P8(a2)), % 58.78/58.94 inference(scs_inference,[],[49,2])). % 58.78/58.94 cnf(96,plain, % 58.78/58.94 (P7(a5,a3)+P4(a2)+~P8(a2)), % 58.78/58.94 inference(scs_inference,[],[55,39])). % 58.78/58.94 cnf(97,plain, % 58.78/58.94 (P7(a5,a7)+P4(a2)+~P8(a2)), % 58.78/58.94 inference(scs_inference,[],[56,40])). % 58.78/58.94 cnf(104,plain, % 58.78/58.94 (P7(a5,a7)+P8(a2)+~P4(a2)), % 58.78/58.94 inference(scs_inference,[],[61,40])). % 58.78/58.94 cnf(108,plain, % 58.78/58.94 (~P8(a2)+~E(a7,a8)), % 58.78/58.94 inference(scs_inference,[],[85,26])). % 58.78/58.94 cnf(111,plain, % 58.78/58.94 (~P8(a2)+~E(a4,a3)), % 58.78/58.94 inference(scs_inference,[],[86,26])). % 58.78/58.94 cnf(114,plain, % 58.78/58.94 (~P8(a2)+~E(a7,a6)), % 58.78/58.94 inference(scs_inference,[],[87,26])). % 58.78/58.94 cnf(117,plain, % 58.78/58.94 (~P8(a2)+~E(a6,a8)), % 58.78/58.94 inference(scs_inference,[],[88,26])). % 58.78/58.94 cnf(118,plain, % 58.78/58.94 (~E(a8,a6)+~P8(a2)), % 58.78/58.94 inference(scs_inference,[],[117,2])). % 58.78/58.94 cnf(127,plain, % 58.78/58.94 (~P8(a2)+P7(a5,a3)), % 58.78/58.94 inference(scs_inference,[],[96,26])). % 58.78/58.94 cnf(130,plain, % 58.78/58.94 (~P8(a2)+P7(a5,a7)), % 58.78/58.94 inference(scs_inference,[],[97,26])). % 58.78/58.94 cnf(186,plain, % 58.78/58.94 (P4(a2)+~E(a7,a8)), % 58.78/58.94 inference(scs_inference,[],[16,108])). % 58.78/58.94 cnf(224,plain, % 58.78/58.94 (~E(a3,a4)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[16,50])). % 58.78/58.94 cnf(239,plain, % 58.78/58.94 (~E(a6,a7)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[16,51])). % 58.78/58.94 cnf(265,plain, % 58.78/58.94 (~E(a8,a7)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[16,52])). % 58.78/58.94 cnf(266,plain, % 58.78/58.94 (~E(a7,a8)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[265,2])). % 58.78/58.94 cnf(267,plain, % 58.78/58.94 (~E(x2671,a8)+~E(a7,x2671)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[266,3])). % 58.78/58.94 cnf(268,plain, % 58.78/58.94 (~E(x2681,a7)+~E(x2681,a8)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[267,2])). % 58.78/58.94 cnf(269,plain, % 58.78/58.94 (~E(a8,x2691)+~E(x2691,a7)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[268,2])). % 58.78/58.94 cnf(270,plain, % 58.78/58.94 (~E(a7,x2701)+~E(a8,x2701)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[269,2])). % 58.78/58.94 cnf(271,plain, % 58.78/58.94 (~P4(a2)+~E(a8,x2711)+~E(a7,x2711)), % 58.78/58.94 inference(scs_inference,[],[270,26])). % 58.78/58.94 cnf(272,plain, % 58.78/58.94 (~E(x2721,a7)+~E(a8,x2721)+~P4(a2)), % 58.78/58.94 inference(scs_inference,[],[271,2])). % 58.78/58.94 cnf(273,plain, % 58.78/58.94 (~E(x2731,a8)+~E(x2731,a7)+~P4(a2)), % 58.78/58.94 inference(scs_inference,[],[272,2])). % 58.78/58.94 cnf(274,plain, % 58.78/58.94 (~E(a7,x2741)+~E(x2741,a8)+~P4(a2)), % 58.78/58.94 inference(scs_inference,[],[273,2])). % 58.78/58.94 cnf(275,plain, % 58.78/58.94 (~E(a7,a8)+~E(x2751,a8)+~E(a7,x2751)), % 58.78/58.94 inference(scs_inference,[],[274,186])). % 58.78/58.94 cnf(276,plain, % 58.78/58.94 (~E(a8,a7)), % 58.78/58.94 inference(scs_inference,[],[275,2])). % 58.78/58.94 cnf(280,plain, % 58.78/58.94 (~E(a8,a6)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[16,53])). % 58.78/58.94 cnf(290,plain, % 58.78/58.94 (P5(a5,a4)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[16,59])). % 58.78/58.94 cnf(291,plain, % 58.78/58.94 (P2(a4)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[290,37])). % 58.78/58.94 cnf(297,plain, % 58.78/58.94 (P5(a5,a3)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[16,60])). % 58.78/58.94 cnf(298,plain, % 58.78/58.94 (P7(a5,a3)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[297,39])). % 58.78/58.94 cnf(301,plain, % 58.78/58.94 (P5(a5,a4)+P4(a2)), % 58.78/58.94 inference(scs_inference,[],[16,54])). % 58.78/58.94 cnf(305,plain, % 58.78/58.94 (P6(a5,a7)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[16,61])). % 58.78/58.94 cnf(306,plain, % 58.78/58.94 (P3(a7)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[305,38])). % 58.78/58.94 cnf(311,plain, % 58.78/58.94 (P5(a5,a3)+P4(a2)), % 58.78/58.94 inference(scs_inference,[],[16,55])). % 58.78/58.94 cnf(315,plain, % 58.78/58.94 (P6(a5,a6)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[16,62])). % 58.78/58.94 cnf(316,plain, % 58.78/58.94 (P7(a5,a6)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[315,40])). % 58.78/58.94 cnf(319,plain, % 58.78/58.94 (P6(a5,a7)+P4(a2)), % 58.78/58.94 inference(scs_inference,[],[16,56])). % 58.78/58.94 cnf(324,plain, % 58.78/58.94 (P6(a5,a8)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[16,63])). % 58.78/58.94 cnf(325,plain, % 58.78/58.94 (P3(a8)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[324,38])). % 58.78/58.94 cnf(329,plain, % 58.78/58.94 (P6(a5,a6)+P4(a2)), % 58.78/58.94 inference(scs_inference,[],[16,57])). % 58.78/58.94 cnf(333,plain, % 58.78/58.94 (P7(a5,a7)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[16,104])). % 58.78/58.94 cnf(336,plain, % 58.78/58.94 (P6(a5,a8)+P4(a2)), % 58.78/58.94 inference(scs_inference,[],[16,58])). % 58.78/58.94 cnf(351,plain, % 58.78/58.94 (~P2(x3511)+~E(x3512,x3511)+~P3(x3512)), % 58.78/58.94 inference(scs_inference,[],[25,13])). % 58.78/58.94 cnf(353,plain, % 58.78/58.94 (~E(x3531,x3532)+~P3(x3532)+~P2(x3531)), % 58.78/58.94 inference(scs_inference,[],[25,14])). % 58.78/58.94 cnf(355,plain, % 58.78/58.94 (~P8(a2)+P5(a5,a4)), % 58.78/58.94 inference(scs_inference,[],[26,301])). % 58.78/58.94 cnf(365,plain, % 58.78/58.94 (~P8(a2)+P5(a5,a3)), % 58.78/58.94 inference(scs_inference,[],[26,311])). % 58.78/58.94 cnf(366,plain, % 58.78/58.94 (P2(a3)+~P8(a2)), % 58.78/58.94 inference(scs_inference,[],[365,37])). % 58.78/58.94 cnf(377,plain, % 58.78/58.94 (~P8(a2)+P6(a5,a7)), % 58.78/58.94 inference(scs_inference,[],[26,319])). % 58.78/58.94 cnf(378,plain, % 58.78/58.94 (P3(a7)+~P8(a2)), % 58.78/58.94 inference(scs_inference,[],[377,38])). % 58.78/58.94 cnf(383,plain, % 58.78/58.94 (~P4(a2)+~E(a7,a8)), % 58.78/58.94 inference(scs_inference,[],[26,266])). % 58.78/58.94 cnf(384,plain, % 58.78/58.94 (~E(a7,a8)), % 58.78/58.94 inference(scs_inference,[],[383,186])). % 58.78/58.94 cnf(385,plain, % 58.78/58.94 (~P8(a2)+P6(a5,a6)), % 58.78/58.94 inference(scs_inference,[],[26,329])). % 58.78/58.94 cnf(386,plain, % 58.78/58.94 (P7(a5,a6)+~P8(a2)), % 58.78/58.94 inference(scs_inference,[],[385,40])). % 58.78/58.94 cnf(397,plain, % 58.78/58.94 (~P8(a2)+P6(a5,a8)), % 58.78/58.94 inference(scs_inference,[],[26,336])). % 58.78/58.94 cnf(398,plain, % 58.78/58.94 (P3(a8)+~P8(a2)), % 58.78/58.94 inference(scs_inference,[],[397,38])). % 58.78/58.94 cnf(446,plain, % 58.78/58.94 (~P4(a2)+P6(a5,a6)), % 58.78/58.94 inference(scs_inference,[],[26,315])). % 58.78/58.94 cnf(447,plain, % 58.78/58.94 (P3(a6)+~P4(a2)), % 58.78/58.94 inference(scs_inference,[],[446,38])). % 58.78/58.94 cnf(549,plain, % 58.78/58.94 (P5(a5,a4)+P2(a4)), % 58.78/58.94 inference(scs_inference,[],[291,355])). % 58.78/58.94 cnf(550,plain, % 58.78/58.94 (P2(a4)), % 58.78/58.94 inference(scs_inference,[],[549,37])). % 58.78/58.94 cnf(551,plain, % 58.78/58.94 (~P3(a4)), % 58.78/58.94 inference(scs_inference,[],[550,25])). % 58.78/58.94 cnf(611,plain, % 58.78/58.94 (P3(a7)), % 58.78/58.94 inference(scs_inference,[],[306,378])). % 58.78/58.94 cnf(614,plain, % 58.78/58.94 (~E(a4,a7)), % 58.78/58.94 inference(scs_inference,[],[611,551,67,83])). % 58.78/58.94 cnf(615,plain, % 58.78/58.94 (~E(a7,a4)), % 58.78/58.94 inference(scs_inference,[],[550,611,551,67,83,351])). % 58.78/58.94 cnf(703,plain, % 58.78/58.94 (P3(a8)), % 58.78/58.94 inference(scs_inference,[],[325,398])). % 58.78/58.94 cnf(706,plain, % 58.78/58.94 (~E(a4,a8)), % 58.78/58.94 inference(scs_inference,[],[550,703,67,353])). % 58.78/58.94 cnf(708,plain, % 58.78/58.94 (~E(a8,a4)), % 58.78/58.94 inference(scs_inference,[],[550,703,67,353,351])). % 58.78/58.94 cnf(852,plain, % 58.78/58.94 (P5(a5,a3)+P2(a3)), % 58.78/58.94 inference(scs_inference,[],[366,297])). % 58.78/58.94 cnf(853,plain, % 58.78/58.94 (P2(a3)), % 58.78/58.94 inference(scs_inference,[],[852,37])). % 58.78/58.94 cnf(867,plain, % 58.78/58.94 (~E(a3,a7)), % 58.78/58.94 inference(scs_inference,[],[853,611,353])). % 58.78/58.94 cnf(869,plain, % 58.78/58.94 (~E(a7,a3)), % 58.78/58.94 inference(scs_inference,[],[853,611,353,351])). % 58.78/58.94 cnf(874,plain, % 58.78/58.94 (~E(a8,a3)), % 58.78/58.94 inference(scs_inference,[],[853,703,353,351])). % 58.78/58.94 cnf(946,plain, % 58.78/58.94 (P6(a5,a6)+P3(a6)), % 58.78/58.94 inference(scs_inference,[],[447,329])). % 58.78/58.94 cnf(947,plain, % 58.78/58.94 (P3(a6)), % 58.78/58.94 inference(scs_inference,[],[946,38])). % 58.78/58.94 cnf(948,plain, % 58.78/58.94 (~E(a4,a6)), % 58.78/58.94 inference(scs_inference,[],[550,947,353])). % 58.78/58.94 cnf(950,plain, % 58.78/58.94 (~E(a6,a4)), % 58.78/58.94 inference(scs_inference,[],[550,947,353,351])). % 58.78/58.94 cnf(958,plain, % 58.78/58.94 (~E(a3,a6)), % 58.78/58.94 inference(scs_inference,[],[853,947,353])). % 58.78/58.94 cnf(960,plain, % 58.78/58.94 (~E(a6,a3)), % 58.78/58.94 inference(scs_inference,[],[853,947,353,351])). % 58.78/58.94 cnf(968,plain, % 58.78/58.94 (~E(a3,a4)+~E(a4,a3)), % 58.78/58.94 inference(scs_inference,[],[111,224])). % 58.78/58.94 cnf(969,plain, % 58.78/58.94 (~E(a4,a3)), % 58.78/58.94 inference(scs_inference,[],[968,2])). % 58.78/58.94 cnf(974,plain, % 58.78/58.94 (~E(a6,a7)+~E(a7,a6)), % 58.78/58.94 inference(scs_inference,[],[114,239])). % 58.78/58.94 cnf(975,plain, % 58.78/58.94 (~E(a7,a6)), % 58.78/58.94 inference(scs_inference,[],[974,2])). % 58.78/58.94 cnf(980,plain, % 58.78/58.94 (~E(a8,a6)+~E(a6,a8)), % 58.78/58.94 inference(scs_inference,[],[117,280])). % 58.78/58.94 cnf(981,plain, % 58.78/58.94 (~E(a6,a8)), % 58.78/58.94 inference(scs_inference,[],[980,2])). % 58.78/58.94 cnf(987,plain, % 58.78/58.94 (~E(a8,a6)), % 58.78/58.94 inference(scs_inference,[],[118,280])). % 58.78/58.94 cnf(996,plain, % 58.78/58.94 (P7(a5,a3)), % 58.78/58.94 inference(scs_inference,[],[127,298])). % 58.78/58.94 cnf(1013,plain, % 58.78/58.94 (P7(a5,a7)), % 58.78/58.94 inference(scs_inference,[],[130,333])). % 58.78/58.94 cnf(1018,plain, % 58.78/58.94 (P5(a5,a4)), % 58.78/58.94 inference(scs_inference,[],[290,355])). % 58.78/58.94 cnf(1019,plain, % 58.78/58.94 (P5(x10191,a4)+~E(a5,x10191)), % 58.78/58.94 inference(scs_inference,[],[1018,11])). % 58.78/58.94 cnf(1030,plain, % 58.78/58.94 (P7(a5,a6)), % 58.78/58.94 inference(scs_inference,[],[316,386])). % 58.78/58.94 cnf(1035,plain, % 58.78/58.94 (P6(a5,a8)), % 58.78/58.94 inference(scs_inference,[],[324,397])). % 58.78/58.94 cnf(1036,plain, % 58.78/58.94 (P6(x10361,a8)+~E(a5,x10361)), % 58.78/58.94 inference(scs_inference,[],[1035,9])). % 58.78/58.94 cnf(1171,plain, % 58.78/58.94 (P7(x11711,a4)+~E(a5,x11711)), % 58.78/58.94 inference(scs_inference,[],[39,1019])). % 58.78/58.94 cnf(1172,plain, % 58.78/58.94 (P7(a5,a4)), % 58.78/58.94 inference(equality_inference,[],[1171])). % 58.78/58.94 cnf(1176,plain, % 58.78/58.94 (P7(x11761,a8)+~E(a5,x11761)), % 58.78/58.94 inference(scs_inference,[],[40,1036])). % 58.78/58.94 cnf(1177,plain, % 58.78/58.94 (P7(a5,a8)), % 58.78/58.94 inference(equality_inference,[],[1176])). % 58.78/58.94 cnf(1302,plain, % 58.78/58.94 (~P8(a2)+P4(a2)), % 58.78/58.94 inference(scs_inference,[],[615,869,874,950,960,969,975,981,384,706,1177,1172,1030,1013,996,64])). % 58.78/58.94 cnf(1305,plain, % 58.78/58.94 (P4(a2)), % 58.78/58.94 inference(scs_inference,[],[1302,16])). % 58.78/58.94 cnf(1306,plain, % 58.78/58.94 (E(x13061,x13062)+E(x13063,x13064)+E(x13065,x13061)+E(x13063,x13062)+E(x13064,x13062)+E(x13063,x13061)+E(x13064,x13061)+E(x13064,x13065)+E(x13063,x13065)+E(x13065,x13062)+~P7(a5,x13063)+~P7(a5,x13064)+~P7(a5,x13065)+~P7(a5,x13061)+~P7(a5,x13062)+P8(a2)), % 58.78/58.94 inference(scs_inference,[],[1305,65])). % 58.78/58.94 cnf(1310,plain, % 58.78/58.94 (~P8(a2)), % 58.78/58.94 inference(scs_inference,[],[1305,26])). % 58.78/58.94 cnf(1333,plain, % 58.78/58.94 (E(x13331,x13332)+E(x13333,x13332)+E(x13331,x13334)+E(x13333,x13334)+E(x13333,x13335)+E(x13331,x13335)+E(x13335,x13332)+E(x13334,x13332)+E(x13331,x13333)+E(x13335,x13334)+~P7(a5,x13334)+~P7(a5,x13332)+~P7(a5,x13335)+~P7(a5,x13333)+~P7(a5,x13331)), % 58.78/58.94 inference(scs_inference,[],[1310,1306])). % 58.78/58.94 cnf(1344,plain, % 58.78/58.94 ($false), % 58.78/58.94 inference(scs_inference,[],[708,867,948,958,975,987,276,874,969,614,1172,1030,1013,996,1177,1333]), % 58.78/58.94 ['proof']). % 58.78/58.94 % SZS output end Proof % 58.78/58.94 % Total time :58.210000s %------------------------------------------------------------------------------