%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS142+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 : n002.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 2.94s 2.99s % Output : CNFRefutation 2.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.14 % Problem : KRS142+1 : TPTP v8.2.0. Released v3.1.0. % 0.07/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.36 % Computer : n002.cluster.edu % 0.13/0.36 % Model : x86_64 x86_64 % 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.36 % Memory : 8042.1875MB % 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.36 % CPULimit : 300 % 0.13/0.36 % WCLimit : 300 % 0.13/0.36 % DateTime : Wed Jun 19 12:16:38 EDT 2024 % 0.13/0.36 % CPUTime : % 0.22/0.60 start to proof:theBenchmark % 2.94/2.98 %------------------------------------------- % 2.94/2.98 % File :CSE---1.7 % 2.94/2.98 % Problem :theBenchmark % 2.94/2.98 % Transform :cnf % 2.94/2.98 % Format :tptp:raw % 2.94/2.98 % Command :java -jar mcs_scs.jar %d %s % 2.94/2.98 % 2.94/2.98 % Result :Theorem 2.340000s % 2.94/2.98 % Output :CNFRefutation 2.340000s % 2.94/2.98 %------------------------------------------- % 2.94/2.98 %------------------------------------------------------------------------------ % 2.94/2.98 % File : KRS142+1 : TPTP v8.2.0. Released v3.1.0. % 2.94/2.98 % Domain : Knowledge Representation (Semantic Web) % 2.94/2.98 % Problem : An owl:cardinality constraint is simply shorthand % 2.94/2.98 % Version : Especial. % 2.94/2.98 % English : An owl:cardinality constraint is simply shorthand for a pair of % 2.94/2.98 % owl:minCardinality and owl:maxCardinality constraints. % 2.94/2.98 % 2.94/2.98 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 2.94/2.98 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 2.94/2.98 % Source : [Bec03] % 2.94/2.98 % Names : positive_cardinality-Manifest001 [Bec03] % 2.94/2.98 % 2.94/2.98 % Status : Theorem % 2.94/2.98 % Rating : 0.03 v8.1.0, 0.06 v7.4.0, 0.07 v7.2.0, 0.03 v7.1.0, 0.00 v7.0.0, 0.03 v6.4.0, 0.08 v6.3.0, 0.04 v6.2.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.04 v5.5.0, 0.11 v5.4.0, 0.14 v5.3.0, 0.15 v5.2.0, 0.00 v4.1.0, 0.04 v4.0.1, 0.09 v4.0.0, 0.08 v3.7.0, 0.00 v3.2.0, 0.11 v3.1.0 % 2.94/2.98 % Syntax : Number of formulae : 11 ( 0 unt; 0 def) % 2.94/2.98 % Number of atoms : 40 ( 9 equ) % 2.94/2.98 % Maximal formula atoms : 10 ( 3 avg) % 2.94/2.98 % Number of connectives : 33 ( 4 ~; 0 |; 15 &) % 2.94/2.98 % ( 2 <=>; 12 =>; 0 <=; 0 <~>) % 2.94/2.98 % Maximal formula depth : 10 ( 6 avg) % 2.94/2.98 % Maximal term depth : 1 ( 1 avg) % 2.94/2.98 % Number of predicates : 7 ( 6 usr; 0 prp; 1-2 aty) % 2.94/2.98 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 2.94/2.98 % Number of variables : 29 ( 27 !; 2 ?) % 2.94/2.98 % SPC : FOF_THM_RFO_SEQ % 2.94/2.98 % 2.94/2.98 % Comments : Sean Bechhofer says there are some errors in the encoding of % 2.94/2.98 % datatypes, so this problem may not be perfect. At least it's % 2.94/2.98 % still representative of the type of reasoning required for OWL. % 2.94/2.98 %------------------------------------------------------------------------------ % 2.94/2.98 fof(cc_substitution_1,axiom, % 2.94/2.98 ! [A,B] : % 2.94/2.98 ( ( A = B % 2.94/2.98 & cc(A) ) % 2.94/2.98 => cc(B) ) ). % 2.94/2.98 % 2.94/2.98 fof(cowlNothing_substitution_1,axiom, % 2.94/2.98 ! [A,B] : % 2.94/2.98 ( ( A = B % 2.94/2.98 & cowlNothing(A) ) % 2.94/2.98 => cowlNothing(B) ) ). % 2.94/2.98 % 2.94/2.98 fof(cowlThing_substitution_1,axiom, % 2.94/2.98 ! [A,B] : % 2.94/2.98 ( ( A = B % 2.94/2.98 & cowlThing(A) ) % 2.94/2.98 => cowlThing(B) ) ). % 2.94/2.98 % 2.94/2.98 fof(rp_substitution_1,axiom, % 2.94/2.98 ! [A,B,C] : % 2.94/2.98 ( ( A = B % 2.94/2.98 & rp(A,C) ) % 2.94/2.98 => rp(B,C) ) ). % 2.94/2.98 % 2.94/2.98 fof(rp_substitution_2,axiom, % 2.94/2.99 ! [A,B,C] : % 2.94/2.99 ( ( A = B % 2.94/2.99 & rp(C,A) ) % 2.94/2.99 => rp(C,B) ) ). % 2.94/2.99 % 2.94/2.99 fof(xsd_integer_substitution_1,axiom, % 2.94/2.99 ! [A,B] : % 2.94/2.99 ( ( A = B % 2.94/2.99 & xsd_integer(A) ) % 2.94/2.99 => xsd_integer(B) ) ). % 2.94/2.99 % 2.94/2.99 fof(xsd_string_substitution_1,axiom, % 2.94/2.99 ! [A,B] : % 2.94/2.99 ( ( A = B % 2.94/2.99 & xsd_string(A) ) % 2.94/2.99 => xsd_string(B) ) ). % 2.94/2.99 % 2.94/2.99 %----Thing and Nothing % 2.94/2.99 fof(axiom_0,axiom, % 2.94/2.99 ! [X] : % 2.94/2.99 ( cowlThing(X) % 2.94/2.99 & ~ cowlNothing(X) ) ). % 2.94/2.99 % 2.94/2.99 %----String and Integer disjoint % 2.94/2.99 fof(axiom_1,axiom, % 2.94/2.99 ! [X] : % 2.94/2.99 ( xsd_string(X) % 2.94/2.99 <=> ~ xsd_integer(X) ) ). % 2.94/2.99 % 2.94/2.99 %----Super cc % 2.94/2.99 fof(axiom_2,axiom, % 2.94/2.99 ! [X] : % 2.94/2.99 ( cc(X) % 2.94/2.99 => ( ? [Y0] : rp(X,Y0) % 2.94/2.99 & ! [Y0,Y1] : % 2.94/2.99 ( ( rp(X,Y0) % 2.94/2.99 & rp(X,Y1) ) % 2.94/2.99 => Y0 = Y1 ) ) ) ). % 2.94/2.99 % 2.94/2.99 %----Thing and Nothing % 2.94/2.99 %----String and Integer disjoint % 2.94/2.99 %----Super cc % 2.94/2.99 %----Super cc % 2.94/2.99 fof(the_axiom,conjecture, % 2.94/2.99 ( ! [X] : % 2.94/2.99 ( cowlThing(X) % 2.94/2.99 & ~ cowlNothing(X) ) % 2.94/2.99 & ! [X] : % 2.94/2.99 ( xsd_string(X) % 2.94/2.99 <=> ~ xsd_integer(X) ) % 2.94/2.99 & ! [X] : % 2.94/2.99 ( cc(X) % 2.94/2.99 => ? [Y0] : rp(X,Y0) ) % 2.94/2.99 & ! [X] : % 2.94/2.99 ( cc(X) % 2.94/2.99 => ! [Y0,Y1] : % 2.94/2.99 ( ( rp(X,Y0) % 2.94/2.99 & rp(X,Y1) ) % 2.94/2.99 => Y0 = Y1 ) ) ) ). % 2.94/2.99 % 2.94/2.99 %------------------------------------------------------------------------------ % 2.94/2.99 %------------------------------------------- % 2.94/2.99 % Proof found % 2.94/2.99 % SZS status Theorem for theBenchmark % 2.94/2.99 % SZS output start Proof % 2.94/2.99 %ClaNum:31(EqnAxiom:10) % 2.94/2.99 %VarNum:23(SingletonVarNum:15) % 2.94/2.99 %MaxLitNum:5 % 2.94/2.99 %MaxfuncDepth:1 % 2.94/2.99 %SharedTerms:16 % 2.94/2.99 %goalClause: 14 15 16 17 18 19 20 21 23 24 25 26 27 28 29 30 % 2.94/2.99 [11]~P1(x111) % 2.94/2.99 [12]P5(x121)+P3(x121) % 2.94/2.99 [13]~P5(x131)+~P3(x131) % 2.94/2.99 [22]~P2(x221)+P4(x221,f3(x221)) % 2.94/2.99 [31]~P4(x313,x312)+~P4(x313,x311)+E(x311,x312)+~P2(x313) % 2.94/2.99 [14]P2(a1)+P1(a2)+P3(a4)+~E(a5,a6)+~P5(a4) % 2.94/2.99 [15]~E(a5,a6)+P2(a1)+P1(a2)+P5(a4)+~P3(a4) % 2.94/2.99 [16]P2(a1)+P2(a7)+P1(a2)+P3(a4)+~P5(a4) % 2.94/2.99 [17]P2(a1)+P2(a7)+P1(a2)+P5(a4)+~P3(a4) % 2.94/2.99 [18]P2(a1)+P1(a2)+P3(a4)+P4(a7,a6)+~P5(a4) % 2.94/2.99 [19]P2(a1)+P1(a2)+P3(a4)+P4(a7,a5)+~P5(a4) % 2.94/2.99 [20]P4(a7,a6)+P2(a1)+P1(a2)+P5(a4)+~P3(a4) % 2.94/2.99 [21]P4(a7,a5)+P2(a1)+P1(a2)+P5(a4)+~P3(a4) % 2.94/2.99 [23]~E(a5,a6)+~P4(a1,x231)+P1(a2)+P3(a4)+~P5(a4) % 2.94/2.99 [24]~E(a5,a6)+~P4(a1,x241)+P1(a2)+P5(a4)+~P3(a4) % 2.94/2.99 [25]~P4(a1,x251)+P2(a7)+P1(a2)+P3(a4)+~P5(a4) % 2.94/2.99 [26]~P4(a1,x261)+P2(a7)+P1(a2)+P5(a4)+~P3(a4) % 2.94/2.99 [27]P4(a7,a6)+~P4(a1,x271)+P1(a2)+P3(a4)+~P5(a4) % 2.94/2.99 [28]P4(a7,a5)+~P4(a1,x281)+P1(a2)+P3(a4)+~P5(a4) % 2.94/2.99 [29]P4(a7,a6)+~P4(a1,x291)+P1(a2)+P5(a4)+~P3(a4) % 2.94/2.99 [30]P4(a7,a5)+~P4(a1,x301)+P1(a2)+P5(a4)+~P3(a4) % 2.94/2.99 %EqnAxiom % 2.94/2.99 [1]E(x11,x11) % 2.94/2.99 [2]E(x22,x21)+~E(x21,x22) % 2.94/2.99 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 2.94/2.99 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 2.94/2.99 [5]~P1(x51)+P1(x52)+~E(x51,x52) % 2.94/2.99 [6]~P3(x61)+P3(x62)+~E(x61,x62) % 2.94/2.99 [7]~P5(x71)+P5(x72)+~E(x71,x72) % 2.94/2.99 [8]P4(x82,x83)+~E(x81,x82)+~P4(x81,x83) % 2.94/2.99 [9]P4(x93,x92)+~E(x91,x92)+~P4(x93,x91) % 2.94/2.99 [10]~P2(x101)+P2(x102)+~E(x101,x102) % 2.94/2.99 % 2.94/2.99 %------------------------------------------- % 2.94/2.99 cnf(36,plain, % 2.94/2.99 (~E(a5,a6)+P2(a1)+P3(a4)+~P5(a4)), % 2.94/2.99 inference(scs_inference,[],[11,14])). % 2.94/2.99 cnf(37,plain, % 2.94/2.99 (~E(a5,a6)+P2(a1)+P5(a4)+~P3(a4)), % 2.94/2.99 inference(scs_inference,[],[11,15])). % 2.94/2.99 cnf(38,plain, % 2.94/2.99 (P2(a1)+P2(a7)+P3(a4)+~P5(a4)), % 2.94/2.99 inference(scs_inference,[],[11,16])). % 2.94/2.99 cnf(39,plain, % 2.94/2.99 (P2(a1)+P2(a7)+P5(a4)+~P3(a4)), % 2.94/2.99 inference(scs_inference,[],[11,17])). % 2.94/2.99 cnf(40,plain, % 2.94/2.99 (P4(a7,a6)+P2(a1)+P3(a4)+~P5(a4)), % 2.94/2.99 inference(scs_inference,[],[11,18])). % 2.94/2.99 cnf(41,plain, % 2.94/2.99 (P4(a7,a5)+P2(a1)+P3(a4)+~P5(a4)), % 2.94/2.99 inference(scs_inference,[],[11,19])). % 2.94/2.99 cnf(42,plain, % 2.94/2.99 (P4(a7,a6)+P2(a1)+P5(a4)+~P3(a4)), % 2.94/2.99 inference(scs_inference,[],[11,20])). % 2.94/2.99 cnf(43,plain, % 2.94/2.99 (P4(a7,a5)+P2(a1)+P5(a4)+~P3(a4)), % 2.94/2.99 inference(scs_inference,[],[11,21])). % 2.94/2.99 cnf(44,plain, % 2.94/2.99 (~E(a5,a6)+~P4(a1,x441)+P3(a4)+~P5(a4)), % 2.94/2.99 inference(scs_inference,[],[11,23])). % 2.94/2.99 cnf(45,plain, % 2.94/2.99 (~E(a5,a6)+~P4(a1,x451)+P5(a4)+~P3(a4)), % 2.94/2.99 inference(scs_inference,[],[11,24])). % 2.94/2.99 cnf(46,plain, % 2.94/2.99 (~P4(a1,x461)+P2(a7)+P3(a4)+~P5(a4)), % 2.94/2.99 inference(scs_inference,[],[11,25])). % 2.94/2.99 cnf(47,plain, % 2.94/2.99 (~P4(a1,x471)+P2(a7)+P5(a4)+~P3(a4)), % 2.94/2.99 inference(scs_inference,[],[11,26])). % 2.94/2.99 cnf(48,plain, % 2.94/2.99 (P4(a7,a6)+~P4(a1,x481)+P3(a4)+~P5(a4)), % 2.94/2.99 inference(scs_inference,[],[11,27])). % 2.94/2.99 cnf(49,plain, % 2.94/2.99 (P4(a7,a5)+~P4(a1,x491)+P3(a4)+~P5(a4)), % 2.94/2.99 inference(scs_inference,[],[11,28])). % 2.94/2.99 cnf(50,plain, % 2.94/2.99 (P4(a7,a6)+~P4(a1,x501)+P5(a4)+~P3(a4)), % 2.94/2.99 inference(scs_inference,[],[11,29])). % 2.94/2.99 cnf(51,plain, % 2.94/2.99 (P4(a7,a5)+~P4(a1,x511)+P5(a4)+~P3(a4)), % 2.94/2.99 inference(scs_inference,[],[11,30])). % 2.94/2.99 cnf(55,plain, % 2.94/2.99 (~E(x551,x552)+~P2(x551)+P4(x552,f3(x552))), % 2.94/2.99 inference(scs_inference,[],[22,10])). % 2.94/2.99 cnf(62,plain, % 2.94/2.99 (P4(x621,f3(x622))+~P2(x622)+~E(x622,x621)), % 2.94/2.99 inference(scs_inference,[],[8,22])). % 2.94/2.99 cnf(64,plain, % 2.94/2.99 (P4(x641,x642)+~P2(x641)+~E(f3(x641),x642)), % 2.94/2.99 inference(scs_inference,[],[9,22])). % 2.94/2.99 cnf(73,plain, % 2.94/2.99 (~E(a5,a6)+P2(a1)+P3(a4)), % 2.94/2.99 inference(scs_inference,[],[12,36])). % 2.94/2.99 cnf(75,plain, % 2.94/2.99 (~E(a5,a6)+P2(a1)+P5(a4)), % 2.94/2.99 inference(scs_inference,[],[12,37])). % 2.94/2.99 cnf(76,plain, % 2.94/2.99 (~E(a6,a5)+P2(a1)+P5(a4)), % 2.94/2.99 inference(scs_inference,[],[75,2])). % 2.94/2.99 cnf(77,plain, % 2.94/2.99 (P2(a1)+P2(a7)+P3(a4)), % 2.94/2.99 inference(scs_inference,[],[12,38])). % 2.94/2.99 cnf(78,plain, % 2.94/2.99 (P4(a1,f3(a1))+P2(a7)+P3(a4)), % 2.94/2.99 inference(scs_inference,[],[77,22])). % 2.94/2.99 cnf(79,plain, % 2.94/2.99 (P2(a7)+P3(a4)+~P5(a4)), % 2.94/2.99 inference(scs_inference,[],[78,46])). % 2.94/2.99 cnf(84,plain, % 2.94/2.99 (P2(a1)+P2(a7)+P5(a4)), % 2.94/2.99 inference(scs_inference,[],[12,39])). % 2.94/2.99 cnf(85,plain, % 2.94/2.99 (P4(a1,f3(a1))+P2(a7)+P5(a4)), % 2.94/2.99 inference(scs_inference,[],[84,22])). % 2.94/2.99 cnf(86,plain, % 2.94/2.99 (P2(a7)+P5(a4)+~P3(a4)), % 2.94/2.99 inference(scs_inference,[],[85,47])). % 2.94/2.99 cnf(97,plain, % 2.94/2.99 (P2(a7)+P3(a4)), % 2.94/2.99 inference(scs_inference,[],[12,79])). % 2.94/2.99 cnf(100,plain, % 2.94/2.99 (P2(a7)+P5(a4)), % 2.94/2.99 inference(scs_inference,[],[12,86])). % 2.94/2.99 cnf(103,plain, % 2.94/2.99 (P4(a7,a6)+P2(a1)+P3(a4)), % 2.94/2.99 inference(scs_inference,[],[12,40])). % 2.94/2.99 cnf(104,plain, % 2.94/2.99 (P4(a7,a6)+P2(a1)+P5(a4)), % 2.94/2.99 inference(scs_inference,[],[12,42])). % 2.94/2.99 cnf(105,plain, % 2.94/2.99 (P4(a7,a5)+P2(a1)+P3(a4)), % 2.94/2.99 inference(scs_inference,[],[12,41])). % 2.94/2.99 cnf(106,plain, % 2.94/2.99 (P4(a7,a5)+P2(a1)+P5(a4)), % 2.94/2.99 inference(scs_inference,[],[12,43])). % 2.94/2.99 cnf(107,plain, % 2.94/2.99 (~E(a5,a6)+~P4(a1,x1071)+P3(a4)), % 2.94/2.99 inference(scs_inference,[],[12,44])). % 2.94/2.99 cnf(109,plain, % 2.94/2.99 (~E(a5,a6)+~P4(a1,x1091)+P5(a4)), % 2.94/2.99 inference(scs_inference,[],[12,45])). % 2.94/2.99 cnf(110,plain, % 2.94/2.99 (~E(a6,a5)+~P4(a1,x1101)+P5(a4)), % 2.94/2.99 inference(scs_inference,[],[109,2])). % 2.94/2.99 cnf(111,plain, % 2.94/2.99 (~P3(a4)+~E(a6,a5)+~P4(a1,x1111)), % 2.94/2.99 inference(scs_inference,[],[110,13])). % 2.94/2.99 cnf(112,plain, % 2.94/2.99 (~E(a5,a6)+~P4(a1,x1121)+~P3(a4)), % 2.94/2.99 inference(scs_inference,[],[111,2])). % 2.94/2.99 cnf(113,plain, % 2.94/2.99 (P4(a7,a6)+~P4(a1,x1131)+P3(a4)), % 2.94/2.99 inference(scs_inference,[],[12,48])). % 2.94/2.99 cnf(114,plain, % 2.94/2.99 (P4(a7,a6)+~P4(a1,x1141)+P5(a4)), % 2.94/2.99 inference(scs_inference,[],[12,50])). % 2.94/2.99 cnf(115,plain, % 2.94/2.99 (~P3(a4)+P4(a7,a6)+~P4(a1,x1151)), % 2.94/2.99 inference(scs_inference,[],[114,13])). % 2.94/2.99 cnf(116,plain, % 2.94/3.00 (P4(a7,a5)+~P4(a1,x1161)+P3(a4)), % 2.94/3.00 inference(scs_inference,[],[12,49])). % 2.94/3.00 cnf(117,plain, % 2.94/3.00 (P4(a7,a5)+~P4(a1,x1171)+P5(a4)), % 2.94/3.00 inference(scs_inference,[],[12,51])). % 2.94/3.00 cnf(123,plain, % 2.94/3.00 (~P3(a4)+P2(a7)), % 2.94/3.00 inference(scs_inference,[],[13,100])). % 2.94/3.00 cnf(124,plain, % 2.94/3.00 (P2(a7)), % 2.94/3.00 inference(scs_inference,[],[123,97])). % 2.94/3.00 cnf(125,plain, % 2.94/3.00 (~E(a7,x1251)+P4(x1251,f3(a7))), % 2.94/3.00 inference(scs_inference,[],[124,62])). % 2.94/3.00 cnf(127,plain, % 2.94/3.00 (~E(f3(a7),x1271)+P4(a7,x1271)), % 2.94/3.00 inference(scs_inference,[],[124,62,64])). % 2.94/3.00 cnf(132,plain, % 2.94/3.00 (P4(a7,f3(a7))), % 2.94/3.00 inference(equality_inference,[],[125])). % 2.94/3.00 cnf(149,plain, % 2.94/3.00 (~P3(a4)+P4(a7,a6)+P2(a1)), % 2.94/3.00 inference(scs_inference,[],[13,104])). % 2.94/3.00 cnf(154,plain, % 2.94/3.00 (~P5(a4)+P4(a7,a5)+P2(a1)), % 2.94/3.00 inference(scs_inference,[],[13,105])). % 2.94/3.00 cnf(155,plain, % 2.94/3.00 (P4(a7,a5)+P4(a1,f3(a1))+~P5(a4)), % 2.94/3.00 inference(scs_inference,[],[154,22])). % 2.94/3.00 cnf(159,plain, % 2.94/3.00 (~P5(a4)+P4(a7,a5)+~P4(a1,x1591)), % 2.94/3.00 inference(scs_inference,[],[13,116])). % 2.94/3.00 cnf(160,plain, % 2.94/3.00 (P4(a7,a5)+~P5(a4)), % 2.94/3.00 inference(scs_inference,[],[159,155])). % 2.94/3.00 cnf(179,plain, % 2.94/3.00 (P4(a7,a5)+P2(a1)), % 2.94/3.00 inference(scs_inference,[],[160,106])). % 2.94/3.00 cnf(185,plain, % 2.94/3.00 (P4(a7,a5)+~P4(a1,x1851)), % 2.94/3.00 inference(scs_inference,[],[160,117])). % 2.94/3.00 cnf(367,plain, % 2.94/3.00 (~P2(a1)+P4(a7,a5)), % 2.94/3.00 inference(scs_inference,[],[22,185])). % 2.94/3.00 cnf(400,plain, % 2.94/3.00 (P4(a7,a5)), % 2.94/3.00 inference(scs_inference,[],[367,179])). % 2.94/3.00 cnf(402,plain, % 2.94/3.00 (P4(a7,x4021)+~E(a5,x4021)), % 2.94/3.00 inference(scs_inference,[],[400,8,9])). % 2.94/3.00 cnf(436,plain, % 2.94/3.00 (~E(a5,a6)+P4(a1,f3(a1))+P3(a4)), % 2.94/3.00 inference(scs_inference,[],[22,73])). % 2.94/3.00 cnf(452,plain, % 2.94/3.00 (~E(a5,a6)+P3(a4)), % 2.94/3.00 inference(scs_inference,[],[436,107])). % 2.94/3.00 cnf(468,plain, % 2.94/3.00 (~E(a6,a5)+P3(a4)), % 2.94/3.00 inference(scs_inference,[],[452,2])). % 2.94/3.00 cnf(484,plain, % 2.94/3.00 (~P4(a7,a6)+P3(a4)), % 2.94/3.00 inference(scs_inference,[],[400,124,468,31])). % 2.94/3.00 cnf(500,plain, % 2.94/3.00 (~E(f3(a7),a6)+P3(a4)), % 2.94/3.00 inference(scs_inference,[],[484,127])). % 2.94/3.00 cnf(516,plain, % 2.94/3.00 (~E(a6,f3(a7))+P3(a4)), % 2.94/3.00 inference(scs_inference,[],[500,2])). % 2.94/3.00 cnf(532,plain, % 2.94/3.00 (~P5(a4)+~E(a6,f3(a7))), % 2.94/3.00 inference(scs_inference,[],[516,13])). % 2.94/3.00 cnf(548,plain, % 2.94/3.00 (~E(f3(a7),a6)+~P5(a4)), % 2.94/3.00 inference(scs_inference,[],[532,2])). % 2.94/3.00 cnf(564,plain, % 2.94/3.00 (~P4(a7,a6)+~P5(a4)), % 2.94/3.00 inference(scs_inference,[],[124,132,548,31])). % 2.94/3.00 cnf(580,plain, % 2.94/3.00 (~E(a5,a6)+~P5(a4)), % 2.94/3.00 inference(scs_inference,[],[564,402])). % 2.94/3.00 cnf(596,plain, % 2.94/3.00 (~E(a6,a5)+~P5(a4)), % 2.94/3.00 inference(scs_inference,[],[580,2])). % 2.94/3.00 cnf(612,plain, % 2.94/3.00 (~E(x6121,a4)+~P5(x6121)+~E(a6,a5)), % 2.94/3.00 inference(scs_inference,[],[596,7])). % 2.94/3.00 cnf(628,plain, % 2.94/3.00 (~E(a6,a5)+P2(a1)), % 2.94/3.00 inference(scs_inference,[],[612,76])). % 2.94/3.00 cnf(644,plain, % 2.94/3.00 (~E(a5,a6)+P2(a1)), % 2.94/3.00 inference(scs_inference,[],[628,2])). % 2.94/3.00 cnf(660,plain, % 2.94/3.00 (~P4(a7,a6)+P2(a1)), % 2.94/3.00 inference(scs_inference,[],[124,400,644,31])). % 2.94/3.00 cnf(789,plain, % 2.94/3.00 (~E(a4,x7891)+P3(x7891)+~E(a5,a6)), % 2.94/3.00 inference(scs_inference,[],[452,6])). % 2.94/3.00 cnf(805,plain, % 2.94/3.00 (~E(a5,a6)+~P4(a1,x8051)), % 2.94/3.00 inference(scs_inference,[],[789,112])). % 2.94/3.00 cnf(821,plain, % 2.94/3.00 (~E(a6,a5)+~P4(a1,x8211)), % 2.94/3.00 inference(scs_inference,[],[805,2])). % 2.94/3.00 cnf(837,plain, % 2.94/3.00 (~P4(a7,a6)+~P4(a1,x8371)), % 2.94/3.00 inference(scs_inference,[],[400,124,821,31])). % 2.94/3.00 cnf(853,plain, % 2.94/3.00 (~E(f3(a7),a6)+~P4(a1,x8531)), % 2.94/3.00 inference(scs_inference,[],[837,127])). % 2.94/3.00 cnf(869,plain, % 2.94/3.00 (~E(a6,f3(a7))+~P4(a1,x8691)), % 2.94/3.00 inference(scs_inference,[],[853,2])). % 2.94/3.00 cnf(885,plain, % 2.94/3.00 (~P2(a1)+~E(a6,f3(a7))), % 2.94/3.00 inference(scs_inference,[],[869,22])). % 2.94/3.00 cnf(901,plain, % 2.94/3.00 (~E(f3(a7),a6)+~P2(a1)), % 2.94/3.00 inference(scs_inference,[],[885,2])). % 2.94/3.00 cnf(917,plain, % 2.94/3.00 (~P4(a7,a6)+~P2(a1)), % 2.94/3.00 inference(scs_inference,[],[124,132,901,31])). % 2.94/3.00 cnf(1775,plain, % 2.94/3.00 (P2(a1)+P3(a4)), % 2.94/3.00 inference(scs_inference,[],[484,103])). % 2.94/3.00 cnf(1942,plain, % 2.94/3.00 (P4(a7,a6)+P2(a1)), % 2.94/3.00 inference(scs_inference,[],[1775,149])). % 2.94/3.00 cnf(1958,plain, % 2.94/3.00 (P2(a1)), % 2.94/3.00 inference(scs_inference,[],[1942,660])). % 2.94/3.00 cnf(1961,plain, % 2.94/3.00 (~P4(a7,a6)), % 2.94/3.00 inference(scs_inference,[],[1958,917])). % 2.94/3.00 cnf(1964,plain, % 2.94/3.00 (P4(x19641,f3(x19641))+~E(a1,x19641)), % 2.94/3.00 inference(scs_inference,[],[1958,55])). % 2.94/3.00 cnf(1971,plain, % 2.94/3.00 (P4(a1,f3(a1))), % 2.94/3.00 inference(equality_inference,[],[1964])). % 2.94/3.00 cnf(1974,plain, % 2.94/3.00 (P3(a4)), % 2.94/3.00 inference(scs_inference,[],[1971,1961,113])). % 2.94/3.00 cnf(1976,plain, % 2.94/3.00 (~P3(a4)), % 2.94/3.00 inference(scs_inference,[],[1971,1961,115])). % 2.94/3.00 cnf(1986,plain, % 2.94/3.00 ($false), % 2.94/3.00 inference(scs_inference,[],[1974,1976]), % 2.94/3.00 ['proof']). % 2.94/3.00 % SZS output end Proof % 2.94/3.00 % Total time :2.340000s %------------------------------------------------------------------------------