%------------------------------------------------------------------------------ % 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/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n018.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:41 EDT 2024 % Result : Unsatisfiable 3.79s 3.88s % Output : CNFRefutation 3.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP204-1 : TPTP v8.2.0. Released v2.4.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n018.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:39:53 EDT 2024 % 0.12/0.33 % CPUTime : % 0.53/0.57 start to proof:theBenchmark % 3.79/3.86 %------------------------------------------- % 3.79/3.86 % File :CSE---1.7 % 3.79/3.86 % Problem :theBenchmark % 3.79/3.86 % Transform :cnf % 3.79/3.86 % Format :tptp:raw % 3.79/3.86 % Command :java -jar mcs_scs.jar %d %s % 3.79/3.86 % 3.79/3.86 % Result :Theorem 3.240000s % 3.79/3.86 % Output :CNFRefutation 3.240000s % 3.79/3.86 %------------------------------------------- % 3.79/3.86 %-------------------------------------------------------------------------- % 3.79/3.86 % File : NLP204-1 : TPTP v8.2.0. Released v2.4.0. % 3.79/3.86 % Domain : Natural Language Processing % 3.79/3.86 % Problem : An old dirty white Chevy, problem 91 % 3.79/3.86 % Version : [Bos00b] axioms. % 3.79/3.86 % English : Eliminating inconsistent interpretations in the statement % 3.79/3.86 % "An old dirty white chevy barrels down a lonely street in % 3.79/3.86 % hollywood. Two young fellas are in the front seat. They are % 3.79/3.86 % wearing cheap black coats. Jules is behind the wheel." % 3.79/3.86 % 3.79/3.86 % Refs : [Bos00a] Bos (2000), DORIS: Discourse Oriented Representation a % 3.79/3.86 % [Bos00b] Bos (2000), Applied Theorem Proving - Natural Language % 3.79/3.86 % Source : [TPTP] % 3.79/3.86 % Names : % 3.79/3.86 % 3.79/3.86 % Status : Unsatisfiable % 3.79/3.86 % Rating : 0.05 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.10 v5.5.0, 0.15 v5.4.0, 0.20 v5.3.0, 0.17 v5.2.0, 0.06 v5.1.0, 0.12 v5.0.0, 0.14 v4.1.0, 0.08 v4.0.1, 0.09 v3.7.0, 0.00 v3.3.0, 0.07 v3.2.0, 0.00 v2.4.0 % 3.79/3.86 % Syntax : Number of clauses : 120 ( 30 unt; 4 nHn; 113 RR) % 3.79/3.86 % Number of literals : 236 ( 11 equ; 123 neg) % 3.79/3.87 % Maximal clause size : 6 ( 1 avg) % 3.79/3.87 % Maximal term depth : 2 ( 1 avg) % 3.79/3.87 % Number of predicates : 72 ( 71 usr; 0 prp; 1-4 aty) % 3.79/3.87 % Number of functors : 18 ( 18 usr; 12 con; 0-4 aty) % 3.79/3.87 % Number of variables : 204 ( 30 sgn) % 3.79/3.87 % SPC : CNF_UNS_RFO_SEQ_NHN % 3.79/3.87 % 3.79/3.87 % Comments : Created from NLP204+1.p using FLOTTER % 3.79/3.87 %-------------------------------------------------------------------------- % 3.79/3.87 cnf(clause1,axiom, % 3.79/3.87 ~ member(U,V,V) ). % 3.79/3.87 % 3.79/3.87 cnf(clause2,axiom, % 3.79/3.87 ( ~ state(U,V) % 3.79/3.87 | eventuality(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause3,axiom, % 3.79/3.87 ( ~ eventuality(U,V) % 3.79/3.87 | thing(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause4,axiom, % 3.79/3.87 ( ~ thing(U,V) % 3.79/3.87 | singleton(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause5,axiom, % 3.79/3.87 ( ~ eventuality(U,V) % 3.79/3.87 | specific(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause6,axiom, % 3.79/3.87 ( ~ eventuality(U,V) % 3.79/3.87 | nonexistent(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause7,axiom, % 3.79/3.87 ( ~ eventuality(U,V) % 3.79/3.87 | unisex(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause8,axiom, % 3.79/3.87 ( ~ state(U,V) % 3.79/3.87 | event(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause9,axiom, % 3.79/3.87 ( ~ event(U,V) % 3.79/3.87 | eventuality(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause10,axiom, % 3.79/3.87 ( ~ wheel(U,V) % 3.79/3.87 | device(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause11,axiom, % 3.79/3.87 ( ~ device(U,V) % 3.79/3.87 | instrumentality(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause12,axiom, % 3.79/3.87 ( ~ instrumentality(U,V) % 3.79/3.87 | artifact(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause13,axiom, % 3.79/3.87 ( ~ artifact(U,V) % 3.79/3.87 | object(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause14,axiom, % 3.79/3.87 ( ~ object(U,V) % 3.79/3.87 | entity(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause15,axiom, % 3.79/3.87 ( ~ entity(U,V) % 3.79/3.87 | thing(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause16,axiom, % 3.79/3.87 ( ~ entity(U,V) % 3.79/3.87 | specific(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause17,axiom, % 3.79/3.87 ( ~ entity(U,V) % 3.79/3.87 | existent(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause18,axiom, % 3.79/3.87 ( ~ object(U,V) % 3.79/3.87 | nonliving(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause19,axiom, % 3.79/3.87 ( ~ object(U,V) % 3.79/3.87 | impartial(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause20,axiom, % 3.79/3.87 ( ~ object(U,V) % 3.79/3.87 | unisex(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause21,axiom, % 3.79/3.87 ( ~ coat(U,V) % 3.79/3.87 | clothes(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause22,axiom, % 3.79/3.87 ( ~ clothes(U,V) % 3.79/3.87 | artifact(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause23,axiom, % 3.79/3.87 ( ~ group(U,V) % 3.79/3.87 | set(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause24,axiom, % 3.79/3.87 ( ~ set(U,V) % 3.79/3.87 | multiple(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause25,axiom, % 3.79/3.87 ( ~ wear(U,V) % 3.79/3.87 | event(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause26,axiom, % 3.79/3.87 ( ~ fellow(U,V) % 3.79/3.87 | man(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause27,axiom, % 3.79/3.87 ( ~ man(U,V) % 3.79/3.87 | human_person(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause28,axiom, % 3.79/3.87 ( ~ human_person(U,V) % 3.79/3.87 | organism(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause29,axiom, % 3.79/3.87 ( ~ organism(U,V) % 3.79/3.87 | entity(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause30,axiom, % 3.79/3.87 ( ~ organism(U,V) % 3.79/3.87 | impartial(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause31,axiom, % 3.79/3.87 ( ~ organism(U,V) % 3.79/3.87 | living(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause32,axiom, % 3.79/3.87 ( ~ human_person(U,V) % 3.79/3.87 | human(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause33,axiom, % 3.79/3.87 ( ~ human_person(U,V) % 3.79/3.87 | animate(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause34,axiom, % 3.79/3.87 ( ~ man(U,V) % 3.79/3.87 | male(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause35,axiom, % 3.79/3.87 ( ~ two(U,V) % 3.79/3.87 | group(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause36,axiom, % 3.79/3.87 ( ~ barrel(U,V) % 3.79/3.87 | event(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause37,axiom, % 3.79/3.87 ( ~ street(U,V) % 3.79/3.87 | way(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause38,axiom, % 3.79/3.87 ( ~ way(U,V) % 3.79/3.87 | artifact(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause39,axiom, % 3.79/3.87 ( ~ chevy(U,V) % 3.79/3.87 | car(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause40,axiom, % 3.79/3.87 ( ~ car(U,V) % 3.79/3.87 | vehicle(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause41,axiom, % 3.79/3.87 ( ~ vehicle(U,V) % 3.79/3.87 | transport(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause42,axiom, % 3.79/3.87 ( ~ transport(U,V) % 3.79/3.87 | instrumentality(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause43,axiom, % 3.79/3.87 ( ~ placename(U,V) % 3.79/3.87 | relname(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause44,axiom, % 3.79/3.87 ( ~ relname(U,V) % 3.79/3.87 | relation(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause45,axiom, % 3.79/3.87 ( ~ relation(U,V) % 3.79/3.87 | abstraction(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause46,axiom, % 3.79/3.87 ( ~ abstraction(U,V) % 3.79/3.87 | thing(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause47,axiom, % 3.79/3.87 ( ~ abstraction(U,V) % 3.79/3.87 | nonhuman(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause48,axiom, % 3.79/3.87 ( ~ abstraction(U,V) % 3.79/3.87 | general(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause49,axiom, % 3.79/3.87 ( ~ abstraction(U,V) % 3.79/3.87 | unisex(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause50,axiom, % 3.79/3.87 ( ~ hollywood_placename(U,V) % 3.79/3.87 | placename(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause51,axiom, % 3.79/3.87 ( ~ city(U,V) % 3.79/3.87 | location(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause52,axiom, % 3.79/3.87 ( ~ location(U,V) % 3.79/3.87 | object(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause53,axiom, % 3.79/3.87 ( ~ frontseat(U,V) % 3.79/3.87 | seat(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause54,axiom, % 3.79/3.87 ( ~ seat(U,V) % 3.79/3.87 | furniture(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause55,axiom, % 3.79/3.87 ( ~ furniture(U,V) % 3.79/3.87 | instrumentality(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause56,axiom, % 3.79/3.87 ( ~ forename(U,V) % 3.79/3.87 | relname(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause57,axiom, % 3.79/3.87 ( ~ jules_forename(U,V) % 3.79/3.87 | forename(U,V) ) ). % 3.79/3.87 % 3.79/3.87 cnf(clause58,axiom, % 3.79/3.87 ( ~ old(U,V) % 3.79/3.87 | ~ young(U,V) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause59,axiom, % 3.79/3.88 ( ~ black(U,V) % 3.79/3.88 | ~ white(U,V) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause60,axiom, % 3.79/3.88 ( ~ male(U,V) % 3.79/3.88 | ~ unisex(U,V) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause61,axiom, % 3.79/3.88 ( ~ general(U,V) % 3.79/3.88 | ~ specific(U,V) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause62,axiom, % 3.79/3.88 ( ~ multiple(U,V) % 3.79/3.88 | ~ singleton(U,V) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause63,axiom, % 3.79/3.88 ( ~ living(U,V) % 3.79/3.88 | ~ nonliving(U,V) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause64,axiom, % 3.79/3.88 ( ~ human(U,V) % 3.79/3.88 | ~ nonhuman(U,V) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause65,axiom, % 3.79/3.88 ( ~ nonexistent(U,V) % 3.79/3.88 | ~ existent(U,V) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause66,axiom, % 3.79/3.88 ( ~ nonliving(U,V) % 3.79/3.88 | ~ animate(U,V) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause67,axiom, % 3.79/3.88 ( ~ be(U,V,W,X) % 3.79/3.88 | W = X ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause68,axiom, % 3.79/3.88 ( ~ two(U,V) % 3.79/3.88 | member(U,skf12(V,U),V) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause69,axiom, % 3.79/3.88 ( ~ two(U,V) % 3.79/3.88 | member(U,skf10(V,U),V) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause70,axiom, % 3.79/3.88 ( skf12(U,V) != skf10(U,V) % 3.79/3.88 | ~ two(V,U) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause71,axiom, % 3.79/3.88 ( ~ nonreflexive(U,V) % 3.79/3.88 | ~ patient(U,V,W) % 3.79/3.88 | ~ agent(U,V,W) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause72,axiom, % 3.79/3.88 ( ~ member(U,V,W) % 3.79/3.88 | ~ two(U,W) % 3.79/3.88 | V = skf10(W,U) % 3.79/3.88 | V = skf12(W,U) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause73,axiom, % 3.79/3.88 ( skf13(U,V,W,X) != V % 3.79/3.88 | ~ member(Y,U,Z) % 3.79/3.88 | ~ member(Y,V,Z) % 3.79/3.88 | two(Y,Z) % 3.79/3.88 | U = V ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause74,axiom, % 3.79/3.88 ( skf13(U,V,W,X) != U % 3.79/3.88 | ~ member(Y,U,Z) % 3.79/3.88 | ~ member(Y,X1,Z) % 3.79/3.88 | two(Y,Z) % 3.79/3.88 | U = X1 ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause75,axiom, % 3.79/3.88 ( ~ member(U,V,W) % 3.79/3.88 | ~ member(U,X,W) % 3.79/3.88 | two(U,W) % 3.79/3.88 | member(U,skf13(V,X,W,U),W) % 3.79/3.88 | V = X ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause76,axiom, % 3.79/3.88 ( ~ placename(U,V) % 3.79/3.88 | ~ of(U,W,X) % 3.79/3.88 | ~ placename(U,W) % 3.79/3.88 | ~ of(U,V,X) % 3.79/3.88 | ~ entity(U,X) % 3.79/3.88 | W = V ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause77,axiom, % 3.79/3.88 ( ~ forename(U,V) % 3.79/3.88 | ~ of(U,W,X) % 3.79/3.88 | ~ forename(U,W) % 3.79/3.88 | ~ of(U,V,X) % 3.79/3.88 | ~ entity(U,X) % 3.79/3.88 | W = V ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause78,negated_conjecture, % 3.79/3.88 actual_world(skc12) ). % 3.79/3.88 % 3.79/3.88 cnf(clause79,negated_conjecture, % 3.79/3.88 hollywood_placename(skc12,skc26) ). % 3.79/3.88 % 3.79/3.88 cnf(clause80,negated_conjecture, % 3.79/3.88 placename(skc12,skc26) ). % 3.79/3.88 % 3.79/3.88 cnf(clause81,negated_conjecture, % 3.79/3.88 lonely(skc12,skc25) ). % 3.79/3.88 % 3.79/3.88 cnf(clause82,negated_conjecture, % 3.79/3.88 street(skc12,skc25) ). % 3.79/3.88 % 3.79/3.88 cnf(clause83,negated_conjecture, % 3.79/3.88 city(skc12,skc25) ). % 3.79/3.88 % 3.79/3.88 cnf(clause84,negated_conjecture, % 3.79/3.88 frontseat(skc12,skc19) ). % 3.79/3.88 % 3.79/3.88 cnf(clause85,negated_conjecture, % 3.79/3.88 group(skc12,skc18) ). % 3.79/3.88 % 3.79/3.88 cnf(clause86,negated_conjecture, % 3.79/3.88 two(skc12,skc18) ). % 3.79/3.88 % 3.79/3.88 cnf(clause87,negated_conjecture, % 3.79/3.88 man(skc12,skc16) ). % 3.79/3.88 % 3.79/3.88 cnf(clause88,negated_conjecture, % 3.79/3.88 state(skc12,skc14) ). % 3.79/3.88 % 3.79/3.88 cnf(clause89,negated_conjecture, % 3.79/3.88 forename(skc12,skc15) ). % 3.79/3.88 % 3.79/3.88 cnf(clause90,negated_conjecture, % 3.79/3.88 jules_forename(skc12,skc15) ). % 3.79/3.88 % 3.79/3.88 cnf(clause91,negated_conjecture, % 3.79/3.88 wheel(skc12,skc13) ). % 3.79/3.88 % 3.79/3.88 cnf(clause92,negated_conjecture, % 3.79/3.88 group(skc12,skc17) ). % 3.79/3.88 % 3.79/3.88 cnf(clause93,negated_conjecture, % 3.79/3.88 old(skc12,skc27) ). % 3.79/3.88 % 3.79/3.88 cnf(clause94,negated_conjecture, % 3.79/3.88 dirty(skc12,skc27) ). % 3.79/3.88 % 3.79/3.88 cnf(clause95,negated_conjecture, % 3.79/3.88 white(skc12,skc27) ). % 3.79/3.88 % 3.79/3.88 cnf(clause96,negated_conjecture, % 3.79/3.88 chevy(skc12,skc27) ). % 3.79/3.88 % 3.79/3.88 cnf(clause97,negated_conjecture, % 3.79/3.88 event(skc12,skc24) ). % 3.79/3.88 % 3.79/3.88 cnf(clause98,negated_conjecture, % 3.79/3.88 present(skc12,skc24) ). % 3.79/3.88 % 3.79/3.88 cnf(clause99,negated_conjecture, % 3.79/3.88 barrel(skc12,skc24) ). % 3.79/3.88 % 3.79/3.88 cnf(clause100,negated_conjecture, % 3.79/3.88 agent(skc12,skc24,skc27) ). % 3.79/3.88 % 3.79/3.88 cnf(clause101,negated_conjecture, % 3.79/3.88 of(skc12,skc26,skc25) ). % 3.79/3.88 % 3.79/3.88 cnf(clause102,negated_conjecture, % 3.79/3.88 in(skc12,skc24,skc25) ). % 3.79/3.88 % 3.79/3.88 cnf(clause103,negated_conjecture, % 3.79/3.88 down(skc12,skc24,skc25) ). % 3.79/3.88 % 3.79/3.88 cnf(clause104,negated_conjecture, % 3.79/3.88 of(skc12,skc15,skc16) ). % 3.79/3.88 % 3.79/3.88 cnf(clause105,negated_conjecture, % 3.79/3.88 behind(skc12,skc13,skc13) ). % 3.79/3.88 % 3.79/3.88 cnf(clause106,negated_conjecture, % 3.79/3.88 be(skc12,skc14,skc16,skc13) ). % 3.79/3.88 % 3.79/3.88 cnf(clause107,negated_conjecture, % 3.79/3.88 ( ~ member(skc12,U,skc18) % 3.79/3.88 | young(skc12,U) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause108,negated_conjecture, % 3.79/3.88 ( ~ member(skc12,U,skc18) % 3.79/3.88 | fellow(skc12,U) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause109,negated_conjecture, % 3.79/3.88 ( ~ member(skc12,U,skc17) % 3.79/3.88 | cheap(skc12,U) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause110,negated_conjecture, % 3.79/3.88 ( ~ member(skc12,U,skc17) % 3.79/3.88 | black(skc12,U) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause111,negated_conjecture, % 3.79/3.88 ( ~ member(skc12,U,skc17) % 3.79/3.88 | coat(skc12,U) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause112,negated_conjecture, % 3.79/3.88 ( ~ member(skc12,U,skc18) % 3.79/3.88 | state(skc12,skf7(V)) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause113,negated_conjecture, % 3.79/3.88 ( ~ member(skc12,U,skc18) % 3.79/3.88 | in(skc12,skf6(V),skc19) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause114,negated_conjecture, % 3.79/3.88 ( ~ member(skc12,U,skc18) % 3.79/3.88 | be(skc12,skf7(U),U,skf6(U)) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause115,negated_conjecture, % 3.79/3.88 ( ~ member(skc12,U,skc18) % 3.79/3.88 | ~ member(skc12,V,skc17) % 3.79/3.88 | event(skc12,skf8(W,X)) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause116,negated_conjecture, % 3.79/3.88 ( ~ member(skc12,U,skc18) % 3.79/3.88 | ~ member(skc12,V,skc17) % 3.79/3.88 | present(skc12,skf8(W,X)) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause117,negated_conjecture, % 3.79/3.88 ( ~ member(skc12,U,skc18) % 3.79/3.88 | ~ member(skc12,V,skc17) % 3.79/3.88 | nonreflexive(skc12,skf8(W,X)) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause118,negated_conjecture, % 3.79/3.88 ( ~ member(skc12,U,skc18) % 3.79/3.88 | ~ member(skc12,V,skc17) % 3.79/3.88 | wear(skc12,skf8(W,X)) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause119,negated_conjecture, % 3.79/3.88 ( ~ member(skc12,U,skc18) % 3.79/3.88 | ~ member(skc12,V,skc17) % 3.79/3.88 | agent(skc12,skf8(U,W),U) ) ). % 3.79/3.88 % 3.79/3.88 cnf(clause120,negated_conjecture, % 3.79/3.88 ( ~ member(skc12,U,skc18) % 3.79/3.88 | ~ member(skc12,V,skc17) % 3.79/3.88 | patient(skc12,skf8(U,V),V) ) ). % 3.79/3.88 % 3.79/3.88 %-------------------------------------------------------------------------- % 3.79/3.88 %------------------------------------------- % 3.79/3.88 % Proof found % 3.79/3.88 % SZS status Theorem for theBenchmark % 3.79/3.88 % SZS output start Proof % 3.79/3.88 %ClaNum:285(EqnAxiom:165) % 3.79/3.88 %VarNum:424(SingletonVarNum:204) % 3.79/3.88 %MaxLitNum:6 % 3.79/3.88 %MaxfuncDepth:1 % 3.79/3.88 %SharedTerms:41 % 3.79/3.88 %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 % 3.79/3.88 %singleGoalClaCount:29 % 3.79/3.88 [166]P1(a1) % 3.79/3.88 [167]P3(a1,a2) % 3.79/3.88 [168]P4(a1,a4) % 3.79/3.88 [169]P61(a1,a3) % 3.79/3.88 [170]P22(a1,a5) % 3.79/3.88 [171]P22(a1,a6) % 3.79/3.88 [172]P30(a1,a7) % 3.79/3.88 [173]P62(a1,a5) % 3.79/3.88 [174]P5(a1,a4) % 3.79/3.88 [175]P63(a1,a10) % 3.79/3.88 [176]P9(a1,a11) % 3.79/3.88 [177]P42(a1,a12) % 3.79/3.88 [178]P31(a1,a12) % 3.79/3.88 [179]P15(a1,a10) % 3.79/3.88 [180]P23(a1,a9) % 3.79/3.88 [181]P24(a1,a8) % 3.79/3.88 [182]P32(a1,a8) % 3.79/3.88 [183]P43(a1,a11) % 3.79/3.88 [184]P70(a1,a11) % 3.79/3.88 [185]P38(a1,a10) % 3.79/3.88 [186]P16(a1,a11) % 3.79/3.88 [187]P54(a1,a4) % 3.79/3.88 [188]P6(a1,a4,a11) % 3.79/3.88 [189]P44(a1,a12,a10) % 3.79/3.88 [190]P44(a1,a8,a7) % 3.79/3.88 [191]P33(a1,a4,a10) % 3.79/3.88 [192]P20(a1,a4,a10) % 3.79/3.88 [193]P10(a1,a3,a3) % 3.79/3.88 [194]P11(a1,a2,a7,a3) % 3.79/3.88 [195]~P45(x1951,x1952,x1952) % 3.79/3.88 [262]P19(a1,x2621)+~P45(a1,x2621,a6) % 3.90/3.88 [263]P27(a1,x2631)+~P45(a1,x2631,a5) % 3.90/3.88 [264]P71(a1,x2641)+~P45(a1,x2641,a5) % 3.90/3.88 [265]P13(a1,x2651)+~P45(a1,x2651,a6) % 3.90/3.88 [266]P14(a1,x2661)+~P45(a1,x2661,a6) % 3.90/3.88 [281]P11(a1,f15(x2811),x2811,f16(x2811))+~P45(a1,x2811,a5) % 3.90/3.88 [196]~P3(x1961,x1962)+P25(x1961,x1962) % 3.90/3.88 [197]~P4(x1971,x1972)+P25(x1971,x1972) % 3.90/3.88 [198]~P25(x1981,x1982)+P64(x1981,x1982) % 3.90/3.88 [199]~P21(x1991,x1992)+P64(x1991,x1992) % 3.90/3.88 [200]~P2(x2001,x2002)+P64(x2001,x2002) % 3.90/3.88 [201]~P64(x2011,x2012)+P55(x2011,x2012) % 3.90/3.88 [202]~P25(x2021,x2022)+P60(x2021,x2022) % 3.90/3.88 [203]~P21(x2031,x2032)+P60(x2031,x2032) % 3.90/3.88 [204]~P25(x2041,x2042)+P46(x2041,x2042) % 3.90/3.88 [205]~P25(x2051,x2052)+P66(x2051,x2052) % 3.90/3.88 [206]~P48(x2061,x2062)+P66(x2061,x2062) % 3.90/3.88 [207]~P2(x2071,x2072)+P66(x2071,x2072) % 3.90/3.88 [208]~P3(x2081,x2082)+P4(x2081,x2082) % 3.90/3.88 [209]~P67(x2091,x2092)+P4(x2091,x2092) % 3.90/3.88 [210]~P5(x2101,x2102)+P4(x2101,x2102) % 3.90/3.88 [211]~P61(x2111,x2112)+P17(x2111,x2112) % 3.90/3.88 [212]~P17(x2121,x2122)+P37(x2121,x2122) % 3.90/3.88 [213]~P65(x2131,x2132)+P37(x2131,x2132) % 3.90/3.88 [214]~P28(x2141,x2142)+P37(x2141,x2142) % 3.90/3.88 [215]~P37(x2151,x2152)+P7(x2151,x2152) % 3.90/3.88 [216]~P18(x2161,x2162)+P7(x2161,x2162) % 3.90/3.88 [217]~P68(x2171,x2172)+P7(x2171,x2172) % 3.90/3.88 [218]~P7(x2181,x2182)+P48(x2181,x2182) % 3.90/3.88 [219]~P39(x2191,x2192)+P48(x2191,x2192) % 3.90/3.88 [220]~P48(x2201,x2202)+P21(x2201,x2202) % 3.90/3.88 [221]~P52(x2211,x2212)+P21(x2211,x2212) % 3.90/3.88 [222]~P21(x2221,x2222)+P26(x2221,x2222) % 3.90/3.88 [223]~P48(x2231,x2232)+P49(x2231,x2232) % 3.90/3.88 [224]~P48(x2241,x2242)+P34(x2241,x2242) % 3.90/3.88 [225]~P52(x2251,x2252)+P34(x2251,x2252) % 3.90/3.88 [226]~P19(x2261,x2262)+P18(x2261,x2262) % 3.90/3.88 [227]~P62(x2271,x2272)+P22(x2271,x2272) % 3.90/3.88 [228]~P22(x2281,x2282)+P56(x2281,x2282) % 3.90/3.88 [229]~P56(x2291,x2292)+P47(x2291,x2292) % 3.90/3.88 [230]~P27(x2301,x2302)+P30(x2301,x2302) % 3.90/3.88 [231]~P30(x2311,x2312)+P35(x2311,x2312) % 3.90/3.88 [232]~P35(x2321,x2322)+P52(x2321,x2322) % 3.90/3.88 [233]~P52(x2331,x2332)+P40(x2331,x2332) % 3.90/3.88 [234]~P35(x2341,x2342)+P36(x2341,x2342) % 3.90/3.88 [235]~P35(x2351,x2352)+P8(x2351,x2352) % 3.90/3.88 [236]~P30(x2361,x2362)+P41(x2361,x2362) % 3.90/3.88 [237]~P63(x2371,x2372)+P68(x2371,x2372) % 3.90/3.88 [238]~P9(x2381,x2382)+P12(x2381,x2382) % 3.90/3.88 [239]~P12(x2391,x2392)+P69(x2391,x2392) % 3.90/3.88 [240]~P69(x2401,x2402)+P65(x2401,x2402) % 3.90/3.88 [241]~P31(x2411,x2412)+P42(x2411,x2412) % 3.90/3.88 [242]~P42(x2421,x2422)+P57(x2421,x2422) % 3.90/3.88 [243]~P24(x2431,x2432)+P57(x2431,x2432) % 3.90/3.88 [244]~P57(x2441,x2442)+P58(x2441,x2442) % 3.90/3.88 [245]~P58(x2451,x2452)+P2(x2451,x2452) % 3.90/3.88 [246]~P2(x2461,x2462)+P50(x2461,x2462) % 3.90/3.88 [247]~P2(x2471,x2472)+P29(x2471,x2472) % 3.90/3.88 [248]~P15(x2481,x2482)+P39(x2481,x2482) % 3.90/3.88 [249]~P23(x2491,x2492)+P59(x2491,x2492) % 3.90/3.88 [250]~P59(x2501,x2502)+P28(x2501,x2502) % 3.90/3.88 [251]~P32(x2511,x2512)+P24(x2511,x2512) % 3.90/3.88 [252]~P47(x2521,x2522)+~P55(x2521,x2522) % 3.90/3.88 [253]~P29(x2531,x2532)+~P60(x2531,x2532) % 3.90/3.88 [254]~P26(x2541,x2542)+~P46(x2541,x2542) % 3.90/3.88 [255]~P41(x2551,x2552)+~P66(x2551,x2552) % 3.90/3.88 [256]~P40(x2561,x2562)+~P49(x2561,x2562) % 3.90/3.88 [257]~P8(x2571,x2572)+~P49(x2571,x2572) % 3.90/3.88 [258]~P50(x2581,x2582)+~P36(x2581,x2582) % 3.90/3.88 [259]~P71(x2591,x2592)+~P43(x2591,x2592) % 3.90/3.88 [260]~P70(x2601,x2602)+~P13(x2601,x2602) % 3.90/3.88 [261]~P62(x2612,x2611)+~E(f13(x2611,x2612),f14(x2611,x2612)) % 3.90/3.88 [267]~P45(a1,x2672,a5)+P3(a1,f15(x2671)) % 3.90/3.88 [268]~P62(x2681,x2682)+P45(x2681,f14(x2682,x2681),x2682) % 3.90/3.88 [269]~P62(x2691,x2692)+P45(x2691,f13(x2692,x2691),x2692) % 3.90/3.88 [270]~P45(a1,x2702,a5)+P33(a1,f16(x2701),a9) % 3.90/3.88 [282]E(x2821,x2822)+~P11(x2823,x2824,x2821,x2822) % 3.90/3.88 [277]~P45(a1,x2772,a6)+~P45(a1,x2771,a5)+P53(a1,f18(x2771,x2772),x2772) % 3.90/3.88 [272]~P6(x2721,x2722,x2723)+~P51(x2721,x2722)+~P53(x2721,x2722,x2723) % 3.90/3.88 [278]~P45(a1,x2781,a5)+P6(a1,f18(x2781,x2782),x2781)+~P45(a1,x2783,a6) % 3.90/3.88 [273]~P45(a1,x2733,a6)+~P45(a1,x2734,a5)+P4(a1,f18(x2731,x2732)) % 3.90/3.88 [274]~P45(a1,x2743,a6)+~P45(a1,x2744,a5)+P67(a1,f18(x2741,x2742)) % 3.90/3.88 [275]~P45(a1,x2753,a6)+~P45(a1,x2754,a5)+P51(a1,f18(x2751,x2752)) % 3.90/3.88 [276]~P45(a1,x2763,a6)+~P45(a1,x2764,a5)+P54(a1,f18(x2761,x2762)) % 3.90/3.88 [271]~P62(x2713,x2712)+~P45(x2713,x2711,x2712)+E(x2711,f13(x2712,x2713))+E(x2711,f14(x2712,x2713)) % 3.90/3.88 [285]~P45(x2853,x2852,x2854)+~P45(x2853,x2851,x2854)+E(x2851,x2852)+P62(x2853,x2854)+P45(x2853,f17(x2851,x2852,x2854,x2853),x2854) % 3.90/3.88 [284]~P45(x2843,x2842,x2844)+~P45(x2843,x2841,x2844)+E(x2841,x2842)+P62(x2843,x2844)+~E(f17(x2841,x2842,x2845,x2846),x2842) % 3.90/3.89 [283]~P45(x2833,x2832,x2834)+~P45(x2833,x2831,x2834)+E(x2831,x2832)+P62(x2833,x2834)+~E(f17(x2831,x2835,x2836,x2837),x2831) % 3.90/3.89 [279]~P42(x2793,x2792)+~P42(x2793,x2791)+~P44(x2793,x2792,x2794)+~P44(x2793,x2791,x2794)+E(x2791,x2792)+~P21(x2793,x2794) % 3.90/3.89 [280]~P24(x2803,x2802)+~P24(x2803,x2801)+~P44(x2803,x2802,x2804)+~P44(x2803,x2801,x2804)+E(x2801,x2802)+~P21(x2803,x2804) % 3.90/3.89 %EqnAxiom % 3.90/3.89 [1]E(x11,x11) % 3.90/3.89 [2]E(x22,x21)+~E(x21,x22) % 3.90/3.89 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 3.90/3.89 [4]~E(x41,x42)+E(f13(x41,x43),f13(x42,x43)) % 3.90/3.89 [5]~E(x51,x52)+E(f13(x53,x51),f13(x53,x52)) % 3.90/3.89 [6]~E(x61,x62)+E(f14(x61,x63),f14(x62,x63)) % 3.90/3.89 [7]~E(x71,x72)+E(f14(x73,x71),f14(x73,x72)) % 3.90/3.89 [8]~E(x81,x82)+E(f15(x81),f15(x82)) % 3.90/3.89 [9]~E(x91,x92)+E(f17(x91,x93,x94,x95),f17(x92,x93,x94,x95)) % 3.90/3.89 [10]~E(x101,x102)+E(f17(x103,x101,x104,x105),f17(x103,x102,x104,x105)) % 3.90/3.89 [11]~E(x111,x112)+E(f17(x113,x114,x111,x115),f17(x113,x114,x112,x115)) % 3.90/3.89 [12]~E(x121,x122)+E(f17(x123,x124,x125,x121),f17(x123,x124,x125,x122)) % 3.90/3.89 [13]~E(x131,x132)+E(f18(x131,x133),f18(x132,x133)) % 3.90/3.89 [14]~E(x141,x142)+E(f18(x143,x141),f18(x143,x142)) % 3.90/3.89 [15]~E(x151,x152)+E(f16(x151),f16(x152)) % 3.90/3.89 [16]~P1(x161)+P1(x162)+~E(x161,x162) % 3.90/3.89 [17]P3(x172,x173)+~E(x171,x172)+~P3(x171,x173) % 3.90/3.89 [18]P3(x183,x182)+~E(x181,x182)+~P3(x183,x181) % 3.90/3.89 [19]P4(x192,x193)+~E(x191,x192)+~P4(x191,x193) % 3.90/3.89 [20]P4(x203,x202)+~E(x201,x202)+~P4(x203,x201) % 3.90/3.89 [21]P61(x212,x213)+~E(x211,x212)+~P61(x211,x213) % 3.90/3.89 [22]P61(x223,x222)+~E(x221,x222)+~P61(x223,x221) % 3.90/3.89 [23]P22(x232,x233)+~E(x231,x232)+~P22(x231,x233) % 3.90/3.89 [24]P22(x243,x242)+~E(x241,x242)+~P22(x243,x241) % 3.90/3.89 [25]P62(x252,x253)+~E(x251,x252)+~P62(x251,x253) % 3.90/3.89 [26]P62(x263,x262)+~E(x261,x262)+~P62(x263,x261) % 3.90/3.89 [27]P30(x272,x273)+~E(x271,x272)+~P30(x271,x273) % 3.90/3.89 [28]P30(x283,x282)+~E(x281,x282)+~P30(x283,x281) % 3.90/3.89 [29]P11(x292,x293,x294,x295)+~E(x291,x292)+~P11(x291,x293,x294,x295) % 3.90/3.89 [30]P11(x303,x302,x304,x305)+~E(x301,x302)+~P11(x303,x301,x304,x305) % 3.90/3.89 [31]P11(x313,x314,x312,x315)+~E(x311,x312)+~P11(x313,x314,x311,x315) % 3.90/3.89 [32]P11(x323,x324,x325,x322)+~E(x321,x322)+~P11(x323,x324,x325,x321) % 3.90/3.89 [33]P5(x332,x333)+~E(x331,x332)+~P5(x331,x333) % 3.90/3.89 [34]P5(x343,x342)+~E(x341,x342)+~P5(x343,x341) % 3.90/3.89 [35]P63(x352,x353)+~E(x351,x352)+~P63(x351,x353) % 3.90/3.89 [36]P63(x363,x362)+~E(x361,x362)+~P63(x363,x361) % 3.90/3.89 [37]P9(x372,x373)+~E(x371,x372)+~P9(x371,x373) % 3.90/3.89 [38]P9(x383,x382)+~E(x381,x382)+~P9(x383,x381) % 3.90/3.89 [39]P42(x392,x393)+~E(x391,x392)+~P42(x391,x393) % 3.90/3.89 [40]P42(x403,x402)+~E(x401,x402)+~P42(x403,x401) % 3.90/3.89 [41]P31(x412,x413)+~E(x411,x412)+~P31(x411,x413) % 3.90/3.89 [42]P31(x423,x422)+~E(x421,x422)+~P31(x423,x421) % 3.90/3.89 [43]P15(x432,x433)+~E(x431,x432)+~P15(x431,x433) % 3.90/3.89 [44]P15(x443,x442)+~E(x441,x442)+~P15(x443,x441) % 3.90/3.89 [45]P23(x452,x453)+~E(x451,x452)+~P23(x451,x453) % 3.90/3.89 [46]P23(x463,x462)+~E(x461,x462)+~P23(x463,x461) % 3.90/3.89 [47]P24(x472,x473)+~E(x471,x472)+~P24(x471,x473) % 3.90/3.89 [48]P24(x483,x482)+~E(x481,x482)+~P24(x483,x481) % 3.90/3.89 [49]P32(x492,x493)+~E(x491,x492)+~P32(x491,x493) % 3.90/3.89 [50]P32(x503,x502)+~E(x501,x502)+~P32(x503,x501) % 3.90/3.89 [51]P43(x512,x513)+~E(x511,x512)+~P43(x511,x513) % 3.90/3.89 [52]P43(x523,x522)+~E(x521,x522)+~P43(x523,x521) % 3.90/3.89 [53]P70(x532,x533)+~E(x531,x532)+~P70(x531,x533) % 3.90/3.89 [54]P70(x543,x542)+~E(x541,x542)+~P70(x543,x541) % 3.90/3.89 [55]P38(x552,x553)+~E(x551,x552)+~P38(x551,x553) % 3.90/3.89 [56]P38(x563,x562)+~E(x561,x562)+~P38(x563,x561) % 3.90/3.89 [57]P16(x572,x573)+~E(x571,x572)+~P16(x571,x573) % 3.90/3.89 [58]P16(x583,x582)+~E(x581,x582)+~P16(x583,x581) % 3.90/3.89 [59]P54(x592,x593)+~E(x591,x592)+~P54(x591,x593) % 3.90/3.89 [60]P54(x603,x602)+~E(x601,x602)+~P54(x603,x601) % 3.90/3.89 [61]P6(x612,x613,x614)+~E(x611,x612)+~P6(x611,x613,x614) % 3.90/3.89 [62]P6(x623,x622,x624)+~E(x621,x622)+~P6(x623,x621,x624) % 3.90/3.89 [63]P6(x633,x634,x632)+~E(x631,x632)+~P6(x633,x634,x631) % 3.90/3.89 [64]P44(x642,x643,x644)+~E(x641,x642)+~P44(x641,x643,x644) % 3.90/3.89 [65]P44(x653,x652,x654)+~E(x651,x652)+~P44(x653,x651,x654) % 3.90/3.89 [66]P44(x663,x664,x662)+~E(x661,x662)+~P44(x663,x664,x661) % 3.90/3.89 [67]P45(x672,x673,x674)+~E(x671,x672)+~P45(x671,x673,x674) % 3.90/3.89 [68]P45(x683,x682,x684)+~E(x681,x682)+~P45(x683,x681,x684) % 3.90/3.89 [69]P45(x693,x694,x692)+~E(x691,x692)+~P45(x693,x694,x691) % 3.90/3.89 [70]P33(x702,x703,x704)+~E(x701,x702)+~P33(x701,x703,x704) % 3.90/3.89 [71]P33(x713,x712,x714)+~E(x711,x712)+~P33(x713,x711,x714) % 3.90/3.89 [72]P33(x723,x724,x722)+~E(x721,x722)+~P33(x723,x724,x721) % 3.90/3.89 [73]P20(x732,x733,x734)+~E(x731,x732)+~P20(x731,x733,x734) % 3.90/3.89 [74]P20(x743,x742,x744)+~E(x741,x742)+~P20(x743,x741,x744) % 3.90/3.89 [75]P20(x753,x754,x752)+~E(x751,x752)+~P20(x753,x754,x751) % 3.90/3.89 [76]P10(x762,x763,x764)+~E(x761,x762)+~P10(x761,x763,x764) % 3.90/3.89 [77]P10(x773,x772,x774)+~E(x771,x772)+~P10(x773,x771,x774) % 3.90/3.89 [78]P10(x783,x784,x782)+~E(x781,x782)+~P10(x783,x784,x781) % 3.90/3.89 [79]P21(x792,x793)+~E(x791,x792)+~P21(x791,x793) % 3.90/3.89 [80]P21(x803,x802)+~E(x801,x802)+~P21(x803,x801) % 3.90/3.89 [81]P14(x812,x813)+~E(x811,x812)+~P14(x811,x813) % 3.90/3.89 [82]P14(x823,x822)+~E(x821,x822)+~P14(x823,x821) % 3.90/3.89 [83]P25(x832,x833)+~E(x831,x832)+~P25(x831,x833) % 3.90/3.89 [84]P25(x843,x842)+~E(x841,x842)+~P25(x843,x841) % 3.90/3.89 [85]P13(x852,x853)+~E(x851,x852)+~P13(x851,x853) % 3.90/3.89 [86]P13(x863,x862)+~E(x861,x862)+~P13(x863,x861) % 3.90/3.89 [87]P51(x872,x873)+~E(x871,x872)+~P51(x871,x873) % 3.90/3.89 [88]P51(x883,x882)+~E(x881,x882)+~P51(x883,x881) % 3.90/3.89 [89]P60(x892,x893)+~E(x891,x892)+~P60(x891,x893) % 3.90/3.89 [90]P60(x903,x902)+~E(x901,x902)+~P60(x903,x901) % 3.90/3.89 [91]P64(x912,x913)+~E(x911,x912)+~P64(x911,x913) % 3.90/3.89 [92]P64(x923,x922)+~E(x921,x922)+~P64(x923,x921) % 3.90/3.89 [93]P59(x932,x933)+~E(x931,x932)+~P59(x931,x933) % 3.90/3.89 [94]P59(x943,x942)+~E(x941,x942)+~P59(x943,x941) % 3.90/3.89 [95]P2(x952,x953)+~E(x951,x952)+~P2(x951,x953) % 3.90/3.89 [96]P2(x963,x962)+~E(x961,x962)+~P2(x963,x961) % 3.90/3.89 [97]P47(x972,x973)+~E(x971,x972)+~P47(x971,x973) % 3.90/3.89 [98]P47(x983,x982)+~E(x981,x982)+~P47(x983,x981) % 3.90/3.89 [99]P57(x992,x993)+~E(x991,x992)+~P57(x991,x993) % 3.90/3.89 [100]P57(x1003,x1002)+~E(x1001,x1002)+~P57(x1003,x1001) % 3.90/3.89 [101]P69(x1012,x1013)+~E(x1011,x1012)+~P69(x1011,x1013) % 3.90/3.89 [102]P69(x1023,x1022)+~E(x1021,x1022)+~P69(x1023,x1021) % 3.90/3.89 [103]P55(x1032,x1033)+~E(x1031,x1032)+~P55(x1031,x1033) % 3.90/3.89 [104]P55(x1043,x1042)+~E(x1041,x1042)+~P55(x1043,x1041) % 3.90/3.89 [105]P58(x1052,x1053)+~E(x1051,x1052)+~P58(x1051,x1053) % 3.90/3.89 [106]P58(x1063,x1062)+~E(x1061,x1062)+~P58(x1063,x1061) % 3.90/3.89 [107]P50(x1072,x1073)+~E(x1071,x1072)+~P50(x1071,x1073) % 3.90/3.89 [108]P50(x1083,x1082)+~E(x1081,x1082)+~P50(x1083,x1081) % 3.90/3.89 [109]P46(x1092,x1093)+~E(x1091,x1092)+~P46(x1091,x1093) % 3.90/3.89 [110]P46(x1103,x1102)+~E(x1101,x1102)+~P46(x1103,x1101) % 3.90/3.89 [111]P49(x1112,x1113)+~E(x1111,x1112)+~P49(x1111,x1113) % 3.90/3.89 [112]P49(x1123,x1122)+~E(x1121,x1122)+~P49(x1123,x1121) % 3.90/3.89 [113]P12(x1132,x1133)+~E(x1131,x1132)+~P12(x1131,x1133) % 3.90/3.89 [114]P12(x1143,x1142)+~E(x1141,x1142)+~P12(x1143,x1141) % 3.90/3.89 [115]P40(x1152,x1153)+~E(x1151,x1152)+~P40(x1151,x1153) % 3.90/3.89 [116]P40(x1163,x1162)+~E(x1161,x1162)+~P40(x1163,x1161) % 3.90/3.89 [117]P39(x1172,x1173)+~E(x1171,x1172)+~P39(x1171,x1173) % 3.90/3.89 [118]P39(x1183,x1182)+~E(x1181,x1182)+~P39(x1183,x1181) % 3.90/3.89 [119]P66(x1192,x1193)+~E(x1191,x1192)+~P66(x1191,x1193) % 3.90/3.89 [120]P66(x1203,x1202)+~E(x1201,x1202)+~P66(x1203,x1201) % 3.90/3.89 [121]P53(x1212,x1213,x1214)+~E(x1211,x1212)+~P53(x1211,x1213,x1214) % 3.90/3.89 [122]P53(x1223,x1222,x1224)+~E(x1221,x1222)+~P53(x1223,x1221,x1224) % 3.90/3.89 [123]P53(x1233,x1234,x1232)+~E(x1231,x1232)+~P53(x1233,x1234,x1231) % 3.90/3.89 [124]P35(x1242,x1243)+~E(x1241,x1242)+~P35(x1241,x1243) % 3.90/3.89 [125]P35(x1253,x1252)+~E(x1251,x1252)+~P35(x1253,x1251) % 3.90/3.89 [126]P48(x1262,x1263)+~E(x1261,x1262)+~P48(x1261,x1263) % 3.90/3.89 [127]P48(x1273,x1272)+~E(x1271,x1272)+~P48(x1273,x1271) % 3.90/3.89 [128]P36(x1282,x1283)+~E(x1281,x1282)+~P36(x1281,x1283) % 3.90/3.89 [129]P36(x1293,x1292)+~E(x1291,x1292)+~P36(x1293,x1291) % 3.90/3.89 [130]P65(x1302,x1303)+~E(x1301,x1302)+~P65(x1301,x1303) % 3.90/3.89 [131]P65(x1313,x1312)+~E(x1311,x1312)+~P65(x1313,x1311) % 3.90/3.89 [132]P71(x1322,x1323)+~E(x1321,x1322)+~P71(x1321,x1323) % 3.90/3.89 [133]P71(x1333,x1332)+~E(x1331,x1332)+~P71(x1333,x1331) % 3.90/3.89 [134]P27(x1342,x1343)+~E(x1341,x1342)+~P27(x1341,x1343) % 3.90/3.89 [135]P27(x1353,x1352)+~E(x1351,x1352)+~P27(x1353,x1351) % 3.90/3.89 [136]P19(x1362,x1363)+~E(x1361,x1362)+~P19(x1361,x1363) % 3.90/3.89 [137]P19(x1373,x1372)+~E(x1371,x1372)+~P19(x1373,x1371) % 3.90/3.89 [138]P67(x1382,x1383)+~E(x1381,x1382)+~P67(x1381,x1383) % 3.90/3.89 [139]P67(x1393,x1392)+~E(x1391,x1392)+~P67(x1393,x1391) % 3.90/3.89 [140]P29(x1402,x1403)+~E(x1401,x1402)+~P29(x1401,x1403) % 3.90/3.89 [141]P29(x1413,x1412)+~E(x1411,x1412)+~P29(x1413,x1411) % 3.90/3.89 [142]P52(x1422,x1423)+~E(x1421,x1422)+~P52(x1421,x1423) % 3.90/3.89 [143]P52(x1433,x1432)+~E(x1431,x1432)+~P52(x1433,x1431) % 3.90/3.89 [144]P17(x1442,x1443)+~E(x1441,x1442)+~P17(x1441,x1443) % 3.90/3.89 [145]P17(x1453,x1452)+~E(x1451,x1452)+~P17(x1453,x1451) % 3.90/3.89 [146]P8(x1462,x1463)+~E(x1461,x1462)+~P8(x1461,x1463) % 3.90/3.89 [147]P8(x1473,x1472)+~E(x1471,x1472)+~P8(x1473,x1471) % 3.90/3.89 [148]P37(x1482,x1483)+~E(x1481,x1482)+~P37(x1481,x1483) % 3.90/3.89 [149]P37(x1493,x1492)+~E(x1491,x1492)+~P37(x1493,x1491) % 3.90/3.89 [150]P56(x1502,x1503)+~E(x1501,x1502)+~P56(x1501,x1503) % 3.90/3.89 [151]P56(x1513,x1512)+~E(x1511,x1512)+~P56(x1513,x1511) % 3.90/3.89 [152]P26(x1522,x1523)+~E(x1521,x1522)+~P26(x1521,x1523) % 3.90/3.89 [153]P26(x1533,x1532)+~E(x1531,x1532)+~P26(x1533,x1531) % 3.90/3.89 [154]P18(x1542,x1543)+~E(x1541,x1542)+~P18(x1541,x1543) % 3.90/3.89 [155]P18(x1553,x1552)+~E(x1551,x1552)+~P18(x1553,x1551) % 3.90/3.89 [156]P41(x1562,x1563)+~E(x1561,x1562)+~P41(x1561,x1563) % 3.90/3.89 [157]P41(x1573,x1572)+~E(x1571,x1572)+~P41(x1573,x1571) % 3.90/3.89 [158]P28(x1582,x1583)+~E(x1581,x1582)+~P28(x1581,x1583) % 3.90/3.89 [159]P28(x1593,x1592)+~E(x1591,x1592)+~P28(x1593,x1591) % 3.90/3.89 [160]P7(x1602,x1603)+~E(x1601,x1602)+~P7(x1601,x1603) % 3.90/3.89 [161]P7(x1613,x1612)+~E(x1611,x1612)+~P7(x1613,x1611) % 3.90/3.89 [162]P34(x1622,x1623)+~E(x1621,x1622)+~P34(x1621,x1623) % 3.90/3.89 [163]P34(x1633,x1632)+~E(x1631,x1632)+~P34(x1633,x1631) % 3.90/3.89 [164]P68(x1642,x1643)+~E(x1641,x1642)+~P68(x1641,x1643) % 3.90/3.89 [165]P68(x1653,x1652)+~E(x1651,x1652)+~P68(x1653,x1651) % 3.90/3.89 % 3.90/3.89 %------------------------------------------- % 3.90/3.89 cnf(422,plain, % 3.90/3.89 (E(a3,a7)), % 3.90/3.89 inference(scs_inference,[],[194,2,282])). % 3.90/3.89 cnf(650,plain, % 3.90/3.89 (~P48(x6501,x6502)+~P41(x6501,x6502)), % 3.90/3.89 inference(scs_inference,[],[206,255])). % 3.90/3.89 cnf(740,plain, % 3.90/3.89 (P37(a1,a3)), % 3.90/3.89 inference(scs_inference,[],[169,211,212])). % 3.90/3.89 cnf(741,plain, % 3.90/3.89 (P37(a1,a7)), % 3.90/3.89 inference(scs_inference,[],[422,740,149])). % 3.90/3.89 cnf(795,plain, % 3.90/3.89 (P48(x7951,x7952)+~P18(x7951,x7952)), % 3.90/3.89 inference(scs_inference,[],[216,218])). % 3.90/3.89 cnf(907,plain, % 3.90/3.89 (~P19(x9071,x9072)+P48(x9071,x9072)), % 3.90/3.89 inference(scs_inference,[],[226,795])). % 3.90/3.89 cnf(1231,plain, % 3.90/3.89 (~P48(a1,a7)), % 3.90/3.89 inference(scs_inference,[],[172,650,236])). % 3.90/3.89 cnf(1244,plain, % 3.90/3.89 ($false), % 3.90/3.89 inference(scs_inference,[],[741,1231,219,907,218,217,237,248,215]), % 3.90/3.89 ['proof']). % 3.90/3.89 % SZS output end Proof % 3.90/3.89 % Total time :3.240000s %------------------------------------------------------------------------------