%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NLP204+1 : TPTP v8.2.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n017.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:42 EDT 2024 % Result : Theorem 2.93s 3.04s % Output : CNFRefutation 2.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NLP204+1 : TPTP v8.2.0. Released v2.4.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n017.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 04:30:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 2.93/3.02 %------------------------------------------- % 2.93/3.02 % File :CSE---1.7 % 2.93/3.02 % Problem :theBenchmark % 2.93/3.02 % Transform :cnf % 2.93/3.02 % Format :tptp:raw % 2.93/3.02 % Command :java -jar mcs_scs.jar %d %s % 2.93/3.02 % 2.93/3.02 % Result :Theorem 2.410000s % 2.93/3.02 % Output :CNFRefutation 2.410000s % 2.93/3.02 %------------------------------------------- % 2.93/3.02 %-------------------------------------------------------------------------- % 2.93/3.02 % File : NLP204+1 : TPTP v8.2.0. Released v2.4.0. % 2.93/3.02 % Domain : Natural Language Processing % 2.93/3.02 % Problem : An old dirty white Chevy, problem 91 % 2.93/3.02 % Version : [Bos00b] axioms. % 2.93/3.02 % English : Eliminating inconsistent interpretations in the statement % 2.93/3.02 % "An old dirty white chevy barrels down a lonely street in % 2.93/3.02 % hollywood. Two young fellas are in the front seat. They are % 2.93/3.02 % wearing cheap black coats. Jules is behind the wheel." % 2.93/3.03 % 2.93/3.03 % Refs : [Bos00a] Bos (2000), DORIS: Discourse Oriented Representation a % 2.93/3.03 % [Bos00b] Bos (2000), Applied Theorem Proving - Natural Language % 2.93/3.03 % Source : [Bos00b] % 2.93/3.03 % Names : doris181 [Bos00b] % 2.93/3.03 % 2.93/3.03 % Status : Theorem % 2.93/3.03 % Rating : 0.08 v8.1.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.04 v6.3.0, 0.00 v6.2.0, 0.08 v6.1.0, 0.17 v6.0.0, 0.09 v5.5.0, 0.15 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0, 0.05 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.1, 0.17 v3.7.0, 0.00 v2.4.0 % 2.93/3.03 % Syntax : Number of formulae : 72 ( 1 unt; 0 def) % 2.93/3.03 % Number of atoms : 204 ( 7 equ) % 2.93/3.03 % Maximal formula atoms : 48 ( 2 avg) % 2.93/3.03 % Number of connectives : 149 ( 17 ~; 1 |; 55 &) % 2.93/3.03 % ( 1 <=>; 75 =>; 0 <=; 0 <~>) % 2.93/3.03 % Maximal formula depth : 51 ( 5 avg) % 2.93/3.03 % Maximal term depth : 1 ( 1 avg) % 2.93/3.03 % Number of predicates : 72 ( 71 usr; 0 prp; 1-4 aty) % 2.93/3.03 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 2.93/3.03 % Number of variables : 173 ( 153 !; 20 ?) % 2.93/3.03 % SPC : FOF_THM_RFO_SEQ % 2.93/3.03 % 2.93/3.03 % Comments : % 2.93/3.03 %-------------------------------------------------------------------------- % 2.93/3.03 fof(ax1,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( jules_forename(U,V) % 2.93/3.03 => forename(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax2,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( forename(U,V) % 2.93/3.03 => relname(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax3,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( furniture(U,V) % 2.93/3.03 => instrumentality(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax4,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( seat(U,V) % 2.93/3.03 => furniture(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax5,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( frontseat(U,V) % 2.93/3.03 => seat(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax6,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( location(U,V) % 2.93/3.03 => object(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax7,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( city(U,V) % 2.93/3.03 => location(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax8,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( hollywood_placename(U,V) % 2.93/3.03 => placename(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax9,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( abstraction(U,V) % 2.93/3.03 => unisex(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax10,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( abstraction(U,V) % 2.93/3.03 => general(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax11,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( abstraction(U,V) % 2.93/3.03 => nonhuman(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax12,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( abstraction(U,V) % 2.93/3.03 => thing(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax13,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( relation(U,V) % 2.93/3.03 => abstraction(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax14,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( relname(U,V) % 2.93/3.03 => relation(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax15,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( placename(U,V) % 2.93/3.03 => relname(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax16,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( transport(U,V) % 2.93/3.03 => instrumentality(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax17,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( vehicle(U,V) % 2.93/3.03 => transport(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax18,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( car(U,V) % 2.93/3.03 => vehicle(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax19,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( chevy(U,V) % 2.93/3.03 => car(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax20,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( way(U,V) % 2.93/3.03 => artifact(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax21,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( street(U,V) % 2.93/3.03 => way(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax22,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( barrel(U,V) % 2.93/3.03 => event(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax23,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( two(U,V) % 2.93/3.03 => group(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax24,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( man(U,V) % 2.93/3.03 => male(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax25,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( human_person(U,V) % 2.93/3.03 => animate(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax26,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( human_person(U,V) % 2.93/3.03 => human(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax27,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( organism(U,V) % 2.93/3.03 => living(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax28,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( organism(U,V) % 2.93/3.03 => impartial(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax29,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( organism(U,V) % 2.93/3.03 => entity(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax30,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( human_person(U,V) % 2.93/3.03 => organism(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax31,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( man(U,V) % 2.93/3.03 => human_person(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax32,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( fellow(U,V) % 2.93/3.03 => man(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax33,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( wear(U,V) % 2.93/3.03 => event(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax34,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( set(U,V) % 2.93/3.03 => multiple(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax35,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( group(U,V) % 2.93/3.03 => set(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax36,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( clothes(U,V) % 2.93/3.03 => artifact(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax37,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( coat(U,V) % 2.93/3.03 => clothes(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax38,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( object(U,V) % 2.93/3.03 => unisex(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax39,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( object(U,V) % 2.93/3.03 => impartial(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax40,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( object(U,V) % 2.93/3.03 => nonliving(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax41,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( entity(U,V) % 2.93/3.03 => existent(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax42,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( entity(U,V) % 2.93/3.03 => specific(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax43,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( entity(U,V) % 2.93/3.03 => thing(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax44,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( object(U,V) % 2.93/3.03 => entity(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax45,axiom, % 2.93/3.03 ! [U,V] : % 2.93/3.03 ( artifact(U,V) % 2.93/3.03 => object(U,V) ) ). % 2.93/3.03 % 2.93/3.03 fof(ax46,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( instrumentality(U,V) % 2.93/3.04 => artifact(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax47,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( device(U,V) % 2.93/3.04 => instrumentality(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax48,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( wheel(U,V) % 2.93/3.04 => device(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax49,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( event(U,V) % 2.93/3.04 => eventuality(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax50,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( state(U,V) % 2.93/3.04 => event(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax51,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( eventuality(U,V) % 2.93/3.04 => unisex(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax52,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( eventuality(U,V) % 2.93/3.04 => nonexistent(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax53,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( eventuality(U,V) % 2.93/3.04 => specific(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax54,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( thing(U,V) % 2.93/3.04 => singleton(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax55,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( eventuality(U,V) % 2.93/3.04 => thing(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax56,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( state(U,V) % 2.93/3.04 => eventuality(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax57,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( animate(U,V) % 2.93/3.04 => ~ nonliving(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax58,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( existent(U,V) % 2.93/3.04 => ~ nonexistent(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax59,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( nonhuman(U,V) % 2.93/3.04 => ~ human(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax60,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( nonliving(U,V) % 2.93/3.04 => ~ living(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax61,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( singleton(U,V) % 2.93/3.04 => ~ multiple(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax62,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( specific(U,V) % 2.93/3.04 => ~ general(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax63,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( unisex(U,V) % 2.93/3.04 => ~ male(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax64,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( white(U,V) % 2.93/3.04 => ~ black(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax65,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( young(U,V) % 2.93/3.04 => ~ old(U,V) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax66,axiom, % 2.93/3.04 ! [U,V,W] : % 2.93/3.04 ( ( entity(U,V) % 2.93/3.04 & forename(U,W) % 2.93/3.04 & of(U,W,V) ) % 2.93/3.04 => ~ ? [X] : % 2.93/3.04 ( forename(U,X) % 2.93/3.04 & X != W % 2.93/3.04 & of(U,X,V) ) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax67,axiom, % 2.93/3.04 ! [U,V,W] : % 2.93/3.04 ( ( entity(U,V) % 2.93/3.04 & placename(U,W) % 2.93/3.04 & of(U,W,V) ) % 2.93/3.04 => ~ ? [X] : % 2.93/3.04 ( placename(U,X) % 2.93/3.04 & X != W % 2.93/3.04 & of(U,X,V) ) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax68,axiom, % 2.93/3.04 ! [U,V] : % 2.93/3.04 ( two(U,V) % 2.93/3.04 <=> ? [W] : % 2.93/3.04 ( member(U,W,V) % 2.93/3.04 & ? [X] : % 2.93/3.04 ( member(U,X,V) % 2.93/3.04 & X != W % 2.93/3.04 & ! [Y] : % 2.93/3.04 ( member(U,Y,V) % 2.93/3.04 => ( Y = X % 2.93/3.04 | Y = W ) ) ) ) ) ). % 2.93/3.04 % 2.93/3.04 fof(ax69,axiom, % 2.93/3.04 ! [U,V,W,X] : % 2.93/3.04 ( ( nonreflexive(U,V) % 2.93/3.04 & agent(U,V,W) % 2.93/3.04 & patient(U,V,X) ) % 2.93/3.04 => W != X ) ). % 2.93/3.04 % 2.93/3.04 fof(ax70,axiom, % 2.93/3.04 ! [U] : % 2.93/3.04 ~ ? [V] : member(U,V,V) ). % 2.93/3.04 % 2.93/3.04 fof(ax71,axiom, % 2.93/3.04 ! [U,V,W,X] : % 2.93/3.04 ( be(U,V,W,X) % 2.93/3.04 => W = X ) ). % 2.93/3.04 % 2.93/3.04 fof(co1,conjecture, % 2.93/3.04 ~ ? [U] : % 2.93/3.04 ( actual_world(U) % 2.93/3.04 & ? [V,W,X,Y,Z,X1,X2,X3,X4,X5,X6] : % 2.93/3.04 ( of(U,W,V) % 2.93/3.04 & man(U,V) % 2.93/3.04 & jules_forename(U,W) % 2.93/3.04 & forename(U,W) % 2.93/3.04 & frontseat(U,X) % 2.93/3.04 & chevy(U,Y) % 2.93/3.04 & white(U,Y) % 2.93/3.04 & dirty(U,Y) % 2.93/3.04 & old(U,Y) % 2.93/3.04 & of(U,Z,X1) % 2.93/3.04 & city(U,X1) % 2.93/3.04 & hollywood_placename(U,Z) % 2.93/3.04 & placename(U,Z) % 2.93/3.04 & street(U,X1) % 2.93/3.04 & lonely(U,X1) % 2.93/3.04 & event(U,X2) % 2.93/3.04 & agent(U,X2,Y) % 2.93/3.04 & present(U,X2) % 2.93/3.04 & barrel(U,X2) % 2.93/3.04 & down(U,X2,X1) % 2.93/3.04 & in(U,X2,X1) % 2.93/3.04 & ! [X7] : % 2.93/3.04 ( member(U,X7,X3) % 2.93/3.04 => ? [X8,X9] : % 2.93/3.04 ( state(U,X8) % 2.93/3.04 & be(U,X8,X7,X9) % 2.93/3.04 & in(U,X9,X) ) ) % 2.93/3.04 & two(U,X3) % 2.93/3.04 & group(U,X3) % 2.93/3.04 & ! [X10] : % 2.93/3.04 ( member(U,X10,X3) % 2.93/3.04 => ( fellow(U,X10) % 2.93/3.04 & young(U,X10) ) ) % 2.93/3.04 & ! [X11] : % 2.93/3.04 ( member(U,X11,X4) % 2.93/3.04 => ! [X12] : % 2.93/3.04 ( member(U,X12,X3) % 2.93/3.04 => ? [X13] : % 2.93/3.04 ( event(U,X13) % 2.93/3.04 & agent(U,X13,X12) % 2.93/3.04 & patient(U,X13,X11) % 2.93/3.04 & present(U,X13) % 2.93/3.04 & nonreflexive(U,X13) % 2.93/3.04 & wear(U,X13) ) ) ) % 2.93/3.04 & group(U,X4) % 2.93/3.04 & ! [X14] : % 2.93/3.04 ( member(U,X14,X4) % 2.93/3.04 => ( coat(U,X14) % 2.93/3.04 & black(U,X14) % 2.93/3.04 & cheap(U,X14) ) ) % 2.93/3.04 & wheel(U,X6) % 2.93/3.04 & state(U,X5) % 2.93/3.04 & be(U,X5,V,X6) % 2.93/3.04 & behind(U,X6,X6) ) ) ). % 2.93/3.04 % 2.93/3.04 %-------------------------------------------------------------------------- % 2.93/3.04 %------------------------------------------- % 2.93/3.04 % Proof found % 2.93/3.04 % SZS status Theorem for theBenchmark % 2.93/3.04 % SZS output start Proof % 2.93/3.04 %ClaNum:285(EqnAxiom:165) % 2.93/3.04 %VarNum:426(SingletonVarNum:189) % 2.93/3.04 %MaxLitNum:6 % 2.93/3.04 %MaxfuncDepth:1 % 2.93/3.04 %SharedTerms:41 % 2.93/3.04 %goalClause: 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 262 263 264 265 266 267 270 273 274 275 276 277 278 281 % 2.93/3.04 %singleGoalClaCount:29 % 2.93/3.04 [166]P1(a1) % 2.93/3.04 [167]P3(a1,a14) % 2.93/3.04 [168]P4(a1,a14) % 2.93/3.04 [169]P26(a1,a16) % 2.93/3.04 [170]P5(a1,a2) % 2.93/3.04 [171]P27(a1,a17) % 2.93/3.04 [172]P36(a1,a17) % 2.93/3.04 [173]P6(a1,a18) % 2.93/3.04 [174]P53(a1,a2) % 2.93/3.04 [175]P7(a1,a3) % 2.93/3.04 [176]P16(a1,a3) % 2.93/3.04 [177]P62(a1,a4) % 2.93/3.04 [178]P28(a1,a4) % 2.93/3.04 [179]P28(a1,a5) % 2.93/3.04 [180]P37(a1,a15) % 2.93/3.04 [181]P65(a1,a6) % 2.93/3.04 [182]P54(a1,a7) % 2.93/3.04 [183]P70(a1,a18) % 2.93/3.04 [184]P42(a1,a18) % 2.93/3.04 [185]P17(a1,a18) % 2.93/3.04 [186]P38(a1,a2) % 2.93/3.04 [187]P55(a1,a3) % 2.93/3.04 [188]P43(a1,a14,a15) % 2.93/3.04 [189]P43(a1,a17,a2) % 2.93/3.04 [190]P8(a1,a3,a18) % 2.93/3.04 [191]P21(a1,a3,a2) % 2.93/3.04 [192]P31(a1,a3,a2) % 2.93/3.04 [193]P11(a1,a6,a6) % 2.93/3.04 [194]P12(a1,a7,a15,a6) % 2.93/3.04 [195]~P44(x1951,x1952,x1952) % 2.93/3.04 [262]P24(a1,x2621)+~P44(a1,x2621,a4) % 2.93/3.04 [263]P20(a1,x2631)+~P44(a1,x2631,a5) % 2.93/3.04 [264]P14(a1,x2641)+~P44(a1,x2641,a5) % 2.93/3.04 [265]P71(a1,x2651)+~P44(a1,x2651,a4) % 2.93/3.04 [266]P15(a1,x2661)+~P44(a1,x2661,a5) % 2.93/3.04 [267]~P44(a1,x2671,a4)+P54(a1,f10(x2671)) % 2.93/3.04 [270]~P44(a1,x2701,a4)+P31(a1,f11(x2701),a16) % 2.93/3.04 [281]P12(a1,f10(x2811),x2811,f11(x2811))+~P44(a1,x2811,a4) % 2.93/3.04 [196]~P3(x1961,x1962)+P4(x1961,x1962) % 2.93/3.04 [197]~P4(x1971,x1972)+P56(x1971,x1972) % 2.93/3.04 [198]~P36(x1981,x1982)+P56(x1981,x1982) % 2.93/3.04 [199]~P58(x1991,x1992)+P29(x1991,x1992) % 2.93/3.04 [200]~P29(x2001,x2002)+P35(x2001,x2002) % 2.93/3.04 [201]~P63(x2011,x2012)+P35(x2011,x2012) % 2.93/3.04 [202]~P18(x2021,x2022)+P35(x2021,x2022) % 2.93/3.04 [203]~P26(x2031,x2032)+P58(x2031,x2032) % 2.93/3.04 [204]~P5(x2041,x2042)+P39(x2041,x2042) % 2.93/3.04 [205]~P39(x2051,x2052)+P45(x2051,x2052) % 2.93/3.04 [206]~P9(x2061,x2062)+P45(x2061,x2062) % 2.93/3.04 [207]~P27(x2071,x2072)+P36(x2071,x2072) % 2.93/3.04 [208]~P57(x2081,x2082)+P2(x2081,x2082) % 2.93/3.04 [209]~P45(x2091,x2092)+P66(x2091,x2092) % 2.93/3.04 [210]~P2(x2101,x2102)+P66(x2101,x2102) % 2.93/3.04 [211]~P23(x2111,x2112)+P66(x2111,x2112) % 2.93/3.04 [212]~P2(x2121,x2122)+P30(x2121,x2122) % 2.93/3.04 [213]~P2(x2131,x2132)+P46(x2131,x2132) % 2.93/3.04 [214]~P2(x2141,x2142)+P64(x2141,x2142) % 2.93/3.04 [215]~P22(x2151,x2152)+P64(x2151,x2152) % 2.93/3.04 [216]~P23(x2161,x2162)+P64(x2161,x2162) % 2.93/3.04 [217]~P56(x2171,x2172)+P57(x2171,x2172) % 2.93/3.04 [218]~P67(x2181,x2182)+P63(x2181,x2182) % 2.93/3.04 [219]~P13(x2191,x2192)+P67(x2191,x2192) % 2.93/3.04 [220]~P6(x2201,x2202)+P13(x2201,x2202) % 2.93/3.04 [221]~P53(x2211,x2212)+P68(x2211,x2212) % 2.93/3.04 [222]~P35(x2221,x2222)+P9(x2221,x2222) % 2.93/3.04 [223]~P68(x2231,x2232)+P9(x2231,x2232) % 2.93/3.04 [224]~P19(x2241,x2242)+P9(x2241,x2242) % 2.93/3.04 [225]~P7(x2251,x2252)+P16(x2251,x2252) % 2.93/3.04 [226]~P69(x2261,x2262)+P16(x2261,x2262) % 2.93/3.04 [227]~P54(x2271,x2272)+P16(x2271,x2272) % 2.93/3.04 [228]~P62(x2281,x2282)+P28(x2281,x2282) % 2.93/3.04 [229]~P24(x2291,x2292)+P37(x2291,x2292) % 2.93/3.04 [230]~P37(x2301,x2302)+P41(x2301,x2302) % 2.93/3.04 [231]~P37(x2311,x2312)+P32(x2311,x2312) % 2.93/3.04 [232]~P32(x2321,x2322)+P10(x2321,x2322) % 2.93/3.04 [233]~P32(x2331,x2332)+P33(x2331,x2332) % 2.93/3.04 [234]~P32(x2341,x2342)+P51(x2341,x2342) % 2.93/3.04 [235]~P51(x2351,x2352)+P40(x2351,x2352) % 2.93/3.04 [236]~P45(x2361,x2362)+P34(x2361,x2362) % 2.93/3.04 [237]~P51(x2371,x2372)+P34(x2371,x2372) % 2.93/3.04 [238]~P45(x2381,x2382)+P22(x2381,x2382) % 2.93/3.04 [239]~P51(x2391,x2392)+P22(x2391,x2392) % 2.93/3.04 [240]~P28(x2401,x2402)+P59(x2401,x2402) % 2.93/3.04 [241]~P59(x2411,x2412)+P47(x2411,x2412) % 2.93/3.04 [242]~P20(x2421,x2422)+P19(x2421,x2422) % 2.93/3.04 [243]~P45(x2431,x2432)+P49(x2431,x2432) % 2.93/3.04 [244]~P22(x2441,x2442)+P25(x2441,x2442) % 2.93/3.04 [245]~P22(x2451,x2452)+P60(x2451,x2452) % 2.93/3.04 [246]~P23(x2461,x2462)+P60(x2461,x2462) % 2.93/3.04 [247]~P65(x2471,x2472)+P18(x2471,x2472) % 2.93/3.04 [248]~P16(x2481,x2482)+P23(x2481,x2482) % 2.93/3.04 [249]~P54(x2491,x2492)+P23(x2491,x2492) % 2.93/3.04 [250]~P23(x2501,x2502)+P48(x2501,x2502) % 2.93/3.04 [251]~P64(x2511,x2512)+P61(x2511,x2512) % 2.93/3.04 [252]~P41(x2521,x2522)+~P66(x2521,x2522) % 2.93/3.04 [253]~P60(x2531,x2532)+~P30(x2531,x2532) % 2.93/3.04 [254]~P33(x2541,x2542)+~P46(x2541,x2542) % 2.93/3.04 [255]~P49(x2551,x2552)+~P10(x2551,x2552) % 2.93/3.04 [256]~P49(x2561,x2562)+~P40(x2561,x2562) % 2.93/3.04 [257]~P61(x2571,x2572)+~P47(x2571,x2572) % 2.93/3.04 [258]~P48(x2581,x2582)+~P25(x2581,x2582) % 2.93/3.04 [259]~P14(x2591,x2592)+~P70(x2591,x2592) % 2.93/3.04 [260]~P42(x2601,x2602)+~P71(x2601,x2602) % 2.93/3.04 [261]~P62(x2611,x2612)+~E(f8(x2611,x2612),f9(x2611,x2612)) % 2.93/3.04 [268]~P62(x2681,x2682)+P44(x2681,f9(x2681,x2682),x2682) % 2.93/3.04 [269]~P62(x2691,x2692)+P44(x2691,f8(x2691,x2692),x2692) % 2.93/3.04 [282]E(x2821,x2822)+~P12(x2823,x2824,x2821,x2822) % 2.93/3.04 [273]~P44(a1,x2732,a4)+~P44(a1,x2731,a5)+P16(a1,f12(x2731,x2732)) % 2.93/3.04 [274]~P44(a1,x2742,a4)+~P44(a1,x2741,a5)+P69(a1,f12(x2741,x2742)) % 2.93/3.04 [275]~P44(a1,x2752,a4)+~P44(a1,x2751,a5)+P50(a1,f12(x2751,x2752)) % 2.93/3.04 [276]~P44(a1,x2762,a4)+~P44(a1,x2761,a5)+P55(a1,f12(x2761,x2762)) % 2.93/3.04 [277]~P44(a1,x2772,a4)+~P44(a1,x2771,a5)+P8(a1,f12(x2771,x2772),x2772) % 2.93/3.04 [278]~P44(a1,x2782,a4)+~P44(a1,x2781,a5)+P52(a1,f12(x2781,x2782),x2781) % 2.93/3.04 [271]~P62(x2712,x2713)+~P44(x2712,x2711,x2713)+E(x2711,f8(x2712,x2713))+E(x2711,f9(x2712,x2713)) % 2.93/3.04 [272]~P8(x2723,x2724,x2721)+~P52(x2723,x2724,x2722)+~E(x2721,x2722)+~P50(x2723,x2724) % 2.93/3.04 [283]~P44(x2833,x2832,x2834)+~P44(x2833,x2831,x2834)+E(x2831,x2832)+P62(x2833,x2834)+~E(f13(x2833,x2834,x2831,x2832),x2832) % 2.93/3.05 [284]~P44(x2843,x2842,x2844)+~P44(x2843,x2841,x2844)+E(x2841,x2842)+P62(x2843,x2844)+~E(f13(x2843,x2844,x2841,x2842),x2841) % 2.93/3.05 [285]~P44(x2853,x2852,x2854)+~P44(x2853,x2851,x2854)+E(x2851,x2852)+P62(x2853,x2854)+P44(x2853,f13(x2853,x2854,x2851,x2852),x2854) % 2.93/3.05 [279]~P4(x2793,x2791)+~P43(x2793,x2792,x2794)+~P43(x2793,x2791,x2794)+E(x2791,x2792)+~P4(x2793,x2792)+~P22(x2793,x2794) % 2.93/3.05 [280]~P36(x2803,x2801)+~P43(x2803,x2802,x2804)+~P43(x2803,x2801,x2804)+E(x2801,x2802)+~P36(x2803,x2802)+~P22(x2803,x2804) % 2.93/3.05 %EqnAxiom % 2.93/3.05 [1]E(x11,x11) % 2.93/3.05 [2]E(x22,x21)+~E(x21,x22) % 2.93/3.05 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 2.93/3.05 [4]~E(x41,x42)+E(f8(x41,x43),f8(x42,x43)) % 2.93/3.05 [5]~E(x51,x52)+E(f8(x53,x51),f8(x53,x52)) % 2.93/3.05 [6]~E(x61,x62)+E(f9(x61,x63),f9(x62,x63)) % 2.93/3.05 [7]~E(x71,x72)+E(f9(x73,x71),f9(x73,x72)) % 2.93/3.05 [8]~E(x81,x82)+E(f10(x81),f10(x82)) % 2.93/3.05 [9]~E(x91,x92)+E(f13(x91,x93,x94,x95),f13(x92,x93,x94,x95)) % 2.93/3.05 [10]~E(x101,x102)+E(f13(x103,x101,x104,x105),f13(x103,x102,x104,x105)) % 2.93/3.05 [11]~E(x111,x112)+E(f13(x113,x114,x111,x115),f13(x113,x114,x112,x115)) % 2.93/3.05 [12]~E(x121,x122)+E(f13(x123,x124,x125,x121),f13(x123,x124,x125,x122)) % 2.93/3.05 [13]~E(x131,x132)+E(f12(x131,x133),f12(x132,x133)) % 2.93/3.05 [14]~E(x141,x142)+E(f12(x143,x141),f12(x143,x142)) % 2.93/3.05 [15]~E(x151,x152)+E(f11(x151),f11(x152)) % 2.93/3.05 [16]~P1(x161)+P1(x162)+~E(x161,x162) % 2.93/3.05 [17]P3(x172,x173)+~E(x171,x172)+~P3(x171,x173) % 2.93/3.05 [18]P3(x183,x182)+~E(x181,x182)+~P3(x183,x181) % 2.93/3.05 [19]P4(x192,x193)+~E(x191,x192)+~P4(x191,x193) % 2.93/3.05 [20]P4(x203,x202)+~E(x201,x202)+~P4(x203,x201) % 2.93/3.05 [21]P26(x212,x213)+~E(x211,x212)+~P26(x211,x213) % 2.93/3.05 [22]P26(x223,x222)+~E(x221,x222)+~P26(x223,x221) % 2.93/3.05 [23]P5(x232,x233)+~E(x231,x232)+~P5(x231,x233) % 2.93/3.05 [24]P5(x243,x242)+~E(x241,x242)+~P5(x243,x241) % 2.93/3.05 [25]P27(x252,x253)+~E(x251,x252)+~P27(x251,x253) % 2.93/3.05 [26]P27(x263,x262)+~E(x261,x262)+~P27(x263,x261) % 2.93/3.05 [27]P36(x272,x273)+~E(x271,x272)+~P36(x271,x273) % 2.93/3.05 [28]P36(x283,x282)+~E(x281,x282)+~P36(x283,x281) % 2.93/3.05 [29]P6(x292,x293)+~E(x291,x292)+~P6(x291,x293) % 2.93/3.05 [30]P6(x303,x302)+~E(x301,x302)+~P6(x303,x301) % 2.93/3.05 [31]P53(x312,x313)+~E(x311,x312)+~P53(x311,x313) % 2.93/3.05 [32]P53(x323,x322)+~E(x321,x322)+~P53(x323,x321) % 2.93/3.05 [33]P7(x332,x333)+~E(x331,x332)+~P7(x331,x333) % 2.93/3.05 [34]P7(x343,x342)+~E(x341,x342)+~P7(x343,x341) % 2.93/3.05 [35]P16(x352,x353)+~E(x351,x352)+~P16(x351,x353) % 2.93/3.05 [36]P16(x363,x362)+~E(x361,x362)+~P16(x363,x361) % 2.93/3.05 [37]P62(x372,x373)+~E(x371,x372)+~P62(x371,x373) % 2.93/3.05 [38]P62(x383,x382)+~E(x381,x382)+~P62(x383,x381) % 2.93/3.05 [39]P28(x392,x393)+~E(x391,x392)+~P28(x391,x393) % 2.93/3.05 [40]P28(x403,x402)+~E(x401,x402)+~P28(x403,x401) % 2.93/3.05 [41]P8(x412,x413,x414)+~E(x411,x412)+~P8(x411,x413,x414) % 2.93/3.05 [42]P8(x423,x422,x424)+~E(x421,x422)+~P8(x423,x421,x424) % 2.93/3.05 [43]P8(x433,x434,x432)+~E(x431,x432)+~P8(x433,x434,x431) % 2.93/3.05 [44]P37(x442,x443)+~E(x441,x442)+~P37(x441,x443) % 2.93/3.05 [45]P37(x453,x452)+~E(x451,x452)+~P37(x453,x451) % 2.93/3.05 [46]P65(x462,x463)+~E(x461,x462)+~P65(x461,x463) % 2.93/3.05 [47]P65(x473,x472)+~E(x471,x472)+~P65(x473,x471) % 2.93/3.05 [48]P54(x482,x483)+~E(x481,x482)+~P54(x481,x483) % 2.93/3.05 [49]P54(x493,x492)+~E(x491,x492)+~P54(x493,x491) % 2.93/3.05 [50]P70(x502,x503)+~E(x501,x502)+~P70(x501,x503) % 2.93/3.05 [51]P70(x513,x512)+~E(x511,x512)+~P70(x513,x511) % 2.93/3.05 [52]P42(x522,x523)+~E(x521,x522)+~P42(x521,x523) % 2.93/3.05 [53]P42(x533,x532)+~E(x531,x532)+~P42(x533,x531) % 2.93/3.05 [54]P17(x542,x543)+~E(x541,x542)+~P17(x541,x543) % 2.93/3.05 [55]P17(x553,x552)+~E(x551,x552)+~P17(x553,x551) % 2.93/3.05 [56]P38(x562,x563)+~E(x561,x562)+~P38(x561,x563) % 2.93/3.05 [57]P38(x573,x572)+~E(x571,x572)+~P38(x573,x571) % 2.93/3.05 [58]P55(x582,x583)+~E(x581,x582)+~P55(x581,x583) % 2.93/3.05 [59]P55(x593,x592)+~E(x591,x592)+~P55(x593,x591) % 2.93/3.05 [60]P43(x602,x603,x604)+~E(x601,x602)+~P43(x601,x603,x604) % 2.93/3.05 [61]P43(x613,x612,x614)+~E(x611,x612)+~P43(x613,x611,x614) % 2.93/3.05 [62]P43(x623,x624,x622)+~E(x621,x622)+~P43(x623,x624,x621) % 2.93/3.05 [63]P50(x632,x633)+~E(x631,x632)+~P50(x631,x633) % 2.93/3.05 [64]P50(x643,x642)+~E(x641,x642)+~P50(x643,x641) % 2.93/3.05 [65]P44(x652,x653,x654)+~E(x651,x652)+~P44(x651,x653,x654) % 2.93/3.05 [66]P44(x663,x662,x664)+~E(x661,x662)+~P44(x663,x661,x664) % 2.93/3.05 [67]P44(x673,x674,x672)+~E(x671,x672)+~P44(x673,x674,x671) % 2.93/3.05 [68]P21(x682,x683,x684)+~E(x681,x682)+~P21(x681,x683,x684) % 2.93/3.05 [69]P21(x693,x692,x694)+~E(x691,x692)+~P21(x693,x691,x694) % 2.93/3.05 [70]P21(x703,x704,x702)+~E(x701,x702)+~P21(x703,x704,x701) % 2.93/3.05 [71]P31(x712,x713,x714)+~E(x711,x712)+~P31(x711,x713,x714) % 2.93/3.05 [72]P31(x723,x722,x724)+~E(x721,x722)+~P31(x723,x721,x724) % 2.93/3.05 [73]P31(x733,x734,x732)+~E(x731,x732)+~P31(x733,x734,x731) % 2.93/3.05 [74]P11(x742,x743,x744)+~E(x741,x742)+~P11(x741,x743,x744) % 2.93/3.05 [75]P11(x753,x752,x754)+~E(x751,x752)+~P11(x753,x751,x754) % 2.93/3.05 [76]P11(x763,x764,x762)+~E(x761,x762)+~P11(x763,x764,x761) % 2.93/3.05 [77]P12(x772,x773,x774,x775)+~E(x771,x772)+~P12(x771,x773,x774,x775) % 2.93/3.05 [78]P12(x783,x782,x784,x785)+~E(x781,x782)+~P12(x783,x781,x784,x785) % 2.93/3.05 [79]P12(x793,x794,x792,x795)+~E(x791,x792)+~P12(x793,x794,x791,x795) % 2.93/3.05 [80]P12(x803,x804,x805,x802)+~E(x801,x802)+~P12(x803,x804,x805,x801) % 2.93/3.05 [81]P52(x812,x813,x814)+~E(x811,x812)+~P52(x811,x813,x814) % 2.93/3.05 [82]P52(x823,x822,x824)+~E(x821,x822)+~P52(x823,x821,x824) % 2.93/3.05 [83]P52(x833,x834,x832)+~E(x831,x832)+~P52(x833,x834,x831) % 2.93/3.05 [84]P15(x842,x843)+~E(x841,x842)+~P15(x841,x843) % 2.93/3.05 [85]P15(x853,x852)+~E(x851,x852)+~P15(x853,x851) % 2.93/3.05 [86]P71(x862,x863)+~E(x861,x862)+~P71(x861,x863) % 2.93/3.05 [87]P71(x873,x872)+~E(x871,x872)+~P71(x873,x871) % 2.93/3.05 [88]P56(x882,x883)+~E(x881,x882)+~P56(x881,x883) % 2.93/3.05 [89]P56(x893,x892)+~E(x891,x892)+~P56(x893,x891) % 2.93/3.05 [90]P14(x902,x903)+~E(x901,x902)+~P14(x901,x903) % 2.93/3.05 [91]P14(x913,x912)+~E(x911,x912)+~P14(x913,x911) % 2.93/3.05 [92]P61(x922,x923)+~E(x921,x922)+~P61(x921,x923) % 2.93/3.05 [93]P61(x933,x932)+~E(x931,x932)+~P61(x933,x931) % 2.93/3.05 [94]P20(x942,x943)+~E(x941,x942)+~P20(x941,x943) % 2.93/3.05 [95]P20(x953,x952)+~E(x951,x952)+~P20(x953,x951) % 2.93/3.05 [96]P29(x962,x963)+~E(x961,x962)+~P29(x961,x963) % 2.93/3.05 [97]P29(x973,x972)+~E(x971,x972)+~P29(x973,x971) % 2.93/3.05 [98]P58(x982,x983)+~E(x981,x982)+~P58(x981,x983) % 2.93/3.05 [99]P58(x993,x992)+~E(x991,x992)+~P58(x993,x991) % 2.93/3.05 [100]P35(x1002,x1003)+~E(x1001,x1002)+~P35(x1001,x1003) % 2.93/3.05 [101]P35(x1013,x1012)+~E(x1011,x1012)+~P35(x1013,x1011) % 2.93/3.05 [102]P33(x1022,x1023)+~E(x1021,x1022)+~P33(x1021,x1023) % 2.93/3.05 [103]P33(x1033,x1032)+~E(x1031,x1032)+~P33(x1033,x1031) % 2.93/3.05 [104]P10(x1042,x1043)+~E(x1041,x1042)+~P10(x1041,x1043) % 2.93/3.05 [105]P10(x1053,x1052)+~E(x1051,x1052)+~P10(x1053,x1051) % 2.93/3.05 [106]P63(x1062,x1063)+~E(x1061,x1062)+~P63(x1061,x1063) % 2.93/3.05 [107]P63(x1073,x1072)+~E(x1071,x1072)+~P63(x1073,x1071) % 2.93/3.05 [108]P18(x1082,x1083)+~E(x1081,x1082)+~P18(x1081,x1083) % 2.93/3.05 [109]P18(x1093,x1092)+~E(x1091,x1092)+~P18(x1093,x1091) % 2.93/3.05 [110]P22(x1102,x1103)+~E(x1101,x1102)+~P22(x1101,x1103) % 2.93/3.05 [111]P22(x1113,x1112)+~E(x1111,x1112)+~P22(x1113,x1111) % 2.93/3.05 [112]P23(x1122,x1123)+~E(x1121,x1122)+~P23(x1121,x1123) % 2.93/3.05 [113]P23(x1133,x1132)+~E(x1131,x1132)+~P23(x1133,x1131) % 2.93/3.05 [114]P24(x1142,x1143)+~E(x1141,x1142)+~P24(x1141,x1143) % 2.93/3.05 [115]P24(x1153,x1152)+~E(x1151,x1152)+~P24(x1153,x1151) % 2.93/3.05 [116]P39(x1162,x1163)+~E(x1161,x1162)+~P39(x1161,x1163) % 2.93/3.05 [117]P39(x1173,x1172)+~E(x1171,x1172)+~P39(x1173,x1171) % 2.93/3.05 [118]P25(x1182,x1183)+~E(x1181,x1182)+~P25(x1181,x1183) % 2.93/3.05 [119]P25(x1193,x1192)+~E(x1191,x1192)+~P25(x1193,x1191) % 2.93/3.05 [120]P45(x1202,x1203)+~E(x1201,x1202)+~P45(x1201,x1203) % 2.93/3.05 [121]P45(x1213,x1212)+~E(x1211,x1212)+~P45(x1213,x1211) % 2.93/3.05 [122]P19(x1222,x1223)+~E(x1221,x1222)+~P19(x1221,x1223) % 2.93/3.05 [123]P19(x1233,x1232)+~E(x1231,x1232)+~P19(x1233,x1231) % 2.93/3.05 [124]P34(x1242,x1243)+~E(x1241,x1242)+~P34(x1241,x1243) % 2.93/3.05 [125]P34(x1253,x1252)+~E(x1251,x1252)+~P34(x1253,x1251) % 2.93/3.05 [126]P9(x1262,x1263)+~E(x1261,x1262)+~P9(x1261,x1263) % 2.93/3.05 [127]P9(x1273,x1272)+~E(x1271,x1272)+~P9(x1273,x1271) % 2.93/3.05 [128]P66(x1282,x1283)+~E(x1281,x1282)+~P66(x1281,x1283) % 2.93/3.05 [129]P66(x1293,x1292)+~E(x1291,x1292)+~P66(x1293,x1291) % 2.93/3.05 [130]P64(x1302,x1303)+~E(x1301,x1302)+~P64(x1301,x1303) % 2.93/3.05 [131]P64(x1313,x1312)+~E(x1311,x1312)+~P64(x1313,x1311) % 2.93/3.05 [132]P2(x1322,x1323)+~E(x1321,x1322)+~P2(x1321,x1323) % 2.93/3.05 [133]P2(x1333,x1332)+~E(x1331,x1332)+~P2(x1333,x1331) % 2.93/3.05 [134]P57(x1342,x1343)+~E(x1341,x1342)+~P57(x1341,x1343) % 2.93/3.05 [135]P57(x1353,x1352)+~E(x1351,x1352)+~P57(x1353,x1351) % 2.93/3.05 [136]P59(x1362,x1363)+~E(x1361,x1362)+~P59(x1361,x1363) % 2.93/3.05 [137]P59(x1373,x1372)+~E(x1371,x1372)+~P59(x1373,x1371) % 2.93/3.05 [138]P51(x1382,x1383)+~E(x1381,x1382)+~P51(x1381,x1383) % 2.93/3.05 [139]P51(x1393,x1392)+~E(x1391,x1392)+~P51(x1393,x1391) % 2.93/3.05 [140]P40(x1402,x1403)+~E(x1401,x1402)+~P40(x1401,x1403) % 2.93/3.05 [141]P40(x1413,x1412)+~E(x1411,x1412)+~P40(x1413,x1411) % 2.93/3.05 [142]P47(x1422,x1423)+~E(x1421,x1422)+~P47(x1421,x1423) % 2.93/3.05 [143]P47(x1433,x1432)+~E(x1431,x1432)+~P47(x1433,x1431) % 2.93/3.05 [144]P32(x1442,x1443)+~E(x1441,x1442)+~P32(x1441,x1443) % 2.93/3.05 [145]P32(x1453,x1452)+~E(x1451,x1452)+~P32(x1453,x1451) % 2.93/3.05 [146]P68(x1462,x1463)+~E(x1461,x1462)+~P68(x1461,x1463) % 2.93/3.05 [147]P68(x1473,x1472)+~E(x1471,x1472)+~P68(x1473,x1471) % 2.93/3.05 [148]P30(x1482,x1483)+~E(x1481,x1482)+~P30(x1481,x1483) % 2.93/3.05 [149]P30(x1493,x1492)+~E(x1491,x1492)+~P30(x1493,x1491) % 2.93/3.05 [150]P46(x1502,x1503)+~E(x1501,x1502)+~P46(x1501,x1503) % 2.93/3.05 [151]P46(x1513,x1512)+~E(x1511,x1512)+~P46(x1513,x1511) % 2.93/3.05 [152]P49(x1522,x1523)+~E(x1521,x1522)+~P49(x1521,x1523) % 2.93/3.05 [153]P49(x1533,x1532)+~E(x1531,x1532)+~P49(x1533,x1531) % 2.93/3.05 [154]P48(x1542,x1543)+~E(x1541,x1542)+~P48(x1541,x1543) % 2.93/3.05 [155]P48(x1553,x1552)+~E(x1551,x1552)+~P48(x1553,x1551) % 2.93/3.05 [156]P13(x1562,x1563)+~E(x1561,x1562)+~P13(x1561,x1563) % 2.93/3.05 [157]P13(x1573,x1572)+~E(x1571,x1572)+~P13(x1573,x1571) % 2.93/3.05 [158]P69(x1582,x1583)+~E(x1581,x1582)+~P69(x1581,x1583) % 2.93/3.05 [159]P69(x1593,x1592)+~E(x1591,x1592)+~P69(x1593,x1591) % 2.93/3.05 [160]P41(x1602,x1603)+~E(x1601,x1602)+~P41(x1601,x1603) % 2.93/3.05 [161]P41(x1613,x1612)+~E(x1611,x1612)+~P41(x1613,x1611) % 2.93/3.05 [162]P60(x1622,x1623)+~E(x1621,x1622)+~P60(x1621,x1623) % 2.93/3.05 [163]P60(x1633,x1632)+~E(x1631,x1632)+~P60(x1633,x1631) % 2.93/3.05 [164]P67(x1642,x1643)+~E(x1641,x1642)+~P67(x1641,x1643) % 2.93/3.05 [165]P67(x1653,x1652)+~E(x1651,x1652)+~P67(x1653,x1651) % 2.93/3.05 % 2.93/3.05 %------------------------------------------- % 2.93/3.05 cnf(350,plain, % 2.93/3.05 (P65(a1,x3501)+~E(a6,x3501)), % 2.93/3.05 inference(scs_inference,[],[181,46,47])). % 2.93/3.05 cnf(402,plain, % 2.93/3.05 (P12(a1,a7,a15,x4021)+~E(a6,x4021)), % 2.93/3.05 inference(scs_inference,[],[194,193,75,76,77,78,79,80])). % 2.93/3.05 cnf(424,plain, % 2.93/3.05 (E(a6,a15)), % 2.93/3.05 inference(scs_inference,[],[194,2,282])). % 2.93/3.05 cnf(425,plain, % 2.93/3.05 (P65(a1,a15)), % 2.93/3.05 inference(scs_inference,[],[424,350])). % 2.93/3.05 cnf(426,plain, % 2.93/3.05 (E(a15,a6)), % 2.93/3.05 inference(scs_inference,[],[424,350,2])). % 2.93/3.05 cnf(430,plain, % 2.93/3.05 (P12(a1,a7,a15,a15)), % 2.93/3.05 inference(scs_inference,[],[194,193,180,424,350,2,79,76,45,80])). % 2.93/3.05 cnf(550,plain, % 2.93/3.05 (P35(x5501,x5502)+~P58(x5501,x5502)), % 2.93/3.05 inference(scs_inference,[],[199,200])). % 2.93/3.05 cnf(566,plain, % 2.93/3.05 (P9(x5661,x5662)+~P63(x5661,x5662)), % 2.93/3.05 inference(scs_inference,[],[201,222])). % 2.93/3.05 cnf(598,plain, % 2.93/3.05 (P35(a1,a16)), % 2.93/3.05 inference(scs_inference,[],[169,203,550])). % 2.93/3.05 cnf(619,plain, % 2.93/3.05 (P45(a1,a2)), % 2.93/3.05 inference(scs_inference,[],[170,204,205])). % 2.93/3.05 cnf(806,plain, % 2.93/3.05 (~P67(x8061,x8062)+P9(x8061,x8062)), % 2.93/3.05 inference(scs_inference,[],[218,566])). % 2.93/3.05 cnf(822,plain, % 2.93/3.05 (P9(x8221,x8222)+~P13(x8221,x8222)), % 2.93/3.05 inference(scs_inference,[],[219,806])). % 2.93/3.05 cnf(838,plain, % 2.93/3.05 (P9(a1,a18)), % 2.93/3.05 inference(scs_inference,[],[173,220,822])). % 2.93/3.05 cnf(1011,plain, % 2.93/3.05 (P10(a1,a15)), % 2.93/3.05 inference(scs_inference,[],[180,231,232])). % 2.93/3.05 cnf(1014,plain, % 2.93/3.05 (P10(a1,a6)), % 2.93/3.05 inference(scs_inference,[],[426,1011,255,105])). % 2.93/3.05 cnf(1019,plain, % 2.93/3.05 (~P39(a1,a15)), % 2.93/3.05 inference(scs_inference,[],[426,619,1011,255,105,243,104,121,205])). % 2.93/3.05 cnf(1023,plain, % 2.93/3.05 (~P35(a1,a15)), % 2.93/3.05 inference(scs_inference,[],[426,619,1011,255,105,243,104,121,205,206,222])). % 2.93/3.05 cnf(1025,plain, % 2.93/3.05 (~P68(a1,a15)), % 2.93/3.05 inference(scs_inference,[],[426,619,1011,255,105,243,104,121,205,206,222,223])). % 2.93/3.05 cnf(1027,plain, % 2.93/3.05 (~P19(a1,a15)), % 2.93/3.05 inference(scs_inference,[],[426,619,1011,255,105,243,104,121,205,206,222,223,224])). % 2.93/3.05 cnf(1029,plain, % 2.93/3.05 (~P67(a1,a15)), % 2.93/3.05 inference(scs_inference,[],[426,619,1011,255,105,243,104,121,205,206,222,223,224,806])). % 2.93/3.05 cnf(1036,plain, % 2.93/3.05 (~E(a15,a2)), % 2.93/3.05 inference(scs_inference,[],[430,426,424,598,619,838,1011,255,105,243,104,121,205,206,222,223,224,806,282,3,101,127,79])). % 2.93/3.05 cnf(1061,plain, % 2.93/3.05 ($false), % 2.93/3.05 inference(scs_inference,[],[425,1036,1014,1019,1023,1025,1027,1029,204,221,242,200,201,202,219,255,282,402,220,247]), % 2.93/3.05 ['proof']). % 2.93/3.05 % SZS output end Proof % 2.93/3.05 % Total time :2.410000s %------------------------------------------------------------------------------