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