%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS145+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 : n032.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:39 EDT 2024 % Result : Theorem 10.23s 10.34s % Output : CNFRefutation 10.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : KRS145+1 : TPTP v8.2.0. Released v3.1.0. % 0.00/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.08/0.28 % Computer : n032.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.12/0.28 % WCLimit : 300 % 0.12/0.28 % DateTime : Wed Jun 19 13:44:38 EDT 2024 % 0.12/0.28 % CPUTime : % 0.14/0.46 start to proof:theBenchmark % 10.23/10.33 %------------------------------------------- % 10.23/10.33 % File :CSE---1.7 % 10.23/10.33 % Problem :theBenchmark % 10.23/10.33 % Transform :cnf % 10.23/10.33 % Format :tptp:raw % 10.23/10.33 % Command :java -jar mcs_scs.jar %d %s % 10.23/10.33 % 10.23/10.33 % Result :Theorem 9.830000s % 10.23/10.33 % Output :CNFRefutation 9.830000s % 10.23/10.33 %------------------------------------------- % 10.23/10.33 %------------------------------------------------------------------------------ % 10.23/10.33 % File : KRS145+1 : TPTP v8.2.0. Released v3.1.0. % 10.23/10.33 % Domain : Knowledge Representation (Semantic Web) % 10.23/10.33 % Problem : An owl:cardinality constraint is simply shorthand % 10.23/10.33 % Version : Especial. % 10.23/10.33 % English : An owl:cardinality constraint is simply shorthand for a pair of % 10.23/10.33 % owl:minCardinality and owl:maxCardinality constraints. % 10.23/10.33 % 10.23/10.33 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 10.23/10.33 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 10.23/10.33 % Source : [Bec03] % 10.23/10.33 % Names : positive_cardinality-Manifest004 [Bec03] % 10.23/10.33 % 10.23/10.33 % Status : Theorem % 10.23/10.33 % Rating : 0.11 v8.2.0, 0.08 v8.1.0, 0.03 v7.2.0, 0.00 v6.4.0, 0.04 v6.3.0, 0.00 v6.1.0, 0.10 v6.0.0, 0.13 v5.5.0, 0.19 v5.4.0, 0.21 v5.3.0, 0.22 v5.2.0, 0.05 v5.1.0, 0.10 v5.0.0, 0.12 v4.1.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.21 v3.7.0, 0.00 v3.3.0, 0.11 v3.2.0, 0.22 v3.1.0 % 10.23/10.33 % Syntax : Number of formulae : 11 ( 0 unt; 0 def) % 10.23/10.33 % Number of atoms : 49 ( 15 equ) % 10.23/10.33 % Maximal formula atoms : 14 ( 4 avg) % 10.23/10.33 % Number of connectives : 44 ( 6 ~; 4 |; 21 &) % 10.23/10.33 % ( 2 <=>; 11 =>; 0 <=; 0 <~>) % 10.23/10.33 % Maximal formula depth : 12 ( 6 avg) % 10.23/10.33 % Maximal term depth : 1 ( 1 avg) % 10.23/10.33 % Number of predicates : 7 ( 6 usr; 0 prp; 1-2 aty) % 10.23/10.33 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 10.23/10.33 % Number of variables : 32 ( 28 !; 4 ?) % 10.23/10.33 % SPC : FOF_THM_RFO_SEQ % 10.23/10.33 % 10.23/10.34 % Comments : Sean Bechhofer says there are some errors in the encoding of % 10.23/10.34 % datatypes, so this problem may not be perfect. At least it's % 10.23/10.34 % still representative of the type of reasoning required for OWL. % 10.23/10.34 %------------------------------------------------------------------------------ % 10.23/10.34 fof(cc_substitution_1,axiom, % 10.23/10.34 ! [A,B] : % 10.23/10.34 ( ( A = B % 10.23/10.34 & cc(A) ) % 10.23/10.34 => cc(B) ) ). % 10.23/10.34 % 10.23/10.34 fof(cowlNothing_substitution_1,axiom, % 10.23/10.34 ! [A,B] : % 10.23/10.34 ( ( A = B % 10.23/10.34 & cowlNothing(A) ) % 10.23/10.34 => cowlNothing(B) ) ). % 10.23/10.34 % 10.23/10.34 fof(cowlThing_substitution_1,axiom, % 10.23/10.34 ! [A,B] : % 10.23/10.34 ( ( A = B % 10.23/10.34 & cowlThing(A) ) % 10.23/10.34 => cowlThing(B) ) ). % 10.23/10.34 % 10.23/10.34 fof(rp_substitution_1,axiom, % 10.23/10.34 ! [A,B,C] : % 10.23/10.34 ( ( A = B % 10.23/10.34 & rp(A,C) ) % 10.23/10.34 => rp(B,C) ) ). % 10.23/10.34 % 10.23/10.34 fof(rp_substitution_2,axiom, % 10.23/10.34 ! [A,B,C] : % 10.23/10.34 ( ( A = B % 10.23/10.34 & rp(C,A) ) % 10.23/10.34 => rp(C,B) ) ). % 10.23/10.34 % 10.23/10.34 fof(xsd_integer_substitution_1,axiom, % 10.23/10.34 ! [A,B] : % 10.23/10.34 ( ( A = B % 10.23/10.34 & xsd_integer(A) ) % 10.23/10.34 => xsd_integer(B) ) ). % 10.23/10.34 % 10.23/10.34 fof(xsd_string_substitution_1,axiom, % 10.23/10.34 ! [A,B] : % 10.23/10.34 ( ( A = B % 10.23/10.34 & xsd_string(A) ) % 10.23/10.34 => xsd_string(B) ) ). % 10.23/10.34 % 10.23/10.34 %----Thing and Nothing % 10.23/10.34 fof(axiom_0,axiom, % 10.23/10.34 ! [X] : % 10.23/10.34 ( cowlThing(X) % 10.23/10.34 & ~ cowlNothing(X) ) ). % 10.23/10.34 % 10.23/10.34 %----String and Integer disjoint % 10.23/10.34 fof(axiom_1,axiom, % 10.23/10.34 ! [X] : % 10.23/10.34 ( xsd_string(X) % 10.23/10.34 <=> ~ xsd_integer(X) ) ). % 10.23/10.34 % 10.23/10.34 %----Super cc % 10.23/10.34 fof(axiom_2,axiom, % 10.23/10.34 ! [X] : % 10.23/10.34 ( cc(X) % 10.23/10.34 => ( ! [Y0,Y1,Y2] : % 10.23/10.34 ( ( rp(X,Y0) % 10.23/10.34 & rp(X,Y1) % 10.23/10.34 & rp(X,Y2) ) % 10.23/10.34 => ( Y0 = Y1 % 10.23/10.34 | Y0 = Y2 % 10.23/10.34 | Y1 = Y2 ) ) % 10.23/10.34 & ? [Y0,Y1] : % 10.23/10.34 ( rp(X,Y0) % 10.23/10.34 & rp(X,Y1) % 10.23/10.34 & Y0 != Y1 ) ) ) ). % 10.23/10.34 % 10.23/10.34 %----Thing and Nothing % 10.23/10.34 %----String and Integer disjoint % 10.23/10.34 %----Super cc % 10.23/10.34 fof(the_axiom,conjecture, % 10.23/10.34 ( ! [X] : % 10.23/10.34 ( cowlThing(X) % 10.23/10.34 & ~ cowlNothing(X) ) % 10.23/10.34 & ! [X] : % 10.23/10.34 ( xsd_string(X) % 10.23/10.34 <=> ~ xsd_integer(X) ) % 10.23/10.34 & ! [X] : % 10.23/10.34 ( cc(X) % 10.23/10.34 => ( ? [Y0,Y1] : % 10.23/10.34 ( rp(X,Y0) % 10.23/10.34 & rp(X,Y1) % 10.23/10.34 & Y0 != Y1 ) % 10.23/10.34 & ! [Y0,Y1,Y2] : % 10.23/10.34 ( ( rp(X,Y0) % 10.23/10.34 & rp(X,Y1) % 10.23/10.34 & rp(X,Y2) ) % 10.23/10.34 => ( Y0 = Y1 % 10.23/10.34 | Y0 = Y2 % 10.23/10.34 | Y1 = Y2 ) ) ) ) ) ). % 10.23/10.34 % 10.23/10.34 %------------------------------------------------------------------------------ % 10.23/10.34 %------------------------------------------- % 10.23/10.34 % Proof found % 10.23/10.34 % SZS status Theorem for theBenchmark % 10.23/10.34 % SZS output start Proof % 10.23/10.34 %ClaNum:32(EqnAxiom:11) % 10.23/10.34 %VarNum:75(SingletonVarNum:34) % 10.23/10.34 %MaxLitNum:7 % 10.23/10.34 %MaxfuncDepth:1 % 10.23/10.34 %SharedTerms:18 % 10.23/10.34 %goalClause: 14 15 20 21 22 23 24 25 26 27 28 29 30 31 % 10.23/10.34 [12]~P1(x121) % 10.23/10.34 [13]P5(x131)+P3(x131) % 10.23/10.34 [16]~P5(x161)+~P3(x161) % 10.23/10.34 [17]~P2(x171)+~E(f3(x171),f4(x171)) % 10.23/10.34 [18]~P2(x181)+P4(x181,f4(x181)) % 10.23/10.34 [19]~P2(x191)+P4(x191,f3(x191)) % 10.23/10.34 [14]P2(a1)+P1(a2)+P3(a5)+~P5(a5) % 10.23/10.34 [15]P2(a1)+P1(a2)+P5(a5)+~P3(a5) % 10.23/10.34 [20]E(x201,x202)+~P4(a1,x202)+~P4(a1,x201)+P1(a2)+P3(a5)+~E(a6,a7)+~P5(a5) % 10.23/10.34 [21]E(x211,x212)+~P4(a1,x212)+~P4(a1,x211)+P1(a2)+P3(a5)+~E(a8,a7)+~P5(a5) % 10.23/10.34 [22]E(x221,x222)+~P4(a1,x222)+~P4(a1,x221)+P1(a2)+P3(a5)+~E(a8,a6)+~P5(a5) % 10.23/10.34 [23]E(x231,x232)+~E(a6,a7)+~P4(a1,x232)+~P4(a1,x231)+P1(a2)+P5(a5)+~P3(a5) % 10.23/10.34 [24]E(x241,x242)+~E(a8,a7)+~P4(a1,x242)+~P4(a1,x241)+P1(a2)+P5(a5)+~P3(a5) % 10.23/10.34 [25]E(x251,x252)+~E(a8,a6)+~P4(a1,x252)+~P4(a1,x251)+P1(a2)+P5(a5)+~P3(a5) % 10.23/10.34 [26]E(x261,x262)+~P4(a1,x262)+~P4(a1,x261)+P1(a2)+P3(a5)+P4(a1,a7)+~P5(a5) % 10.23/10.34 [27]E(x271,x272)+~P4(a1,x272)+~P4(a1,x271)+P1(a2)+P3(a5)+P4(a1,a6)+~P5(a5) % 10.23/10.34 [28]E(x281,x282)+~P4(a1,x282)+~P4(a1,x281)+P1(a2)+P3(a5)+P4(a1,a8)+~P5(a5) % 10.23/10.34 [29]E(x291,x292)+P4(a1,a7)+~P4(a1,x292)+~P4(a1,x291)+P1(a2)+P5(a5)+~P3(a5) % 10.23/10.34 [30]E(x301,x302)+P4(a1,a6)+~P4(a1,x302)+~P4(a1,x301)+P1(a2)+P5(a5)+~P3(a5) % 10.23/10.34 [31]E(x311,x312)+P4(a1,a8)+~P4(a1,x312)+~P4(a1,x311)+P1(a2)+P5(a5)+~P3(a5) % 10.23/10.34 [32]E(x323,x321)+~P4(x324,x322)+~P4(x324,x321)+~P4(x324,x323)+E(x321,x322)+E(x323,x322)+~P2(x324) % 10.23/10.34 %EqnAxiom % 10.23/10.34 [1]E(x11,x11) % 10.23/10.34 [2]E(x22,x21)+~E(x21,x22) % 10.23/10.34 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 10.23/10.34 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 10.23/10.34 [5]~E(x51,x52)+E(f4(x51),f4(x52)) % 10.23/10.34 [6]~P1(x61)+P1(x62)+~E(x61,x62) % 10.23/10.34 [7]~P3(x71)+P3(x72)+~E(x71,x72) % 10.23/10.34 [8]~P5(x81)+P5(x82)+~E(x81,x82) % 10.23/10.34 [9]~P2(x91)+P2(x92)+~E(x91,x92) % 10.23/10.34 [10]P4(x102,x103)+~E(x101,x102)+~P4(x101,x103) % 10.23/10.34 [11]P4(x113,x112)+~E(x111,x112)+~P4(x113,x111) % 10.23/10.34 % 10.23/10.34 %------------------------------------------- % 10.23/10.34 cnf(33,plain, % 10.23/10.34 (~P1(x331)), % 10.23/10.34 inference(rename_variables,[],[12])). % 10.23/10.34 cnf(35,plain, % 10.23/10.34 (E(x351,x352)+~E(a8,a7)+~P4(a1,x351)+~P4(a1,x352)+P3(a5)+~P5(a5)), % 10.23/10.34 inference(scs_inference,[],[12,33,21])). % 10.23/10.34 cnf(36,plain, % 10.23/10.34 (P2(a1)+P3(a5)+~P5(a5)), % 10.23/10.34 inference(scs_inference,[],[12,14])). % 10.23/10.34 cnf(37,plain, % 10.23/10.34 (P2(a1)+P5(a5)+~P3(a5)), % 10.23/10.34 inference(scs_inference,[],[12,15])). % 10.23/10.34 cnf(38,plain, % 10.23/10.34 (E(x381,x382)+~P4(a1,x382)+~P4(a1,x381)+~E(a6,a7)+P3(a5)+~P5(a5)), % 10.23/10.34 inference(scs_inference,[],[12,20])). % 10.23/10.34 cnf(39,plain, % 10.23/10.34 (E(x391,x392)+~P4(a1,x392)+~P4(a1,x391)+~E(a8,a6)+P3(a5)+~P5(a5)), % 10.23/10.34 inference(scs_inference,[],[12,22])). % 10.23/10.34 cnf(40,plain, % 10.23/10.34 (E(x401,x402)+~E(a6,a7)+~P4(a1,x402)+~P4(a1,x401)+P5(a5)+~P3(a5)), % 10.23/10.34 inference(scs_inference,[],[12,23])). % 10.23/10.34 cnf(41,plain, % 10.23/10.34 (E(x411,x412)+~E(a8,a7)+~P4(a1,x412)+~P4(a1,x411)+P5(a5)+~P3(a5)), % 10.23/10.34 inference(scs_inference,[],[12,24])). % 10.23/10.34 cnf(42,plain, % 10.23/10.34 (E(x421,x422)+~E(a8,a6)+~P4(a1,x422)+~P4(a1,x421)+P5(a5)+~P3(a5)), % 10.23/10.34 inference(scs_inference,[],[12,25])). % 10.23/10.34 cnf(43,plain, % 10.23/10.34 (E(x431,x432)+~P4(a1,x432)+~P4(a1,x431)+P4(a1,a7)+P3(a5)+~P5(a5)), % 10.23/10.34 inference(scs_inference,[],[12,26])). % 10.23/10.34 cnf(44,plain, % 10.23/10.34 (E(x441,x442)+~P4(a1,x442)+~P4(a1,x441)+P4(a1,a6)+P3(a5)+~P5(a5)), % 10.23/10.34 inference(scs_inference,[],[12,27])). % 10.23/10.34 cnf(45,plain, % 10.23/10.34 (E(x451,x452)+~P4(a1,x452)+~P4(a1,x451)+P4(a1,a8)+P3(a5)+~P5(a5)), % 10.23/10.34 inference(scs_inference,[],[12,28])). % 10.23/10.34 cnf(46,plain, % 10.23/10.34 (E(x461,x462)+P4(a1,a7)+~P4(a1,x462)+~P4(a1,x461)+P5(a5)+~P3(a5)), % 10.23/10.34 inference(scs_inference,[],[12,29])). % 10.23/10.34 cnf(47,plain, % 10.23/10.34 (E(x471,x472)+P4(a1,a6)+~P4(a1,x472)+~P4(a1,x471)+P5(a5)+~P3(a5)), % 10.23/10.34 inference(scs_inference,[],[12,30])). % 10.23/10.34 cnf(48,plain, % 10.23/10.34 (E(x481,x482)+P4(a1,a8)+~P4(a1,x482)+~P4(a1,x481)+P5(a5)+~P3(a5)), % 10.23/10.34 inference(scs_inference,[],[12,31])). % 10.23/10.34 cnf(52,plain, % 10.23/10.34 (~E(x521,x522)+~P2(x521)+P4(x522,f4(x522))), % 10.23/10.34 inference(scs_inference,[],[18,9])). % 10.23/10.34 cnf(55,plain, % 10.23/10.34 (~E(f3(a1),f4(a1))+P5(a5)+~P3(a5)), % 10.23/10.34 inference(scs_inference,[],[17,37])). % 10.23/10.34 cnf(65,plain, % 10.23/10.34 (~E(x651,x652)+E(x653,x651)+~E(x653,x652)), % 10.23/10.34 inference(scs_inference,[],[3,2])). % 10.23/10.34 cnf(68,plain, % 10.23/10.34 (~E(f4(a1),f3(a1))+P5(a5)+~P3(a5)), % 10.23/10.34 inference(scs_inference,[],[55,2])). % 10.23/10.34 cnf(69,plain, % 10.23/10.34 (~E(x691,x692)+~E(x693,x691)+E(x692,x693)), % 10.23/10.34 inference(scs_inference,[],[65,2])). % 10.23/10.34 cnf(70,plain, % 10.23/10.35 (~P3(a5)+~E(f4(a1),f3(a1))), % 10.23/10.35 inference(scs_inference,[],[68,16])). % 10.23/10.35 cnf(71,plain, % 10.23/10.35 (~E(f3(a1),f4(a1))+~P3(a5)), % 10.23/10.35 inference(scs_inference,[],[70,2])). % 10.23/10.35 cnf(72,plain, % 10.23/10.35 (~E(x721,f3(a1))+~E(f4(a1),x721)+~P3(a5)), % 10.23/10.35 inference(scs_inference,[],[71,69])). % 10.23/10.35 cnf(87,plain, % 10.23/10.35 (P2(a1)+P3(a5)), % 10.23/10.35 inference(scs_inference,[],[13,36])). % 10.23/10.35 cnf(93,plain, % 10.23/10.35 (P2(a1)+P5(a5)), % 10.23/10.35 inference(scs_inference,[],[13,37])). % 10.23/10.35 cnf(97,plain, % 10.23/10.35 (P5(a5)+~E(f4(a1),x971)+~E(x971,f3(a1))), % 10.23/10.35 inference(scs_inference,[],[13,72])). % 10.23/10.35 cnf(98,plain, % 10.23/10.35 (~E(f3(a1),x981)+~E(f4(a1),x981)+P5(a5)), % 10.23/10.35 inference(scs_inference,[],[97,2])). % 10.23/10.35 cnf(99,plain, % 10.23/10.35 (~E(a1,x991)+~E(f3(a1),f4(x991))+P5(a5)), % 10.23/10.35 inference(scs_inference,[],[98,5])). % 10.23/10.35 cnf(100,plain, % 10.23/10.35 (~E(f4(x1001),f3(a1))+~E(a1,x1001)+P5(a5)), % 10.23/10.35 inference(scs_inference,[],[99,2])). % 10.23/10.35 cnf(107,plain, % 10.23/10.35 (~P3(a5)+P2(a1)), % 10.23/10.35 inference(scs_inference,[],[16,93])). % 10.23/10.35 cnf(127,plain, % 10.23/10.35 (P2(a1)), % 10.23/10.35 inference(scs_inference,[],[87,107])). % 10.23/10.35 cnf(128,plain, % 10.23/10.35 (P4(x1281,f4(x1281))+~E(a1,x1281)), % 10.23/10.35 inference(scs_inference,[],[127,52])). % 10.23/10.35 cnf(133,plain, % 10.23/10.35 (P4(a1,f4(a1))), % 10.23/10.35 inference(equality_inference,[],[128])). % 10.23/10.35 cnf(138,plain, % 10.23/10.35 (~E(f4(a1),f3(a1))), % 10.23/10.35 inference(scs_inference,[],[127,2,17])). % 10.23/10.35 cnf(152,plain, % 10.23/10.35 (~E(f3(a1),x1521)+~E(f4(a1),x1521)), % 10.23/10.35 inference(scs_inference,[],[138,2,65])). % 10.23/10.35 cnf(153,plain, % 10.23/10.35 (~E(f3(a1),f4(a1))), % 10.23/10.35 inference(scs_inference,[],[133,127,152,32])). % 10.23/10.35 cnf(154,plain, % 10.23/10.35 (~E(x1541,f3(a1))+~E(f4(a1),x1541)), % 10.23/10.35 inference(scs_inference,[],[153,69])). % 10.23/10.35 cnf(166,plain, % 10.23/10.35 (~E(x1661,a1)+P2(x1661)), % 10.23/10.35 inference(scs_inference,[],[127,2,9])). % 10.23/10.35 cnf(172,plain, % 10.23/10.35 (P4(x1721,f3(x1721))+~E(x1721,a1)), % 10.23/10.35 inference(scs_inference,[],[166,19])). % 10.23/10.35 cnf(173,plain, % 10.23/10.35 (P4(a1,f3(a1))), % 10.23/10.35 inference(equality_inference,[],[172])). % 10.23/10.35 cnf(186,plain, % 10.23/10.35 (~E(a8,a7)+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[138,173,133,2,35])). % 10.23/10.35 cnf(187,plain, % 10.23/10.35 (~E(a7,a8)+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[186,2])). % 10.23/10.35 cnf(188,plain, % 10.23/10.35 (~P5(a5)+~E(a7,a8)), % 10.23/10.35 inference(scs_inference,[],[187,16])). % 10.23/10.35 cnf(189,plain, % 10.23/10.35 (P3(a5)+~E(a7,a8)), % 10.23/10.35 inference(scs_inference,[],[188,13])). % 10.23/10.35 cnf(201,plain, % 10.23/10.35 (~E(a8,a7)+P3(a5)), % 10.23/10.35 inference(scs_inference,[],[189,2])). % 10.23/10.35 cnf(212,plain, % 10.23/10.35 (~E(a6,a7)+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[138,133,173,2,38])). % 10.23/10.35 cnf(213,plain, % 10.23/10.35 (~E(a7,a6)+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[212,2])). % 10.23/10.35 cnf(214,plain, % 10.23/10.35 (~P5(a5)+~E(a7,a6)), % 10.23/10.35 inference(scs_inference,[],[213,16])). % 10.23/10.35 cnf(215,plain, % 10.23/10.35 (P3(a5)+~E(a7,a6)), % 10.23/10.35 inference(scs_inference,[],[214,13])). % 10.23/10.35 cnf(227,plain, % 10.23/10.35 (~E(a6,a7)+P3(a5)), % 10.23/10.35 inference(scs_inference,[],[215,2])). % 10.23/10.35 cnf(238,plain, % 10.23/10.35 (~E(a8,a6)+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[138,133,173,2,39])). % 10.23/10.35 cnf(239,plain, % 10.23/10.35 (~E(a6,a8)+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[238,2])). % 10.23/10.35 cnf(240,plain, % 10.23/10.35 (~P5(a5)+~E(a6,a8)), % 10.23/10.35 inference(scs_inference,[],[239,16])). % 10.23/10.35 cnf(241,plain, % 10.23/10.35 (P3(a5)+~E(a6,a8)), % 10.23/10.35 inference(scs_inference,[],[240,13])). % 10.23/10.35 cnf(253,plain, % 10.23/10.35 (~E(a8,a6)+P3(a5)), % 10.23/10.35 inference(scs_inference,[],[241,2])). % 10.23/10.35 cnf(264,plain, % 10.23/10.35 (~E(a6,a7)+P5(a5)+~P3(a5)), % 10.23/10.35 inference(scs_inference,[],[138,133,173,2,40])). % 10.23/10.35 cnf(265,plain, % 10.23/10.35 (~E(a7,a6)+P5(a5)+~P3(a5)), % 10.23/10.35 inference(scs_inference,[],[264,2])). % 10.23/10.35 cnf(266,plain, % 10.23/10.35 (~P3(a5)+~E(a7,a6)), % 10.23/10.35 inference(scs_inference,[],[265,16])). % 10.23/10.35 cnf(267,plain, % 10.23/10.35 (~E(a6,a7)+~P3(a5)), % 10.23/10.35 inference(scs_inference,[],[266,2])). % 10.23/10.35 cnf(307,plain, % 10.23/10.35 (~E(a7,a6)), % 10.23/10.35 inference(scs_inference,[],[266,215])). % 10.23/10.35 cnf(315,plain, % 10.23/10.35 (~E(a6,a7)), % 10.23/10.35 inference(scs_inference,[],[267,227])). % 10.23/10.35 cnf(1261,plain, % 10.23/10.35 (~E(a8,a7)+P5(a5)+~P3(a5)), % 10.23/10.35 inference(scs_inference,[],[127,133,173,17,41])). % 10.23/10.35 cnf(1277,plain, % 10.23/10.35 (~E(a7,a8)+P5(a5)+~P3(a5)), % 10.23/10.35 inference(scs_inference,[],[1261,2])). % 10.23/10.35 cnf(1293,plain, % 10.23/10.35 (~P3(a5)+~E(a7,a8)), % 10.23/10.35 inference(scs_inference,[],[1277,16])). % 10.23/10.35 cnf(1309,plain, % 10.23/10.35 (~E(a8,a7)+~P3(a5)), % 10.23/10.35 inference(scs_inference,[],[1293,2])). % 10.23/10.35 cnf(1429,plain, % 10.23/10.35 (~E(a7,a8)), % 10.23/10.35 inference(scs_inference,[],[1293,189])). % 10.23/10.35 cnf(1526,plain, % 10.23/10.35 (~E(a8,a7)), % 10.23/10.35 inference(scs_inference,[],[1309,201])). % 10.23/10.35 cnf(2039,plain, % 10.23/10.35 (~E(a8,a6)+P5(a5)+~P3(a5)), % 10.23/10.35 inference(scs_inference,[],[127,133,173,17,42])). % 10.23/10.35 cnf(2055,plain, % 10.23/10.35 (~E(a6,a8)+P5(a5)+~P3(a5)), % 10.23/10.35 inference(scs_inference,[],[2039,2])). % 10.23/10.35 cnf(2071,plain, % 10.23/10.35 (~P3(a5)+~E(a6,a8)), % 10.23/10.35 inference(scs_inference,[],[2055,16])). % 10.23/10.35 cnf(2087,plain, % 10.23/10.35 (~E(a8,a6)+~P3(a5)), % 10.23/10.35 inference(scs_inference,[],[2071,2])). % 10.23/10.35 cnf(2258,plain, % 10.23/10.35 (~E(a6,a8)), % 10.23/10.35 inference(scs_inference,[],[2071,241])). % 10.23/10.35 cnf(2355,plain, % 10.23/10.35 (~E(a8,a6)), % 10.23/10.35 inference(scs_inference,[],[2087,253])). % 10.23/10.35 cnf(2929,plain, % 10.23/10.35 (P4(a1,a7)+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[127,133,173,17,43])). % 10.23/10.35 cnf(2945,plain, % 10.23/10.35 (~P5(a5)+P4(a1,a7)), % 10.23/10.35 inference(scs_inference,[],[2929,16])). % 10.23/10.35 cnf(2961,plain, % 10.23/10.35 (~P4(a1,a8)+~P4(a1,a6)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[2355,1526,307,127,2945,32])). % 10.23/10.35 cnf(3262,plain, % 10.23/10.35 (P4(a1,a6)+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[127,133,173,17,44])). % 10.23/10.35 cnf(3278,plain, % 10.23/10.35 (~P4(a1,a8)+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[3262,2961])). % 10.23/10.35 cnf(3294,plain, % 10.23/10.35 (~E(f4(a1),a8)+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[133,3278,11])). % 10.23/10.35 cnf(3310,plain, % 10.23/10.35 (~E(a8,f4(a1))+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[3294,2])). % 10.23/10.35 cnf(3326,plain, % 10.23/10.35 (~P5(a5)+~E(a8,f4(a1))), % 10.23/10.35 inference(scs_inference,[],[3310,16])). % 10.23/10.35 cnf(3495,plain, % 10.23/10.35 (~E(x34951,f4(a1))+~E(a8,x34951)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[3326,3])). % 10.23/10.35 cnf(4178,plain, % 10.23/10.35 (P4(a1,a8)+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[127,133,173,17,45])). % 10.23/10.35 cnf(4194,plain, % 10.23/10.35 (~P4(a1,a6)+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[4178,2961])). % 10.23/10.35 cnf(4210,plain, % 10.23/10.35 (~E(f4(a1),a6)+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[133,4194,11])). % 10.23/10.35 cnf(4226,plain, % 10.23/10.35 (~E(a6,f4(a1))+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[4210,2])). % 10.23/10.35 cnf(4242,plain, % 10.23/10.35 (~P5(a5)+~E(a6,f4(a1))), % 10.23/10.35 inference(scs_inference,[],[4226,16])). % 10.23/10.35 cnf(4384,plain, % 10.23/10.35 (~P4(a1,a6)+E(a6,f3(a1))+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[173,153,127,133,4242,32])). % 10.23/10.35 cnf(4400,plain, % 10.23/10.35 (E(a6,f3(a1))+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[4384,3262])). % 10.23/10.35 cnf(4416,plain, % 10.23/10.35 (~E(a8,f3(a1))+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[2355,4400,65])). % 10.23/10.35 cnf(4432,plain, % 10.23/10.35 (~P5(a5)+~E(a8,f3(a1))), % 10.23/10.35 inference(scs_inference,[],[4416,16])). % 10.23/10.35 cnf(5114,plain, % 10.23/10.35 (~P4(a1,a8)+E(a8,f4(a1))+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[133,138,127,173,4432,32])). % 10.23/10.35 cnf(5130,plain, % 10.23/10.35 (E(a8,f4(a1))+P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[5114,4178])). % 10.23/10.35 cnf(5146,plain, % 10.23/10.35 (P3(a5)+~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[5130,3495])). % 10.23/10.35 cnf(5162,plain, % 10.23/10.35 (~P5(a5)), % 10.23/10.35 inference(scs_inference,[],[5146,16])). % 10.23/10.35 cnf(5163,plain, % 10.23/10.35 (E(x51631,x51632)+P4(a1,a7)+~P4(a1,x51632)+~P4(a1,x51631)+~P3(a5)), % 10.23/10.35 inference(scs_inference,[],[5162,46])). % 10.23/10.35 cnf(5164,plain, % 10.23/10.35 (E(x51641,x51642)+P4(a1,a6)+~P4(a1,x51642)+~P4(a1,x51641)+~P3(a5)), % 10.23/10.35 inference(scs_inference,[],[5162,47])). % 10.23/10.35 cnf(5165,plain, % 10.23/10.35 (E(x51651,x51652)+P4(a1,a8)+~P4(a1,x51652)+~P4(a1,x51651)+~P3(a5)), % 10.23/10.35 inference(scs_inference,[],[5162,48])). % 10.23/10.35 cnf(5166,plain, % 10.23/10.35 (~E(f3(a1),f4(x51661))+~E(a1,x51661)), % 10.23/10.35 inference(scs_inference,[],[5162,99])). % 10.23/10.35 cnf(5167,plain, % 10.23/10.35 (~E(f4(x51671),f3(a1))+~E(a1,x51671)), % 10.23/10.35 inference(scs_inference,[],[5162,100])). % 10.23/10.35 cnf(5168,plain, % 10.23/10.35 (P3(a5)), % 10.23/10.35 inference(scs_inference,[],[5162,13])). % 10.23/10.35 cnf(5183,plain, % 10.23/10.35 (E(x51831,x51832)+P4(a1,a7)+~P4(a1,x51832)+~P4(a1,x51831)), % 10.23/10.35 inference(scs_inference,[],[5168,5163])). % 10.23/10.35 cnf(5184,plain, % 10.23/10.35 (E(x51841,x51842)+P4(a1,a6)+~P4(a1,x51842)+~P4(a1,x51841)), % 10.23/10.35 inference(scs_inference,[],[5168,5164])). % 10.23/10.35 cnf(5185,plain, % 10.23/10.35 (E(x51851,x51852)+P4(a1,a8)+~P4(a1,x51852)+~P4(a1,x51851)), % 10.23/10.35 inference(scs_inference,[],[5168,5165])). % 10.23/10.35 cnf(5219,plain, % 10.23/10.35 (P4(a1,a7)), % 10.23/10.35 inference(scs_inference,[],[173,133,154,5183])). % 10.23/10.35 cnf(5246,plain, % 10.23/10.35 (~P4(a1,a6)+~P4(a1,a8)), % 10.23/10.35 inference(scs_inference,[],[2258,127,5219,315,1429,32])). % 10.23/10.35 cnf(5373,plain, % 10.23/10.35 (P4(a1,a6)), % 10.23/10.35 inference(scs_inference,[],[133,173,5166,5184])). % 10.23/10.35 cnf(5389,plain, % 10.23/10.35 (~P4(a1,a8)), % 10.23/10.35 inference(scs_inference,[],[5373,5246])). % 10.23/10.35 cnf(5399,plain, % 10.23/10.35 (E(x53991,x53992)+~P4(a1,x53992)+~P4(a1,x53991)), % 10.23/10.35 inference(scs_inference,[],[5389,5185])). % 10.23/10.35 cnf(5464,plain, % 10.23/10.35 ($false), % 10.23/10.35 inference(scs_inference,[],[173,133,5167,5399]), % 10.23/10.35 ['proof']). % 10.23/10.35 % SZS output end Proof % 10.23/10.35 % Total time :9.830000s %------------------------------------------------------------------------------