%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NLP145+1 : TPTP v8.2.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n023.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 12:01:25 EDT 2024 % Result : Theorem 11.94s 11.98s % Output : CNFRefutation 11.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP145+1 : TPTP v8.2.0. Released v2.4.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n023.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sat Jun 22 01:43:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.49/0.56 start to proof:theBenchmark % 11.90/11.95 %------------------------------------------- % 11.90/11.95 % File :CSE---1.7 % 11.90/11.95 % Problem :theBenchmark % 11.90/11.95 % Transform :cnf % 11.90/11.95 % Format :tptp:raw % 11.90/11.95 % Command :java -jar mcs_scs.jar %d %s % 11.90/11.95 % 11.90/11.95 % Result :Theorem 11.340000s % 11.90/11.96 % Output :CNFRefutation 11.340000s % 11.90/11.96 %------------------------------------------- % 11.90/11.96 %-------------------------------------------------------------------------- % 11.90/11.96 % File : NLP145+1 : TPTP v8.2.0. Released v2.4.0. % 11.90/11.96 % Domain : Natural Language Processing % 11.90/11.96 % Problem : An old dirty white Chevy, problem 32 % 11.90/11.96 % Version : [Bos00b] axioms. % 11.90/11.96 % English : Eliminating inconsistent interpretations in the statement % 11.90/11.96 % "An old dirty white chevy barrels down a lonely street in % 11.90/11.96 % hollywood. Two young fellas are in the front seat." % 11.90/11.96 % 11.90/11.96 % Refs : [Bos00a] Bos (2000), DORIS: Discourse Oriented Representation a % 11.90/11.96 % [Bos00b] Bos (2000), Applied Theorem Proving - Natural Language % 11.90/11.96 % Source : [Bos00b] % 11.90/11.96 % Names : doris122 [Bos00b] % 11.90/11.96 % 11.90/11.96 % Status : Theorem % 11.90/11.96 % Rating : 0.14 v8.2.0, 0.11 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.10 v7.3.0, 0.17 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.08 v6.2.0, 0.12 v6.1.0, 0.20 v6.0.0, 0.09 v5.5.0, 0.19 v5.4.0, 0.21 v5.3.0, 0.26 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.17 v4.1.0, 0.22 v4.0.0, 0.21 v3.7.0, 0.00 v3.2.0, 0.11 v3.1.0, 0.00 v2.4.0 % 11.90/11.96 % Syntax : Number of formulae : 62 ( 1 unt; 0 def) % 11.90/11.96 % Number of atoms : 157 ( 5 equ) % 11.90/11.96 % Maximal formula atoms : 27 ( 2 avg) % 11.90/11.96 % Number of connectives : 108 ( 13 ~; 1 |; 31 &) % 11.90/11.96 % ( 1 <=>; 62 =>; 0 <=; 0 <~>) % 11.90/11.96 % Maximal formula depth : 34 ( 5 avg) % 11.90/11.96 % Maximal term depth : 1 ( 1 avg) % 11.90/11.96 % Number of predicates : 60 ( 59 usr; 0 prp; 1-4 aty) % 11.90/11.96 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 11.90/11.96 % Number of variables : 140 ( 127 !; 13 ?) % 11.90/11.96 % SPC : FOF_THM_RFO_SEQ % 11.90/11.96 % 11.90/11.96 % Comments : % 11.90/11.96 %-------------------------------------------------------------------------- % 11.90/11.96 fof(ax1,axiom, % 11.90/11.96 ! [U,V] : % 11.90/11.96 ( furniture(U,V) % 11.90/11.96 => instrumentality(U,V) ) ). % 11.90/11.96 % 11.90/11.96 fof(ax2,axiom, % 11.90/11.96 ! [U,V] : % 11.90/11.96 ( seat(U,V) % 11.90/11.96 => furniture(U,V) ) ). % 11.90/11.96 % 11.90/11.96 fof(ax3,axiom, % 11.90/11.96 ! [U,V] : % 11.90/11.96 ( frontseat(U,V) % 11.90/11.96 => seat(U,V) ) ). % 11.90/11.96 % 11.90/11.96 fof(ax4,axiom, % 11.90/11.96 ! [U,V] : % 11.90/11.96 ( location(U,V) % 11.90/11.96 => object(U,V) ) ). % 11.90/11.96 % 11.90/11.96 fof(ax5,axiom, % 11.90/11.96 ! [U,V] : % 11.90/11.96 ( city(U,V) % 11.90/11.96 => location(U,V) ) ). % 11.90/11.96 % 11.90/11.96 fof(ax6,axiom, % 11.90/11.96 ! [U,V] : % 11.90/11.96 ( hollywood_placename(U,V) % 11.90/11.96 => placename(U,V) ) ). % 11.90/11.96 % 11.90/11.96 fof(ax7,axiom, % 11.90/11.96 ! [U,V] : % 11.90/11.96 ( abstraction(U,V) % 11.90/11.96 => unisex(U,V) ) ). % 11.90/11.96 % 11.90/11.96 fof(ax8,axiom, % 11.90/11.96 ! [U,V] : % 11.90/11.96 ( abstraction(U,V) % 11.90/11.96 => general(U,V) ) ). % 11.90/11.96 % 11.90/11.96 fof(ax9,axiom, % 11.90/11.96 ! [U,V] : % 11.90/11.96 ( abstraction(U,V) % 11.90/11.96 => nonhuman(U,V) ) ). % 11.90/11.96 % 11.90/11.96 fof(ax10,axiom, % 11.90/11.96 ! [U,V] : % 11.90/11.96 ( abstraction(U,V) % 11.90/11.96 => thing(U,V) ) ). % 11.90/11.96 % 11.90/11.96 fof(ax11,axiom, % 11.90/11.96 ! [U,V] : % 11.90/11.96 ( relation(U,V) % 11.90/11.96 => abstraction(U,V) ) ). % 11.90/11.96 % 11.90/11.96 fof(ax12,axiom, % 11.90/11.96 ! [U,V] : % 11.90/11.96 ( relname(U,V) % 11.90/11.96 => relation(U,V) ) ). % 11.90/11.96 % 11.90/11.96 fof(ax13,axiom, % 11.94/11.96 ! [U,V] : % 11.94/11.96 ( placename(U,V) % 11.94/11.96 => relname(U,V) ) ). % 11.94/11.96 % 11.94/11.96 fof(ax14,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( way(U,V) % 11.94/11.97 => artifact(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax15,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( street(U,V) % 11.94/11.97 => way(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax16,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( object(U,V) % 11.94/11.97 => unisex(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax17,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( object(U,V) % 11.94/11.97 => impartial(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax18,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( object(U,V) % 11.94/11.97 => nonliving(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax19,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( object(U,V) % 11.94/11.97 => entity(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax20,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( artifact(U,V) % 11.94/11.97 => object(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax21,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( instrumentality(U,V) % 11.94/11.97 => artifact(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax22,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( transport(U,V) % 11.94/11.97 => instrumentality(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax23,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( vehicle(U,V) % 11.94/11.97 => transport(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax24,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( car(U,V) % 11.94/11.97 => vehicle(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax25,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( chevy(U,V) % 11.94/11.97 => car(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax26,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( barrel(U,V) % 11.94/11.97 => event(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax27,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( event(U,V) % 11.94/11.97 => eventuality(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax28,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( state(U,V) % 11.94/11.97 => event(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax29,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( eventuality(U,V) % 11.94/11.97 => unisex(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax30,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( eventuality(U,V) % 11.94/11.97 => nonexistent(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax31,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( eventuality(U,V) % 11.94/11.97 => specific(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax32,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( eventuality(U,V) % 11.94/11.97 => thing(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax33,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( state(U,V) % 11.94/11.97 => eventuality(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax34,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( two(U,V) % 11.94/11.97 => group(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax35,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( set(U,V) % 11.94/11.97 => multiple(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax36,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( group(U,V) % 11.94/11.97 => set(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax37,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( man(U,V) % 11.94/11.97 => male(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax38,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( human_person(U,V) % 11.94/11.97 => animate(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax39,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( human_person(U,V) % 11.94/11.97 => human(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax40,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( organism(U,V) % 11.94/11.97 => living(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax41,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( organism(U,V) % 11.94/11.97 => impartial(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax42,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( entity(U,V) % 11.94/11.97 => existent(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax43,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( entity(U,V) % 11.94/11.97 => specific(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax44,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( thing(U,V) % 11.94/11.97 => singleton(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax45,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( entity(U,V) % 11.94/11.97 => thing(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax46,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( organism(U,V) % 11.94/11.97 => entity(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax47,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( human_person(U,V) % 11.94/11.97 => organism(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax48,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( man(U,V) % 11.94/11.97 => human_person(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax49,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( fellow(U,V) % 11.94/11.97 => man(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax50,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( animate(U,V) % 11.94/11.97 => ~ nonliving(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax51,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( existent(U,V) % 11.94/11.97 => ~ nonexistent(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax52,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( nonhuman(U,V) % 11.94/11.97 => ~ human(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax53,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( nonliving(U,V) % 11.94/11.97 => ~ living(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax54,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( singleton(U,V) % 11.94/11.97 => ~ multiple(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax55,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( specific(U,V) % 11.94/11.97 => ~ general(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax56,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( unisex(U,V) % 11.94/11.97 => ~ male(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax57,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( young(U,V) % 11.94/11.97 => ~ old(U,V) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax58,axiom, % 11.94/11.97 ! [U,V,W] : % 11.94/11.97 ( ( entity(U,V) % 11.94/11.97 & placename(U,W) % 11.94/11.97 & of(U,W,V) ) % 11.94/11.97 => ~ ? [X] : % 11.94/11.97 ( placename(U,X) % 11.94/11.97 & X != W % 11.94/11.97 & of(U,X,V) ) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax59,axiom, % 11.94/11.97 ! [U,V,W,X] : % 11.94/11.97 ( be(U,V,W,X) % 11.94/11.97 => W = X ) ). % 11.94/11.97 % 11.94/11.97 fof(ax60,axiom, % 11.94/11.97 ! [U,V] : % 11.94/11.97 ( two(U,V) % 11.94/11.97 <=> ? [W] : % 11.94/11.97 ( member(U,W,V) % 11.94/11.97 & ? [X] : % 11.94/11.97 ( member(U,X,V) % 11.94/11.97 & X != W % 11.94/11.97 & ! [Y] : % 11.94/11.97 ( member(U,Y,V) % 11.94/11.97 => ( Y = X % 11.94/11.97 | Y = W ) ) ) ) ) ). % 11.94/11.97 % 11.94/11.97 fof(ax61,axiom, % 11.94/11.97 ! [U] : % 11.94/11.97 ~ ? [V] : member(U,V,V) ). % 11.94/11.97 % 11.94/11.97 fof(co1,conjecture, % 11.94/11.97 ~ ? [U] : % 11.94/11.97 ( actual_world(U) % 11.94/11.97 & ? [V,W,X,Y,Z,X1] : % 11.94/11.97 ( of(U,W,V) % 11.94/11.97 & city(U,V) % 11.94/11.97 & hollywood_placename(U,W) % 11.94/11.97 & placename(U,W) % 11.94/11.97 & chevy(U,X) % 11.94/11.97 & white(U,X) % 11.94/11.97 & dirty(U,X) % 11.94/11.97 & old(U,X) % 11.94/11.97 & street(U,Y) % 11.94/11.97 & lonely(U,Y) % 11.94/11.97 & event(U,Z) % 11.94/11.97 & agent(U,Z,X) % 11.94/11.97 & present(U,Z) % 11.94/11.97 & barrel(U,Z) % 11.94/11.97 & down(U,Z,Y) % 11.94/11.97 & in(U,Z,V) % 11.94/11.97 & ! [X2] : % 11.94/11.97 ( member(U,X2,X1) % 11.94/11.97 => ? [X3,X4] : % 11.94/11.97 ( frontseat(U,X4) % 11.94/11.97 & state(U,X3) % 11.94/11.97 & be(U,X3,X2,X4) % 11.94/11.97 & in(U,X4,X4) ) ) % 11.94/11.98 & two(U,X1) % 11.94/11.98 & group(U,X1) % 11.94/11.98 & ! [X5] : % 11.94/11.98 ( member(U,X5,X1) % 11.94/11.98 => ( fellow(U,X5) % 11.94/11.98 & young(U,X5) ) ) ) ) ). % 11.94/11.98 % 11.94/11.98 %-------------------------------------------------------------------------- % 11.94/11.98 %------------------------------------------- % 11.94/11.98 % Proof found % 11.94/11.98 % SZS status Theorem for theBenchmark % 11.94/11.98 % SZS output start Proof % 11.94/11.98 %ClaNum:229(EqnAxiom:137) % 11.94/11.98 %VarNum:341(SingletonVarNum:151) % 11.94/11.98 %MaxLitNum:6 % 11.94/11.98 %MaxfuncDepth:1 % 11.94/11.98 %SharedTerms:26 % 11.94/11.98 %goalClause: 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 216 217 218 219 223 225 % 11.94/11.98 %singleGoalClaCount:19 % 11.94/11.98 [138]P1(a1) % 11.94/11.98 [139]P3(a1,a8) % 11.94/11.98 [140]P11(a1,a9) % 11.94/11.98 [141]P23(a1,a9) % 11.94/11.98 [142]P43(a1,a10) % 11.94/11.98 [143]P4(a1,a11) % 11.94/11.98 [144]P5(a1,a12) % 11.94/11.98 [145]P12(a1,a12) % 11.94/11.98 [146]P52(a1,a2) % 11.94/11.98 [147]P16(a1,a2) % 11.94/11.98 [148]P24(a1,a11) % 11.94/11.98 [149]P55(a1,a11) % 11.94/11.98 [150]P13(a1,a11) % 11.94/11.98 [151]P25(a1,a10) % 11.94/11.98 [152]P44(a1,a12) % 11.94/11.98 [153]P33(a1,a9,a8) % 11.94/11.98 [154]P6(a1,a12,a11) % 11.94/11.98 [155]P14(a1,a12,a10) % 11.94/11.98 [156]P26(a1,a12,a8) % 11.94/11.98 [157]~P34(x1571,x1572,x1572) % 11.94/11.98 [216]P20(a1,x2161)+~P34(a1,x2161,a2) % 11.94/11.98 [217]P59(a1,x2171)+~P34(a1,x2171,a2) % 11.94/11.98 [218]~P34(a1,x2181,a2)+P18(a1,f5(x2181)) % 11.94/11.98 [219]~P34(a1,x2191,a2)+P48(a1,f6(x2191)) % 11.94/11.98 [223]~P34(a1,x2231,a2)+P26(a1,f5(x2231),f5(x2231)) % 11.94/11.98 [225]P10(a1,f6(x2251),x2251,f5(x2251))+~P34(a1,x2251,a2) % 11.94/11.98 [158]~P45(x1581,x1582)+P17(x1581,x1582) % 11.94/11.98 [159]~P17(x1591,x1592)+P30(x1591,x1592) % 11.94/11.98 [160]~P53(x1601,x1602)+P30(x1601,x1602) % 11.94/11.98 [161]~P18(x1611,x1612)+P45(x1611,x1612) % 11.94/11.98 [162]~P3(x1621,x1622)+P31(x1621,x1622) % 11.94/11.98 [163]~P31(x1631,x1632)+P37(x1631,x1632) % 11.94/11.98 [164]~P7(x1641,x1642)+P37(x1641,x1642) % 11.94/11.98 [165]~P11(x1651,x1652)+P23(x1651,x1652) % 11.94/11.98 [166]~P46(x1661,x1662)+P2(x1661,x1662) % 11.94/11.98 [167]~P37(x1671,x1672)+P56(x1671,x1672) % 11.94/11.98 [168]~P2(x1681,x1682)+P56(x1681,x1682) % 11.94/11.98 [169]~P19(x1691,x1692)+P56(x1691,x1692) % 11.94/11.98 [170]~P2(x1701,x1702)+P22(x1701,x1702) % 11.94/11.98 [171]~P2(x1711,x1712)+P38(x1711,x1712) % 11.94/11.98 [172]~P2(x1721,x1722)+P54(x1721,x1722) % 11.94/11.98 [173]~P15(x1731,x1732)+P54(x1731,x1732) % 11.94/11.98 [174]~P19(x1741,x1742)+P54(x1741,x1742) % 11.94/11.98 [175]~P47(x1751,x1752)+P46(x1751,x1752) % 11.94/11.98 [176]~P23(x1761,x1762)+P47(x1761,x1762) % 11.94/11.98 [177]~P43(x1771,x1772)+P57(x1771,x1772) % 11.94/11.98 [178]~P30(x1781,x1782)+P7(x1781,x1782) % 11.94/11.98 [179]~P57(x1791,x1792)+P7(x1791,x1792) % 11.94/11.98 [180]~P37(x1801,x1802)+P27(x1801,x1802) % 11.94/11.98 [181]~P42(x1811,x1812)+P27(x1811,x1812) % 11.94/11.98 [182]~P37(x1821,x1822)+P41(x1821,x1822) % 11.94/11.98 [183]~P37(x1831,x1832)+P15(x1831,x1832) % 11.94/11.98 [184]~P42(x1841,x1842)+P15(x1841,x1842) % 11.94/11.98 [185]~P58(x1851,x1852)+P53(x1851,x1852) % 11.94/11.98 [186]~P9(x1861,x1862)+P58(x1861,x1862) % 11.94/11.98 [187]~P4(x1871,x1872)+P9(x1871,x1872) % 11.94/11.98 [188]~P5(x1881,x1882)+P12(x1881,x1882) % 11.94/11.98 [189]~P48(x1891,x1892)+P12(x1891,x1892) % 11.94/11.98 [190]~P12(x1901,x1902)+P19(x1901,x1902) % 11.94/11.98 [191]~P48(x1911,x1912)+P19(x1911,x1912) % 11.94/11.98 [192]~P19(x1921,x1922)+P39(x1921,x1922) % 11.94/11.98 [193]~P15(x1931,x1932)+P49(x1931,x1932) % 11.94/11.98 [194]~P19(x1941,x1942)+P49(x1941,x1942) % 11.94/11.98 [195]~P52(x1951,x1952)+P16(x1951,x1952) % 11.94/11.98 [196]~P16(x1961,x1962)+P50(x1961,x1962) % 11.94/11.98 [197]~P50(x1971,x1972)+P40(x1971,x1972) % 11.94/11.98 [198]~P20(x1981,x1982)+P35(x1981,x1982) % 11.94/11.98 [199]~P35(x1991,x1992)+P36(x1991,x1992) % 11.94/11.98 [200]~P35(x2001,x2002)+P28(x2001,x2002) % 11.94/11.98 [201]~P28(x2011,x2012)+P8(x2011,x2012) % 11.94/11.98 [202]~P28(x2021,x2022)+P29(x2021,x2022) % 11.94/11.98 [203]~P28(x2031,x2032)+P42(x2031,x2032) % 11.94/11.98 [204]~P42(x2041,x2042)+P32(x2041,x2042) % 11.94/11.98 [205]~P15(x2051,x2052)+P21(x2051,x2052) % 11.94/11.98 [206]~P54(x2061,x2062)+P51(x2061,x2062) % 11.94/11.98 [207]~P36(x2071,x2072)+~P56(x2071,x2072) % 11.94/11.98 [208]~P49(x2081,x2082)+~P22(x2081,x2082) % 11.94/11.98 [209]~P29(x2091,x2092)+~P38(x2091,x2092) % 11.94/11.98 [210]~P8(x2101,x2102)+~P41(x2101,x2102) % 11.94/11.98 [211]~P32(x2111,x2112)+~P41(x2111,x2112) % 11.94/11.98 [212]~P21(x2121,x2122)+~P39(x2121,x2122) % 11.94/11.98 [213]~P51(x2131,x2132)+~P40(x2131,x2132) % 11.94/11.98 [214]~P24(x2141,x2142)+~P59(x2141,x2142) % 11.94/11.98 [215]~P52(x2151,x2152)+~E(f3(x2151,x2152),f4(x2151,x2152)) % 11.94/11.98 [220]~P52(x2201,x2202)+P34(x2201,f4(x2201,x2202),x2202) % 11.94/11.98 [221]~P52(x2211,x2212)+P34(x2211,f3(x2211,x2212),x2212) % 11.94/11.98 [226]E(x2261,x2262)+~P10(x2263,x2264,x2261,x2262) % 11.94/11.98 [222]~P52(x2222,x2223)+~P34(x2222,x2221,x2223)+E(x2221,f3(x2222,x2223))+E(x2221,f4(x2222,x2223)) % 11.94/11.98 [227]~P34(x2273,x2272,x2274)+~P34(x2273,x2271,x2274)+E(x2271,x2272)+P52(x2273,x2274)+~E(f7(x2273,x2274,x2271,x2272),x2272) % 11.94/11.98 [228]~P34(x2283,x2282,x2284)+~P34(x2283,x2281,x2284)+E(x2281,x2282)+P52(x2283,x2284)+~E(f7(x2283,x2284,x2281,x2282),x2281) % 11.94/11.98 [229]~P34(x2293,x2292,x2294)+~P34(x2293,x2291,x2294)+E(x2291,x2292)+P52(x2293,x2294)+P34(x2293,f7(x2293,x2294,x2291,x2292),x2294) % 11.94/11.98 [224]~P23(x2243,x2241)+~P33(x2243,x2242,x2244)+~P33(x2243,x2241,x2244)+E(x2241,x2242)+~P23(x2243,x2242)+~P15(x2243,x2244) % 11.94/11.98 %EqnAxiom % 11.94/11.98 [1]E(x11,x11) % 11.94/11.98 [2]E(x22,x21)+~E(x21,x22) % 11.94/11.98 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 11.94/11.98 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43)) % 11.94/11.98 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52)) % 11.94/11.98 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63)) % 11.94/11.98 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72)) % 11.94/11.98 [8]~E(x81,x82)+E(f5(x81),f5(x82)) % 11.94/11.98 [9]~E(x91,x92)+E(f6(x91),f6(x92)) % 11.94/11.98 [10]~E(x101,x102)+E(f7(x101,x103,x104,x105),f7(x102,x103,x104,x105)) % 11.94/11.98 [11]~E(x111,x112)+E(f7(x113,x111,x114,x115),f7(x113,x112,x114,x115)) % 11.94/11.98 [12]~E(x121,x122)+E(f7(x123,x124,x121,x125),f7(x123,x124,x122,x125)) % 11.94/11.98 [13]~E(x131,x132)+E(f7(x133,x134,x135,x131),f7(x133,x134,x135,x132)) % 11.94/11.98 [14]~P1(x141)+P1(x142)+~E(x141,x142) % 11.94/11.98 [15]P3(x152,x153)+~E(x151,x152)+~P3(x151,x153) % 11.94/11.98 [16]P3(x163,x162)+~E(x161,x162)+~P3(x163,x161) % 11.94/11.98 [17]P11(x172,x173)+~E(x171,x172)+~P11(x171,x173) % 11.94/11.98 [18]P11(x183,x182)+~E(x181,x182)+~P11(x183,x181) % 11.94/11.98 [19]P23(x192,x193)+~E(x191,x192)+~P23(x191,x193) % 11.94/11.98 [20]P23(x203,x202)+~E(x201,x202)+~P23(x203,x201) % 11.94/11.98 [21]P43(x212,x213)+~E(x211,x212)+~P43(x211,x213) % 11.94/11.98 [22]P43(x223,x222)+~E(x221,x222)+~P43(x223,x221) % 11.94/11.98 [23]P4(x232,x233)+~E(x231,x232)+~P4(x231,x233) % 11.94/11.98 [24]P4(x243,x242)+~E(x241,x242)+~P4(x243,x241) % 11.94/11.98 [25]P5(x252,x253)+~E(x251,x252)+~P5(x251,x253) % 11.94/11.98 [26]P5(x263,x262)+~E(x261,x262)+~P5(x263,x261) % 11.94/11.98 [27]P12(x272,x273)+~E(x271,x272)+~P12(x271,x273) % 11.94/11.98 [28]P12(x283,x282)+~E(x281,x282)+~P12(x283,x281) % 11.94/11.98 [29]P52(x292,x293)+~E(x291,x292)+~P52(x291,x293) % 11.94/11.98 [30]P52(x303,x302)+~E(x301,x302)+~P52(x303,x301) % 11.94/11.98 [31]P16(x312,x313)+~E(x311,x312)+~P16(x311,x313) % 11.94/11.98 [32]P16(x323,x322)+~E(x321,x322)+~P16(x323,x321) % 11.94/11.98 [33]P24(x332,x333)+~E(x331,x332)+~P24(x331,x333) % 11.94/11.98 [34]P24(x343,x342)+~E(x341,x342)+~P24(x343,x341) % 11.94/11.98 [35]P55(x352,x353)+~E(x351,x352)+~P55(x351,x353) % 11.94/11.98 [36]P55(x363,x362)+~E(x361,x362)+~P55(x363,x361) % 11.94/11.98 [37]P13(x372,x373)+~E(x371,x372)+~P13(x371,x373) % 11.94/11.98 [38]P13(x383,x382)+~E(x381,x382)+~P13(x383,x381) % 11.94/11.98 [39]P25(x392,x393)+~E(x391,x392)+~P25(x391,x393) % 11.94/11.98 [40]P25(x403,x402)+~E(x401,x402)+~P25(x403,x401) % 11.94/11.98 [41]P44(x412,x413)+~E(x411,x412)+~P44(x411,x413) % 11.94/11.98 [42]P44(x423,x422)+~E(x421,x422)+~P44(x423,x421) % 11.94/11.98 [43]P33(x432,x433,x434)+~E(x431,x432)+~P33(x431,x433,x434) % 11.94/11.98 [44]P33(x443,x442,x444)+~E(x441,x442)+~P33(x443,x441,x444) % 11.94/11.98 [45]P33(x453,x454,x452)+~E(x451,x452)+~P33(x453,x454,x451) % 11.94/11.98 [46]P6(x462,x463,x464)+~E(x461,x462)+~P6(x461,x463,x464) % 11.94/11.98 [47]P6(x473,x472,x474)+~E(x471,x472)+~P6(x473,x471,x474) % 11.94/11.98 [48]P6(x483,x484,x482)+~E(x481,x482)+~P6(x483,x484,x481) % 11.94/11.98 [49]P14(x492,x493,x494)+~E(x491,x492)+~P14(x491,x493,x494) % 11.94/11.98 [50]P14(x503,x502,x504)+~E(x501,x502)+~P14(x503,x501,x504) % 11.94/11.98 [51]P14(x513,x514,x512)+~E(x511,x512)+~P14(x513,x514,x511) % 11.94/11.98 [52]P26(x522,x523,x524)+~E(x521,x522)+~P26(x521,x523,x524) % 11.94/11.98 [53]P26(x533,x532,x534)+~E(x531,x532)+~P26(x533,x531,x534) % 11.94/11.98 [54]P26(x543,x544,x542)+~E(x541,x542)+~P26(x543,x544,x541) % 11.94/11.98 [55]P34(x552,x553,x554)+~E(x551,x552)+~P34(x551,x553,x554) % 11.94/11.98 [56]P34(x563,x562,x564)+~E(x561,x562)+~P34(x563,x561,x564) % 11.94/11.98 [57]P34(x573,x574,x572)+~E(x571,x572)+~P34(x573,x574,x571) % 11.94/11.98 [58]P17(x582,x583)+~E(x581,x582)+~P17(x581,x583) % 11.94/11.98 [59]P17(x593,x592)+~E(x591,x592)+~P17(x593,x591) % 11.94/11.98 [60]P45(x602,x603)+~E(x601,x602)+~P45(x601,x603) % 11.94/11.98 [61]P45(x613,x612)+~E(x611,x612)+~P45(x613,x611) % 11.94/11.98 [62]P30(x622,x623)+~E(x621,x622)+~P30(x621,x623) % 11.94/11.98 [63]P30(x633,x632)+~E(x631,x632)+~P30(x633,x631) % 11.94/11.98 [64]P41(x642,x643)+~E(x641,x642)+~P41(x641,x643) % 11.94/11.98 [65]P41(x653,x652)+~E(x651,x652)+~P41(x653,x651) % 11.94/11.98 [66]P38(x662,x663)+~E(x661,x662)+~P38(x661,x663) % 11.94/11.98 [67]P38(x673,x672)+~E(x671,x672)+~P38(x673,x671) % 11.94/11.98 [68]P53(x682,x683)+~E(x681,x682)+~P53(x681,x683) % 11.94/11.98 [69]P53(x693,x692)+~E(x691,x692)+~P53(x693,x691) % 11.94/11.98 [70]P8(x702,x703)+~E(x701,x702)+~P8(x701,x703) % 11.94/11.98 [71]P8(x713,x712)+~E(x711,x712)+~P8(x713,x711) % 11.94/11.98 [72]P18(x722,x723)+~E(x721,x722)+~P18(x721,x723) % 11.94/11.98 [73]P18(x733,x732)+~E(x731,x732)+~P18(x733,x731) % 11.94/11.98 [74]P31(x742,x743)+~E(x741,x742)+~P31(x741,x743) % 11.94/11.98 [75]P31(x753,x752)+~E(x751,x752)+~P31(x753,x751) % 11.94/11.98 [76]P48(x762,x763)+~E(x761,x762)+~P48(x761,x763) % 11.94/11.98 [77]P48(x773,x772)+~E(x771,x772)+~P48(x773,x771) % 11.94/11.98 [78]P37(x782,x783)+~E(x781,x782)+~P37(x781,x783) % 11.94/11.98 [79]P37(x793,x792)+~E(x791,x792)+~P37(x793,x791) % 11.94/11.98 [80]P51(x802,x803)+~E(x801,x802)+~P51(x801,x803) % 11.94/11.98 [81]P51(x813,x812)+~E(x811,x812)+~P51(x813,x811) % 11.94/11.98 [82]P42(x822,x823)+~E(x821,x822)+~P42(x821,x823) % 11.94/11.98 [83]P42(x833,x832)+~E(x831,x832)+~P42(x833,x831) % 11.94/11.98 [84]P7(x842,x843)+~E(x841,x842)+~P7(x841,x843) % 11.94/11.98 [85]P7(x853,x852)+~E(x851,x852)+~P7(x853,x851) % 11.94/11.98 [86]P54(x862,x863)+~E(x861,x862)+~P54(x861,x863) % 11.94/11.98 [87]P54(x873,x872)+~E(x871,x872)+~P54(x873,x871) % 11.94/11.98 [88]P59(x882,x883)+~E(x881,x882)+~P59(x881,x883) % 11.94/11.98 [89]P59(x893,x892)+~E(x891,x892)+~P59(x893,x891) % 11.94/11.98 [90]P2(x902,x903)+~E(x901,x902)+~P2(x901,x903) % 11.94/11.98 [91]P2(x913,x912)+~E(x911,x912)+~P2(x913,x911) % 11.94/11.98 [92]P46(x922,x923)+~E(x921,x922)+~P46(x921,x923) % 11.94/11.98 [93]P46(x933,x932)+~E(x931,x932)+~P46(x933,x931) % 11.94/11.98 [94]P56(x942,x943)+~E(x941,x942)+~P56(x941,x943) % 11.94/11.98 [95]P56(x953,x952)+~E(x951,x952)+~P56(x953,x951) % 11.94/11.98 [96]P32(x962,x963)+~E(x961,x962)+~P32(x961,x963) % 11.94/11.98 [97]P32(x973,x972)+~E(x971,x972)+~P32(x973,x971) % 11.94/11.98 [98]P19(x982,x983)+~E(x981,x982)+~P19(x981,x983) % 11.94/11.98 [99]P19(x993,x992)+~E(x991,x992)+~P19(x993,x991) % 11.94/11.98 [100]P40(x1002,x1003)+~E(x1001,x1002)+~P40(x1001,x1003) % 11.94/11.98 [101]P40(x1013,x1012)+~E(x1011,x1012)+~P40(x1013,x1011) % 11.94/11.98 [102]P49(x1022,x1023)+~E(x1021,x1022)+~P49(x1021,x1023) % 11.94/11.98 [103]P49(x1033,x1032)+~E(x1031,x1032)+~P49(x1033,x1031) % 11.94/11.98 [104]P39(x1042,x1043)+~E(x1041,x1042)+~P39(x1041,x1043) % 11.94/11.98 [105]P39(x1053,x1052)+~E(x1051,x1052)+~P39(x1053,x1051) % 11.94/11.98 [106]P22(x1062,x1063)+~E(x1061,x1062)+~P22(x1061,x1063) % 11.94/11.98 [107]P22(x1073,x1072)+~E(x1071,x1072)+~P22(x1073,x1071) % 11.94/11.98 [108]P15(x1082,x1083)+~E(x1081,x1082)+~P15(x1081,x1083) % 11.94/11.98 [109]P15(x1093,x1092)+~E(x1091,x1092)+~P15(x1093,x1091) % 11.94/11.98 [110]P29(x1102,x1103)+~E(x1101,x1102)+~P29(x1101,x1103) % 11.94/11.98 [111]P29(x1113,x1112)+~E(x1111,x1112)+~P29(x1113,x1111) % 11.94/11.98 [112]P50(x1122,x1123)+~E(x1121,x1122)+~P50(x1121,x1123) % 11.94/11.98 [113]P50(x1133,x1132)+~E(x1131,x1132)+~P50(x1133,x1131) % 11.94/11.98 [114]P36(x1142,x1143)+~E(x1141,x1142)+~P36(x1141,x1143) % 11.94/11.98 [115]P36(x1153,x1152)+~E(x1151,x1152)+~P36(x1153,x1151) % 11.94/11.98 [116]P35(x1162,x1163)+~E(x1161,x1162)+~P35(x1161,x1163) % 11.94/11.98 [117]P35(x1173,x1172)+~E(x1171,x1172)+~P35(x1173,x1171) % 11.94/11.98 [118]P20(x1182,x1183)+~E(x1181,x1182)+~P20(x1181,x1183) % 11.94/11.98 [119]P20(x1193,x1192)+~E(x1191,x1192)+~P20(x1193,x1191) % 11.94/11.98 [120]P9(x1202,x1203)+~E(x1201,x1202)+~P9(x1201,x1203) % 11.94/11.98 [121]P9(x1213,x1212)+~E(x1211,x1212)+~P9(x1213,x1211) % 11.94/11.98 [122]P28(x1222,x1223)+~E(x1221,x1222)+~P28(x1221,x1223) % 11.94/11.98 [123]P28(x1233,x1232)+~E(x1231,x1232)+~P28(x1233,x1231) % 11.94/11.98 [124]P21(x1242,x1243)+~E(x1241,x1242)+~P21(x1241,x1243) % 11.94/11.98 [125]P21(x1253,x1252)+~E(x1251,x1252)+~P21(x1253,x1251) % 11.94/11.98 [126]P27(x1262,x1263)+~E(x1261,x1262)+~P27(x1261,x1263) % 11.94/11.98 [127]P27(x1273,x1272)+~E(x1271,x1272)+~P27(x1273,x1271) % 11.94/11.98 [128]P47(x1282,x1283)+~E(x1281,x1282)+~P47(x1281,x1283) % 11.94/11.98 [129]P47(x1293,x1292)+~E(x1291,x1292)+~P47(x1293,x1291) % 11.94/11.98 [130]P58(x1302,x1303)+~E(x1301,x1302)+~P58(x1301,x1303) % 11.94/11.98 [131]P58(x1313,x1312)+~E(x1311,x1312)+~P58(x1313,x1311) % 11.94/11.98 [132]P10(x1322,x1323,x1324,x1325)+~E(x1321,x1322)+~P10(x1321,x1323,x1324,x1325) % 11.94/11.98 [133]P10(x1333,x1332,x1334,x1335)+~E(x1331,x1332)+~P10(x1333,x1331,x1334,x1335) % 11.94/11.98 [134]P10(x1343,x1344,x1342,x1345)+~E(x1341,x1342)+~P10(x1343,x1344,x1341,x1345) % 11.94/11.98 [135]P10(x1353,x1354,x1355,x1352)+~E(x1351,x1352)+~P10(x1353,x1354,x1355,x1351) % 11.94/11.98 [136]P57(x1362,x1363)+~E(x1361,x1362)+~P57(x1361,x1363) % 11.94/11.98 [137]P57(x1373,x1372)+~E(x1371,x1372)+~P57(x1373,x1371) % 11.94/11.98 % 11.94/11.98 %------------------------------------------- % 11.94/11.98 cnf(256,plain, % 11.94/11.98 (P52(x2561,a2)+~E(a1,x2561)), % 11.94/11.98 inference(scs_inference,[],[145,146,27,28,29])). % 11.94/11.98 cnf(313,plain, % 11.94/11.98 (P30(x3131,x3132)+~P45(x3131,x3132)), % 11.94/11.98 inference(scs_inference,[],[158,159])). % 11.94/11.98 cnf(314,plain, % 11.94/11.98 (P7(x3141,x3142)+~P53(x3141,x3142)), % 11.94/11.98 inference(scs_inference,[],[160,178])). % 11.94/11.98 cnf(315,plain, % 11.94/11.98 (~P18(x3151,x3152)+P30(x3151,x3152)), % 11.94/11.98 inference(scs_inference,[],[161,313])). % 11.94/11.98 cnf(410,plain, % 11.94/11.98 (~P58(x4101,x4102)+P7(x4101,x4102)), % 11.94/11.98 inference(scs_inference,[],[185,314])). % 11.94/11.98 cnf(519,plain, % 11.94/11.98 (P39(x5191,x5192)+~P48(x5191,x5192)), % 11.94/11.98 inference(scs_inference,[],[191,192])). % 11.94/11.98 cnf(683,plain, % 11.94/11.98 (~P41(x6831,x6832)+~P42(x6831,x6832)), % 11.94/11.98 inference(scs_inference,[],[204,211])). % 11.94/11.98 cnf(840,plain, % 11.94/11.98 (P39(a1,f6(x8401))+~P34(a1,x8401,a2)), % 11.94/11.98 inference(scs_inference,[],[519,219])). % 11.94/11.98 cnf(872,plain, % 11.94/11.98 (~P41(x8721,x8722)+~P28(x8721,x8722)), % 11.94/11.98 inference(scs_inference,[],[683,203])). % 11.94/11.98 cnf(904,plain, % 11.94/11.98 (~P41(x9041,x9042)+~P35(x9041,x9042)), % 11.94/11.98 inference(scs_inference,[],[872,200])). % 11.94/11.98 cnf(920,plain, % 11.94/11.98 (~P41(x9201,x9202)+~P20(x9201,x9202)), % 11.94/11.98 inference(scs_inference,[],[904,198])). % 11.94/11.98 cnf(936,plain, % 11.94/11.98 (~P41(a1,x9361)+~P34(a1,x9361,a2)), % 11.94/11.98 inference(scs_inference,[],[920,216])). % 11.94/11.98 cnf(1107,plain, % 11.94/11.98 (P34(x11071,f3(x11071,a2),a2)+~E(a1,x11071)), % 11.94/11.98 inference(scs_inference,[],[221,256])). % 11.94/11.98 cnf(1108,plain, % 11.94/11.98 (P34(a1,f3(a1,a2),a2)), % 11.94/11.98 inference(equality_inference,[],[1107])). % 11.94/11.98 cnf(1115,plain, % 11.94/11.98 (~P41(a1,f3(a1,a2))), % 11.94/11.98 inference(scs_inference,[],[1108,216,217,840,936])). % 11.94/11.98 cnf(1333,plain, % 11.94/11.98 (E(f3(a1,a2),f5(f3(a1,a2)))), % 11.94/11.98 inference(scs_inference,[],[1108,225,226])). % 11.94/11.98 cnf(1334,plain, % 11.94/11.98 (E(f5(f3(a1,a2)),f3(a1,a2))), % 11.94/11.98 inference(scs_inference,[],[1333,2])). % 11.94/11.98 cnf(2198,plain, % 11.94/11.98 (~P37(a1,f5(f3(a1,a2)))), % 11.94/11.98 inference(scs_inference,[],[1115,1334,65,182])). % 11.94/11.98 cnf(2225,plain, % 11.94/11.98 ($false), % 11.94/11.98 inference(scs_inference,[],[1108,2198,164,163,410,179,186,178,162,187,159,177,315,158,160,218]), % 11.94/11.98 ['proof']). % 11.94/11.98 % SZS output end Proof % 11.94/11.98 % Total time :11.340000s %------------------------------------------------------------------------------