%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NLP141-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 : n026.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:23 EDT 2024 % Result : Unsatisfiable 7.95s 7.96s % Output : CNFRefutation 7.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : NLP141-1 : TPTP v8.2.0. Released v2.4.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n026.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sat Jun 22 03:17:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.47/0.61 start to proof:theBenchmark % 7.92/7.94 %------------------------------------------- % 7.92/7.94 % File :CSE---1.7 % 7.92/7.94 % Problem :theBenchmark % 7.92/7.94 % Transform :cnf % 7.92/7.94 % Format :tptp:raw % 7.92/7.94 % Command :java -jar mcs_scs.jar %d %s % 7.92/7.94 % 7.92/7.94 % Result :Theorem 7.280000s % 7.92/7.94 % Output :CNFRefutation 7.280000s % 7.92/7.94 %------------------------------------------- % 7.92/7.94 %-------------------------------------------------------------------------- % 7.92/7.94 % File : NLP141-1 : TPTP v8.2.0. Released v2.4.0. % 7.92/7.94 % Domain : Natural Language Processing % 7.92/7.94 % Problem : An old dirty white Chevy, problem 28 % 7.92/7.94 % Version : [Bos00b] axioms. % 7.92/7.94 % English : Eliminating inconsistent interpretations in the statement % 7.92/7.94 % "An old dirty white chevy barrels down a lonely street in % 7.92/7.94 % hollywood. Two young fellas are in the front seat." % 7.92/7.94 % 7.92/7.94 % Refs : [Bos00a] Bos (2000), DORIS: Discourse Oriented Representation a % 7.92/7.94 % [Bos00b] Bos (2000), Applied Theorem Proving - Natural Language % 7.92/7.94 % Source : [TPTP] % 7.92/7.94 % Names : % 7.92/7.94 % 7.92/7.94 % Status : Unsatisfiable % 7.92/7.94 % Rating : 0.10 v8.1.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.3.0, 0.09 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.10 v5.5.0, 0.15 v5.3.0, 0.17 v5.2.0, 0.12 v5.0.0, 0.07 v4.1.0, 0.08 v4.0.1, 0.09 v4.0.0, 0.00 v3.3.0, 0.07 v3.2.0, 0.15 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.5.0, 0.11 v2.4.0 % 7.92/7.94 % Syntax : Number of clauses : 92 ( 20 unt; 4 nHn; 89 RR) % 7.92/7.94 % Number of literals : 179 ( 10 equ; 92 neg) % 7.92/7.94 % Maximal clause size : 6 ( 1 avg) % 7.92/7.94 % Maximal term depth : 2 ( 1 avg) % 7.92/7.94 % Number of predicates : 60 ( 59 usr; 0 prp; 1-4 aty) % 7.92/7.94 % Number of functors : 11 ( 11 usr; 6 con; 0-4 aty) % 7.92/7.94 % Number of variables : 159 ( 13 sgn) % 7.92/7.94 % SPC : CNF_UNS_RFO_SEQ_NHN % 7.92/7.94 % 7.92/7.94 % Comments : Created from NLP141+1.p using FLOTTER % 7.92/7.94 %-------------------------------------------------------------------------- % 7.92/7.94 cnf(clause1,axiom, % 7.92/7.94 ~ member(U,V,V) ). % 7.92/7.94 % 7.92/7.94 cnf(clause2,axiom, % 7.92/7.94 ( ~ fellow(U,V) % 7.92/7.94 | man(U,V) ) ). % 7.92/7.94 % 7.92/7.94 cnf(clause3,axiom, % 7.92/7.94 ( ~ man(U,V) % 7.92/7.94 | human_person(U,V) ) ). % 7.92/7.94 % 7.92/7.94 cnf(clause4,axiom, % 7.92/7.94 ( ~ human_person(U,V) % 7.92/7.94 | organism(U,V) ) ). % 7.92/7.94 % 7.92/7.94 cnf(clause5,axiom, % 7.92/7.94 ( ~ organism(U,V) % 7.92/7.94 | entity(U,V) ) ). % 7.92/7.94 % 7.92/7.94 cnf(clause6,axiom, % 7.92/7.94 ( ~ entity(U,V) % 7.92/7.94 | thing(U,V) ) ). % 7.92/7.94 % 7.92/7.94 cnf(clause7,axiom, % 7.92/7.94 ( ~ thing(U,V) % 7.92/7.94 | singleton(U,V) ) ). % 7.92/7.94 % 7.92/7.94 cnf(clause8,axiom, % 7.92/7.94 ( ~ entity(U,V) % 7.92/7.94 | specific(U,V) ) ). % 7.92/7.94 % 7.92/7.94 cnf(clause9,axiom, % 7.92/7.94 ( ~ entity(U,V) % 7.92/7.94 | existent(U,V) ) ). % 7.92/7.94 % 7.92/7.94 cnf(clause10,axiom, % 7.92/7.94 ( ~ organism(U,V) % 7.92/7.94 | impartial(U,V) ) ). % 7.92/7.94 % 7.92/7.94 cnf(clause11,axiom, % 7.92/7.94 ( ~ organism(U,V) % 7.92/7.94 | living(U,V) ) ). % 7.92/7.94 % 7.92/7.94 cnf(clause12,axiom, % 7.92/7.94 ( ~ human_person(U,V) % 7.92/7.94 | human(U,V) ) ). % 7.92/7.94 % 7.92/7.94 cnf(clause13,axiom, % 7.92/7.94 ( ~ human_person(U,V) % 7.92/7.95 | animate(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause14,axiom, % 7.92/7.95 ( ~ man(U,V) % 7.92/7.95 | male(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause15,axiom, % 7.92/7.95 ( ~ group(U,V) % 7.92/7.95 | set(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause16,axiom, % 7.92/7.95 ( ~ set(U,V) % 7.92/7.95 | multiple(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause17,axiom, % 7.92/7.95 ( ~ two(U,V) % 7.92/7.95 | group(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause18,axiom, % 7.92/7.95 ( ~ state(U,V) % 7.92/7.95 | eventuality(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause19,axiom, % 7.92/7.95 ( ~ eventuality(U,V) % 7.92/7.95 | thing(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause20,axiom, % 7.92/7.95 ( ~ eventuality(U,V) % 7.92/7.95 | specific(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause21,axiom, % 7.92/7.95 ( ~ eventuality(U,V) % 7.92/7.95 | nonexistent(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause22,axiom, % 7.92/7.95 ( ~ eventuality(U,V) % 7.92/7.95 | unisex(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause23,axiom, % 7.92/7.95 ( ~ state(U,V) % 7.92/7.95 | event(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause24,axiom, % 7.92/7.95 ( ~ event(U,V) % 7.92/7.95 | eventuality(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause25,axiom, % 7.92/7.95 ( ~ barrel(U,V) % 7.92/7.95 | event(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause26,axiom, % 7.92/7.95 ( ~ chevy(U,V) % 7.92/7.95 | car(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause27,axiom, % 7.92/7.95 ( ~ car(U,V) % 7.92/7.95 | vehicle(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause28,axiom, % 7.92/7.95 ( ~ vehicle(U,V) % 7.92/7.95 | transport(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause29,axiom, % 7.92/7.95 ( ~ transport(U,V) % 7.92/7.95 | instrumentality(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause30,axiom, % 7.92/7.95 ( ~ instrumentality(U,V) % 7.92/7.95 | artifact(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause31,axiom, % 7.92/7.95 ( ~ artifact(U,V) % 7.92/7.95 | object(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause32,axiom, % 7.92/7.95 ( ~ object(U,V) % 7.92/7.95 | entity(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause33,axiom, % 7.92/7.95 ( ~ object(U,V) % 7.92/7.95 | nonliving(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause34,axiom, % 7.92/7.95 ( ~ object(U,V) % 7.92/7.95 | impartial(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause35,axiom, % 7.92/7.95 ( ~ object(U,V) % 7.92/7.95 | unisex(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause36,axiom, % 7.92/7.95 ( ~ street(U,V) % 7.92/7.95 | way(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause37,axiom, % 7.92/7.95 ( ~ way(U,V) % 7.92/7.95 | artifact(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause38,axiom, % 7.92/7.95 ( ~ placename(U,V) % 7.92/7.95 | relname(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause39,axiom, % 7.92/7.95 ( ~ relname(U,V) % 7.92/7.95 | relation(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause40,axiom, % 7.92/7.95 ( ~ relation(U,V) % 7.92/7.95 | abstraction(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause41,axiom, % 7.92/7.95 ( ~ abstraction(U,V) % 7.92/7.95 | thing(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause42,axiom, % 7.92/7.95 ( ~ abstraction(U,V) % 7.92/7.95 | nonhuman(U,V) ) ). % 7.92/7.95 % 7.92/7.95 cnf(clause43,axiom, % 7.92/7.95 ( ~ abstraction(U,V) % 7.92/7.95 | general(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause44,axiom, % 7.95/7.95 ( ~ abstraction(U,V) % 7.95/7.95 | unisex(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause45,axiom, % 7.95/7.95 ( ~ hollywood_placename(U,V) % 7.95/7.95 | placename(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause46,axiom, % 7.95/7.95 ( ~ city(U,V) % 7.95/7.95 | location(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause47,axiom, % 7.95/7.95 ( ~ location(U,V) % 7.95/7.95 | object(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause48,axiom, % 7.95/7.95 ( ~ frontseat(U,V) % 7.95/7.95 | seat(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause49,axiom, % 7.95/7.95 ( ~ seat(U,V) % 7.95/7.95 | furniture(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause50,axiom, % 7.95/7.95 ( ~ furniture(U,V) % 7.95/7.95 | instrumentality(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause51,axiom, % 7.95/7.95 ( ~ old(U,V) % 7.95/7.95 | ~ young(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause52,axiom, % 7.95/7.95 ( ~ male(U,V) % 7.95/7.95 | ~ unisex(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause53,axiom, % 7.95/7.95 ( ~ general(U,V) % 7.95/7.95 | ~ specific(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause54,axiom, % 7.95/7.95 ( ~ multiple(U,V) % 7.95/7.95 | ~ singleton(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause55,axiom, % 7.95/7.95 ( ~ living(U,V) % 7.95/7.95 | ~ nonliving(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause56,axiom, % 7.95/7.95 ( ~ human(U,V) % 7.95/7.95 | ~ nonhuman(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause57,axiom, % 7.95/7.95 ( ~ nonexistent(U,V) % 7.95/7.95 | ~ existent(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause58,axiom, % 7.95/7.95 ( ~ nonliving(U,V) % 7.95/7.95 | ~ animate(U,V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause59,axiom, % 7.95/7.95 ( ~ be(U,V,W,X) % 7.95/7.95 | W = X ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause60,axiom, % 7.95/7.95 ( ~ two(U,V) % 7.95/7.95 | member(U,skf10(V,U),V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause61,axiom, % 7.95/7.95 ( ~ two(U,V) % 7.95/7.95 | member(U,skf8(V,U),V) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause62,axiom, % 7.95/7.95 ( skf10(U,V) != skf8(U,V) % 7.95/7.95 | ~ two(V,U) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause63,axiom, % 7.95/7.95 ( ~ member(U,V,W) % 7.95/7.95 | ~ two(U,W) % 7.95/7.95 | V = skf8(W,U) % 7.95/7.95 | V = skf10(W,U) ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause64,axiom, % 7.95/7.95 ( skf11(U,V,W,X) != V % 7.95/7.95 | ~ member(Y,U,Z) % 7.95/7.95 | ~ member(Y,V,Z) % 7.95/7.95 | two(Y,Z) % 7.95/7.95 | U = V ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause65,axiom, % 7.95/7.95 ( skf11(U,V,W,X) != U % 7.95/7.95 | ~ member(Y,U,Z) % 7.95/7.95 | ~ member(Y,X1,Z) % 7.95/7.95 | two(Y,Z) % 7.95/7.95 | U = X1 ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause66,axiom, % 7.95/7.95 ( ~ member(U,V,W) % 7.95/7.95 | ~ member(U,X,W) % 7.95/7.95 | two(U,W) % 7.95/7.95 | member(U,skf11(V,X,W,U),W) % 7.95/7.95 | V = X ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause67,axiom, % 7.95/7.95 ( ~ placename(U,V) % 7.95/7.95 | ~ of(U,W,X) % 7.95/7.95 | ~ placename(U,W) % 7.95/7.95 | ~ of(U,V,X) % 7.95/7.95 | ~ entity(U,X) % 7.95/7.95 | W = V ) ). % 7.95/7.95 % 7.95/7.95 cnf(clause68,negated_conjecture, % 7.95/7.95 actual_world(skc6) ). % 7.95/7.95 % 7.95/7.95 cnf(clause69,negated_conjecture, % 7.95/7.95 chevy(skc6,skc13) ). % 7.95/7.95 % 7.95/7.95 cnf(clause70,negated_conjecture, % 7.95/7.95 placename(skc6,skc12) ). % 7.95/7.95 % 7.95/7.95 cnf(clause71,negated_conjecture, % 7.95/7.95 hollywood_placename(skc6,skc12) ). % 7.95/7.95 % 7.95/7.95 cnf(clause72,negated_conjecture, % 7.95/7.95 city(skc6,skc11) ). % 7.95/7.95 % 7.95/7.95 cnf(clause73,negated_conjecture, % 7.95/7.95 street(skc6,skc11) ). % 7.95/7.95 % 7.95/7.95 cnf(clause74,negated_conjecture, % 7.95/7.95 lonely(skc6,skc11) ). % 7.95/7.95 % 7.95/7.95 cnf(clause75,negated_conjecture, % 7.95/7.95 two(skc6,skc7) ). % 7.95/7.95 % 7.95/7.95 cnf(clause76,negated_conjecture, % 7.95/7.95 group(skc6,skc7) ). % 7.95/7.95 % 7.95/7.95 cnf(clause77,negated_conjecture, % 7.95/7.95 white(skc6,skc13) ). % 7.95/7.95 % 7.95/7.95 cnf(clause78,negated_conjecture, % 7.95/7.95 dirty(skc6,skc13) ). % 7.95/7.95 % 7.95/7.95 cnf(clause79,negated_conjecture, % 7.95/7.95 old(skc6,skc13) ). % 7.95/7.95 % 7.95/7.95 cnf(clause80,negated_conjecture, % 7.95/7.95 barrel(skc6,skc10) ). % 7.95/7.95 % 7.95/7.95 cnf(clause81,negated_conjecture, % 7.95/7.95 present(skc6,skc10) ). % 7.95/7.95 % 7.95/7.95 cnf(clause82,negated_conjecture, % 7.95/7.95 event(skc6,skc10) ). % 7.95/7.96 % 7.95/7.96 cnf(clause83,negated_conjecture, % 7.95/7.96 of(skc6,skc12,skc11) ). % 7.95/7.96 % 7.95/7.96 cnf(clause84,negated_conjecture, % 7.95/7.96 down(skc6,skc10,skc11) ). % 7.95/7.96 % 7.95/7.96 cnf(clause85,negated_conjecture, % 7.95/7.96 in(skc6,skc10,skc11) ). % 7.95/7.96 % 7.95/7.96 cnf(clause86,negated_conjecture, % 7.95/7.96 agent(skc6,skc10,skc13) ). % 7.95/7.96 % 7.95/7.96 cnf(clause87,negated_conjecture, % 7.95/7.96 ( ~ member(skc6,U,skc7) % 7.95/7.96 | young(skc6,U) ) ). % 7.95/7.96 % 7.95/7.96 cnf(clause88,negated_conjecture, % 7.95/7.96 ( ~ member(skc6,U,skc7) % 7.95/7.96 | fellow(skc6,U) ) ). % 7.95/7.96 % 7.95/7.96 cnf(clause89,negated_conjecture, % 7.95/7.96 ( ~ member(skc6,U,skc7) % 7.95/7.96 | frontseat(skc6,skf5(V)) ) ). % 7.95/7.96 % 7.95/7.96 cnf(clause90,negated_conjecture, % 7.95/7.96 ( ~ member(skc6,U,skc7) % 7.95/7.96 | state(skc6,skf6(V)) ) ). % 7.95/7.96 % 7.95/7.96 cnf(clause91,negated_conjecture, % 7.95/7.96 ( ~ member(skc6,U,skc7) % 7.95/7.96 | in(skc6,skf5(V),skf5(V)) ) ). % 7.95/7.96 % 7.95/7.96 cnf(clause92,negated_conjecture, % 7.95/7.96 ( ~ member(skc6,U,skc7) % 7.95/7.96 | be(skc6,skf6(U),U,skf5(U)) ) ). % 7.95/7.96 % 7.95/7.96 %-------------------------------------------------------------------------- % 7.95/7.96 %------------------------------------------- % 7.95/7.96 % Proof found % 7.95/7.96 % SZS status Theorem for theBenchmark % 7.95/7.96 % SZS output start Proof % 7.95/7.96 %ClaNum:229(EqnAxiom:137) % 7.95/7.96 %VarNum:341(SingletonVarNum:159) % 7.95/7.96 %MaxLitNum:6 % 7.95/7.96 %MaxfuncDepth:1 % 7.95/7.96 %SharedTerms:25 % 7.95/7.96 %goalClause: 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 216 217 218 219 223 225 % 7.95/7.96 %singleGoalClaCount:19 % 7.95/7.96 [138]P1(a1) % 7.95/7.96 [139]P3(a1,a6) % 7.95/7.96 [140]P22(a1,a6) % 7.95/7.96 [141]P4(a1,a2) % 7.95/7.96 [142]P5(a1,a2) % 7.95/7.96 [143]P9(a1,a3) % 7.95/7.96 [144]P23(a1,a4) % 7.95/7.96 [145]P24(a1,a5) % 7.95/7.96 [146]P25(a1,a5) % 7.95/7.96 [147]P12(a1,a4) % 7.95/7.96 [148]P26(a1,a3) % 7.95/7.96 [149]P27(a1,a4) % 7.95/7.96 [150]P55(a1,a3) % 7.95/7.96 [151]P13(a1,a3) % 7.95/7.96 [152]P45(a1,a2) % 7.95/7.96 [153]P35(a1,a5,a4) % 7.95/7.96 [154]P14(a1,a2,a4) % 7.95/7.96 [155]P28(a1,a2,a4) % 7.95/7.96 [156]P6(a1,a2,a3) % 7.95/7.96 [157]~P36(x1571,x1572,x1572) % 7.95/7.96 [216]P16(a1,x2161)+~P36(a1,x2161,a6) % 7.95/7.96 [217]P59(a1,x2171)+~P36(a1,x2171,a6) % 7.95/7.96 [225]P11(a1,f9(x2251),x2251,f10(x2251))+~P36(a1,x2251,a6) % 7.95/7.96 [158]~P16(x1581,x1582)+P37(x1581,x1582) % 7.95/7.96 [159]~P37(x1591,x1592)+P29(x1591,x1592) % 7.95/7.96 [160]~P29(x1601,x1602)+P44(x1601,x1602) % 7.95/7.96 [161]~P44(x1611,x1612)+P15(x1611,x1612) % 7.95/7.96 [162]~P39(x1621,x1622)+P15(x1621,x1622) % 7.95/7.96 [163]~P15(x1631,x1632)+P53(x1631,x1632) % 7.95/7.96 [164]~P17(x1641,x1642)+P53(x1641,x1642) % 7.95/7.96 [165]~P2(x1651,x1652)+P53(x1651,x1652) % 7.95/7.96 [166]~P53(x1661,x1662)+P46(x1661,x1662) % 7.95/7.96 [167]~P15(x1671,x1672)+P51(x1671,x1672) % 7.95/7.96 [168]~P17(x1681,x1682)+P51(x1681,x1682) % 7.95/7.96 [169]~P15(x1691,x1692)+P18(x1691,x1692) % 7.95/7.96 [170]~P44(x1701,x1702)+P31(x1701,x1702) % 7.95/7.96 [171]~P39(x1711,x1712)+P31(x1711,x1712) % 7.95/7.96 [172]~P44(x1721,x1722)+P32(x1721,x1722) % 7.95/7.96 [173]~P29(x1731,x1732)+P30(x1731,x1732) % 7.95/7.96 [174]~P29(x1741,x1742)+P7(x1741,x1742) % 7.95/7.96 [175]~P37(x1751,x1752)+P38(x1751,x1752) % 7.95/7.96 [176]~P22(x1761,x1762)+P3(x1761,x1762) % 7.95/7.96 [177]~P3(x1771,x1772)+P47(x1771,x1772) % 7.95/7.96 [178]~P47(x1781,x1782)+P40(x1781,x1782) % 7.95/7.96 [179]~P52(x1791,x1792)+P17(x1791,x1792) % 7.95/7.96 [180]~P4(x1801,x1802)+P17(x1801,x1802) % 7.95/7.96 [181]~P17(x1811,x1812)+P41(x1811,x1812) % 7.95/7.96 [182]~P17(x1821,x1822)+P56(x1821,x1822) % 7.95/7.96 [183]~P39(x1831,x1832)+P56(x1831,x1832) % 7.95/7.96 [184]~P2(x1841,x1842)+P56(x1841,x1842) % 7.95/7.96 [185]~P52(x1851,x1852)+P4(x1851,x1852) % 7.95/7.96 [186]~P5(x1861,x1862)+P4(x1861,x1862) % 7.95/7.96 [187]~P9(x1871,x1872)+P10(x1871,x1872) % 7.95/7.96 [188]~P10(x1881,x1882)+P57(x1881,x1882) % 7.95/7.96 [189]~P57(x1891,x1892)+P54(x1891,x1892) % 7.95/7.96 [190]~P54(x1901,x1902)+P33(x1901,x1902) % 7.95/7.96 [191]~P19(x1911,x1912)+P33(x1911,x1912) % 7.95/7.96 [192]~P33(x1921,x1922)+P8(x1921,x1922) % 7.95/7.96 [193]~P58(x1931,x1932)+P8(x1931,x1932) % 7.95/7.96 [194]~P8(x1941,x1942)+P39(x1941,x1942) % 7.95/7.96 [195]~P34(x1951,x1952)+P39(x1951,x1952) % 7.95/7.96 [196]~P39(x1961,x1962)+P42(x1961,x1962) % 7.95/7.96 [197]~P23(x1971,x1972)+P58(x1971,x1972) % 7.95/7.96 [198]~P25(x1981,x1982)+P24(x1981,x1982) % 7.95/7.96 [199]~P24(x1991,x1992)+P48(x1991,x1992) % 7.95/7.96 [200]~P48(x2001,x2002)+P49(x2001,x2002) % 7.95/7.96 [201]~P49(x2011,x2012)+P2(x2011,x2012) % 7.95/7.96 [202]~P2(x2021,x2022)+P43(x2021,x2022) % 7.95/7.96 [203]~P2(x2031,x2032)+P21(x2031,x2032) % 7.95/7.96 [204]~P12(x2041,x2042)+P34(x2041,x2042) % 7.95/7.96 [205]~P20(x2051,x2052)+P50(x2051,x2052) % 7.95/7.96 [206]~P50(x2061,x2062)+P19(x2061,x2062) % 7.95/7.96 [207]~P40(x2071,x2072)+~P46(x2071,x2072) % 7.95/7.96 [208]~P21(x2081,x2082)+~P51(x2081,x2082) % 7.95/7.96 [209]~P41(x2091,x2092)+~P18(x2091,x2092) % 7.95/7.96 [210]~P42(x2101,x2102)+~P32(x2101,x2102) % 7.95/7.96 [211]~P43(x2111,x2112)+~P30(x2111,x2112) % 7.95/7.96 [212]~P42(x2121,x2122)+~P7(x2121,x2122) % 7.95/7.96 [213]~P56(x2131,x2132)+~P38(x2131,x2132) % 7.95/7.96 [214]~P59(x2141,x2142)+~P26(x2141,x2142) % 7.95/7.96 [215]~P22(x2152,x2151)+~E(f7(x2151,x2152),f8(x2151,x2152)) % 7.95/7.96 [218]~P36(a1,x2182,a6)+P52(a1,f9(x2181)) % 7.95/7.96 [219]~P36(a1,x2192,a6)+P20(a1,f10(x2191)) % 7.95/7.96 [220]~P22(x2201,x2202)+P36(x2201,f8(x2202,x2201),x2202) % 7.95/7.96 [221]~P22(x2211,x2212)+P36(x2211,f7(x2212,x2211),x2212) % 7.95/7.96 [223]P28(a1,f10(x2231),f10(x2231))+~P36(a1,x2232,a6) % 7.95/7.96 [226]E(x2261,x2262)+~P11(x2263,x2264,x2261,x2262) % 7.95/7.96 [222]~P22(x2223,x2222)+~P36(x2223,x2221,x2222)+E(x2221,f7(x2222,x2223))+E(x2221,f8(x2222,x2223)) % 7.95/7.96 [229]~P36(x2293,x2292,x2294)+~P36(x2293,x2291,x2294)+E(x2291,x2292)+P22(x2293,x2294)+P36(x2293,f11(x2291,x2292,x2294,x2293),x2294) % 7.95/7.96 [228]~P36(x2283,x2282,x2284)+~P36(x2283,x2281,x2284)+E(x2281,x2282)+P22(x2283,x2284)+~E(f11(x2281,x2282,x2285,x2286),x2282) % 7.95/7.96 [227]~P36(x2273,x2272,x2274)+~P36(x2273,x2271,x2274)+E(x2271,x2272)+P22(x2273,x2274)+~E(f11(x2271,x2275,x2276,x2277),x2271) % 7.95/7.96 [224]~P24(x2243,x2242)+~P24(x2243,x2241)+~P35(x2243,x2242,x2244)+~P35(x2243,x2241,x2244)+E(x2241,x2242)+~P15(x2243,x2244) % 7.95/7.96 %EqnAxiom % 7.95/7.96 [1]E(x11,x11) % 7.95/7.96 [2]E(x22,x21)+~E(x21,x22) % 7.95/7.96 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 7.95/7.96 [4]~E(x41,x42)+E(f7(x41,x43),f7(x42,x43)) % 7.95/7.96 [5]~E(x51,x52)+E(f7(x53,x51),f7(x53,x52)) % 7.95/7.96 [6]~E(x61,x62)+E(f8(x61,x63),f8(x62,x63)) % 7.95/7.96 [7]~E(x71,x72)+E(f8(x73,x71),f8(x73,x72)) % 7.95/7.96 [8]~E(x81,x82)+E(f9(x81),f9(x82)) % 7.95/7.96 [9]~E(x91,x92)+E(f10(x91),f10(x92)) % 7.95/7.96 [10]~E(x101,x102)+E(f11(x101,x103,x104,x105),f11(x102,x103,x104,x105)) % 7.95/7.96 [11]~E(x111,x112)+E(f11(x113,x111,x114,x115),f11(x113,x112,x114,x115)) % 7.95/7.96 [12]~E(x121,x122)+E(f11(x123,x124,x121,x125),f11(x123,x124,x122,x125)) % 7.95/7.96 [13]~E(x131,x132)+E(f11(x133,x134,x135,x131),f11(x133,x134,x135,x132)) % 7.95/7.96 [14]~P1(x141)+P1(x142)+~E(x141,x142) % 7.95/7.96 [15]P3(x152,x153)+~E(x151,x152)+~P3(x151,x153) % 7.95/7.96 [16]P3(x163,x162)+~E(x161,x162)+~P3(x163,x161) % 7.95/7.96 [17]P22(x172,x173)+~E(x171,x172)+~P22(x171,x173) % 7.95/7.96 [18]P22(x183,x182)+~E(x181,x182)+~P22(x183,x181) % 7.95/7.96 [19]P4(x192,x193)+~E(x191,x192)+~P4(x191,x193) % 7.95/7.96 [20]P4(x203,x202)+~E(x201,x202)+~P4(x203,x201) % 7.95/7.96 [21]P5(x212,x213)+~E(x211,x212)+~P5(x211,x213) % 7.95/7.96 [22]P5(x223,x222)+~E(x221,x222)+~P5(x223,x221) % 7.95/7.96 [23]P9(x232,x233)+~E(x231,x232)+~P9(x231,x233) % 7.95/7.96 [24]P9(x243,x242)+~E(x241,x242)+~P9(x243,x241) % 7.95/7.96 [25]P23(x252,x253)+~E(x251,x252)+~P23(x251,x253) % 7.95/7.96 [26]P23(x263,x262)+~E(x261,x262)+~P23(x263,x261) % 7.95/7.96 [27]P24(x272,x273)+~E(x271,x272)+~P24(x271,x273) % 7.95/7.96 [28]P24(x283,x282)+~E(x281,x282)+~P24(x283,x281) % 7.95/7.96 [29]P25(x292,x293)+~E(x291,x292)+~P25(x291,x293) % 7.95/7.96 [30]P25(x303,x302)+~E(x301,x302)+~P25(x303,x301) % 7.95/7.96 [31]P12(x312,x313)+~E(x311,x312)+~P12(x311,x313) % 7.95/7.96 [32]P12(x323,x322)+~E(x321,x322)+~P12(x323,x321) % 7.95/7.96 [33]P26(x332,x333)+~E(x331,x332)+~P26(x331,x333) % 7.95/7.96 [34]P26(x343,x342)+~E(x341,x342)+~P26(x343,x341) % 7.95/7.96 [35]P27(x352,x353)+~E(x351,x352)+~P27(x351,x353) % 7.95/7.96 [36]P27(x363,x362)+~E(x361,x362)+~P27(x363,x361) % 7.95/7.96 [37]P55(x372,x373)+~E(x371,x372)+~P55(x371,x373) % 7.95/7.96 [38]P55(x383,x382)+~E(x381,x382)+~P55(x383,x381) % 7.95/7.96 [39]P13(x392,x393)+~E(x391,x392)+~P13(x391,x393) % 7.95/7.96 [40]P13(x403,x402)+~E(x401,x402)+~P13(x403,x401) % 7.95/7.96 [41]P45(x412,x413)+~E(x411,x412)+~P45(x411,x413) % 7.95/7.96 [42]P45(x423,x422)+~E(x421,x422)+~P45(x423,x421) % 7.95/7.96 [43]P35(x432,x433,x434)+~E(x431,x432)+~P35(x431,x433,x434) % 7.95/7.96 [44]P35(x443,x442,x444)+~E(x441,x442)+~P35(x443,x441,x444) % 7.95/7.96 [45]P35(x453,x454,x452)+~E(x451,x452)+~P35(x453,x454,x451) % 7.95/7.96 [46]P14(x462,x463,x464)+~E(x461,x462)+~P14(x461,x463,x464) % 7.95/7.96 [47]P14(x473,x472,x474)+~E(x471,x472)+~P14(x473,x471,x474) % 7.95/7.96 [48]P14(x483,x484,x482)+~E(x481,x482)+~P14(x483,x484,x481) % 7.95/7.96 [49]P28(x492,x493,x494)+~E(x491,x492)+~P28(x491,x493,x494) % 7.95/7.96 [50]P28(x503,x502,x504)+~E(x501,x502)+~P28(x503,x501,x504) % 7.95/7.96 [51]P28(x513,x514,x512)+~E(x511,x512)+~P28(x513,x514,x511) % 7.95/7.96 [52]P6(x522,x523,x524)+~E(x521,x522)+~P6(x521,x523,x524) % 7.95/7.96 [53]P6(x533,x532,x534)+~E(x531,x532)+~P6(x533,x531,x534) % 7.95/7.96 [54]P6(x543,x544,x542)+~E(x541,x542)+~P6(x543,x544,x541) % 7.95/7.96 [55]P36(x552,x553,x554)+~E(x551,x552)+~P36(x551,x553,x554) % 7.95/7.96 [56]P36(x563,x562,x564)+~E(x561,x562)+~P36(x563,x561,x564) % 7.95/7.96 [57]P36(x573,x574,x572)+~E(x571,x572)+~P36(x573,x574,x571) % 7.95/7.96 [58]P37(x582,x583)+~E(x581,x582)+~P37(x581,x583) % 7.95/7.96 [59]P37(x593,x592)+~E(x591,x592)+~P37(x593,x591) % 7.95/7.96 [60]P16(x602,x603)+~E(x601,x602)+~P16(x601,x603) % 7.95/7.96 [61]P16(x613,x612)+~E(x611,x612)+~P16(x613,x611) % 7.95/7.96 [62]P29(x622,x623)+~E(x621,x622)+~P29(x621,x623) % 7.95/7.96 [63]P29(x633,x632)+~E(x631,x632)+~P29(x633,x631) % 7.95/7.96 [64]P30(x642,x643)+~E(x641,x642)+~P30(x641,x643) % 7.95/7.96 [65]P30(x653,x652)+~E(x651,x652)+~P30(x653,x651) % 7.95/7.96 [66]P44(x662,x663)+~E(x661,x662)+~P44(x661,x663) % 7.95/7.96 [67]P44(x673,x672)+~E(x671,x672)+~P44(x673,x671) % 7.95/7.96 [68]P41(x682,x683)+~E(x681,x682)+~P41(x681,x683) % 7.95/7.96 [69]P41(x693,x692)+~E(x691,x692)+~P41(x693,x691) % 7.95/7.96 [70]P15(x702,x703)+~E(x701,x702)+~P15(x701,x703) % 7.95/7.96 [71]P15(x713,x712)+~E(x711,x712)+~P15(x713,x711) % 7.95/7.96 [72]P40(x722,x723)+~E(x721,x722)+~P40(x721,x723) % 7.95/7.96 [73]P40(x733,x732)+~E(x731,x732)+~P40(x733,x731) % 7.95/7.96 [74]P20(x742,x743)+~E(x741,x742)+~P20(x741,x743) % 7.95/7.96 [75]P20(x753,x752)+~E(x751,x752)+~P20(x753,x751) % 7.95/7.96 [76]P39(x762,x763)+~E(x761,x762)+~P39(x761,x763) % 7.95/7.96 [77]P39(x773,x772)+~E(x771,x772)+~P39(x773,x771) % 7.95/7.96 [78]P53(x782,x783)+~E(x781,x782)+~P53(x781,x783) % 7.95/7.96 [79]P53(x793,x792)+~E(x791,x792)+~P53(x793,x791) % 7.95/7.96 [80]P50(x802,x803)+~E(x801,x802)+~P50(x801,x803) % 7.95/7.96 [81]P50(x813,x812)+~E(x811,x812)+~P50(x813,x811) % 7.95/7.96 [82]P7(x822,x823)+~E(x821,x822)+~P7(x821,x823) % 7.95/7.96 [83]P7(x833,x832)+~E(x831,x832)+~P7(x833,x831) % 7.95/7.96 [84]P17(x842,x843)+~E(x841,x842)+~P17(x841,x843) % 7.95/7.96 [85]P17(x853,x852)+~E(x851,x852)+~P17(x853,x851) % 7.95/7.96 [86]P48(x862,x863)+~E(x861,x862)+~P48(x861,x863) % 7.95/7.96 [87]P48(x873,x872)+~E(x871,x872)+~P48(x873,x871) % 7.95/7.96 [88]P2(x882,x883)+~E(x881,x882)+~P2(x881,x883) % 7.95/7.96 [89]P2(x893,x892)+~E(x891,x892)+~P2(x893,x891) % 7.95/7.96 [90]P46(x902,x903)+~E(x901,x902)+~P46(x901,x903) % 7.95/7.96 [91]P46(x913,x912)+~E(x911,x912)+~P46(x913,x911) % 7.95/7.96 [92]P42(x922,x923)+~E(x921,x922)+~P42(x921,x923) % 7.95/7.96 [93]P42(x933,x932)+~E(x931,x932)+~P42(x933,x931) % 7.95/7.96 [94]P51(x942,x943)+~E(x941,x942)+~P51(x941,x943) % 7.95/7.96 [95]P51(x953,x952)+~E(x951,x952)+~P51(x953,x951) % 7.95/7.96 [96]P43(x962,x963)+~E(x961,x962)+~P43(x961,x963) % 7.95/7.96 [97]P43(x973,x972)+~E(x971,x972)+~P43(x973,x971) % 7.95/7.96 [98]P54(x982,x983)+~E(x981,x982)+~P54(x981,x983) % 7.95/7.96 [99]P54(x993,x992)+~E(x991,x992)+~P54(x993,x991) % 7.95/7.96 [100]P58(x1002,x1003)+~E(x1001,x1002)+~P58(x1001,x1003) % 7.95/7.96 [101]P58(x1013,x1012)+~E(x1011,x1012)+~P58(x1013,x1011) % 7.95/7.96 [102]P18(x1022,x1023)+~E(x1021,x1022)+~P18(x1021,x1023) % 7.95/7.96 [103]P18(x1033,x1032)+~E(x1031,x1032)+~P18(x1033,x1031) % 7.95/7.96 [104]P34(x1042,x1043)+~E(x1041,x1042)+~P34(x1041,x1043) % 7.95/7.96 [105]P34(x1053,x1052)+~E(x1051,x1052)+~P34(x1053,x1051) % 7.95/7.96 [106]P31(x1062,x1063)+~E(x1061,x1062)+~P31(x1061,x1063) % 7.95/7.96 [107]P31(x1073,x1072)+~E(x1071,x1072)+~P31(x1073,x1071) % 7.95/7.96 [108]P8(x1082,x1083)+~E(x1081,x1082)+~P8(x1081,x1083) % 7.95/7.96 [109]P8(x1093,x1092)+~E(x1091,x1092)+~P8(x1093,x1091) % 7.95/7.96 [110]P10(x1102,x1103)+~E(x1101,x1102)+~P10(x1101,x1103) % 7.95/7.96 [111]P10(x1113,x1112)+~E(x1111,x1112)+~P10(x1113,x1111) % 7.95/7.96 [112]P57(x1122,x1123)+~E(x1121,x1122)+~P57(x1121,x1123) % 7.95/7.96 [113]P57(x1133,x1132)+~E(x1131,x1132)+~P57(x1133,x1131) % 7.95/7.96 [114]P32(x1142,x1143)+~E(x1141,x1142)+~P32(x1141,x1143) % 7.95/7.96 [115]P32(x1153,x1152)+~E(x1151,x1152)+~P32(x1153,x1151) % 7.95/7.96 [116]P38(x1162,x1163)+~E(x1161,x1162)+~P38(x1161,x1163) % 7.95/7.96 [117]P38(x1173,x1172)+~E(x1171,x1172)+~P38(x1173,x1171) % 7.95/7.96 [118]P33(x1182,x1183)+~E(x1181,x1182)+~P33(x1181,x1183) % 7.95/7.96 [119]P33(x1193,x1192)+~E(x1191,x1192)+~P33(x1193,x1191) % 7.95/7.96 [120]P49(x1202,x1203)+~E(x1201,x1202)+~P49(x1201,x1203) % 7.95/7.96 [121]P49(x1213,x1212)+~E(x1211,x1212)+~P49(x1213,x1211) % 7.95/7.96 [122]P52(x1222,x1223)+~E(x1221,x1222)+~P52(x1221,x1223) % 7.95/7.96 [123]P52(x1233,x1232)+~E(x1231,x1232)+~P52(x1233,x1231) % 7.95/7.96 [124]P21(x1242,x1243)+~E(x1241,x1242)+~P21(x1241,x1243) % 7.95/7.96 [125]P21(x1253,x1252)+~E(x1251,x1252)+~P21(x1253,x1251) % 7.95/7.96 [126]P56(x1262,x1263)+~E(x1261,x1262)+~P56(x1261,x1263) % 7.95/7.96 [127]P56(x1273,x1272)+~E(x1271,x1272)+~P56(x1273,x1271) % 7.95/7.96 [128]P19(x1282,x1283)+~E(x1281,x1282)+~P19(x1281,x1283) % 7.95/7.96 [129]P19(x1293,x1292)+~E(x1291,x1292)+~P19(x1293,x1291) % 7.95/7.96 [130]P59(x1302,x1303)+~E(x1301,x1302)+~P59(x1301,x1303) % 7.95/7.96 [131]P59(x1313,x1312)+~E(x1311,x1312)+~P59(x1313,x1311) % 7.95/7.96 [132]P11(x1322,x1323,x1324,x1325)+~E(x1321,x1322)+~P11(x1321,x1323,x1324,x1325) % 7.95/7.96 [133]P11(x1333,x1332,x1334,x1335)+~E(x1331,x1332)+~P11(x1333,x1331,x1334,x1335) % 7.95/7.96 [134]P11(x1343,x1344,x1342,x1345)+~E(x1341,x1342)+~P11(x1343,x1344,x1341,x1345) % 7.95/7.96 [135]P11(x1353,x1354,x1355,x1352)+~E(x1351,x1352)+~P11(x1353,x1354,x1355,x1351) % 7.95/7.96 [136]P47(x1362,x1363)+~E(x1361,x1362)+~P47(x1361,x1363) % 7.95/7.96 [137]P47(x1373,x1372)+~E(x1371,x1372)+~P47(x1373,x1371) % 7.95/7.96 % 7.95/7.96 %------------------------------------------- % 7.95/7.96 cnf(230,plain, % 7.95/7.96 (~P59(a1,a3)), % 7.95/7.96 inference(scs_inference,[],[148,214])). % 7.95/7.96 cnf(324,plain, % 7.95/7.96 (P29(x3241,x3242)+~P16(x3241,x3242)), % 7.95/7.96 inference(scs_inference,[],[158,159])). % 7.95/7.96 cnf(325,plain, % 7.95/7.96 (P15(x3251,x3252)+~P29(x3251,x3252)), % 7.95/7.96 inference(scs_inference,[],[160,161])). % 7.95/7.96 cnf(337,plain, % 7.95/7.96 (~P29(x3371,x3372)+~P43(x3371,x3372)), % 7.95/7.96 inference(scs_inference,[],[173,211])). % 7.95/7.96 cnf(338,plain, % 7.95/7.96 (~P29(x3381,x3382)+~P42(x3381,x3382)), % 7.95/7.96 inference(scs_inference,[],[174,212])). % 7.95/7.96 cnf(339,plain, % 7.95/7.96 (~P37(x3391,x3392)+~P56(x3391,x3392)), % 7.95/7.96 inference(scs_inference,[],[175,213])). % 7.95/7.96 cnf(340,plain, % 7.95/7.96 (P47(a1,a6)), % 7.95/7.96 inference(scs_inference,[],[140,176,177])). % 7.95/7.96 cnf(345,plain, % 7.95/7.96 (~P46(a1,a6)), % 7.95/7.96 inference(scs_inference,[],[340,178,207])). % 7.95/7.96 cnf(362,plain, % 7.95/7.96 (~P44(a1,a6)), % 7.95/7.96 inference(scs_inference,[],[345,166,163,164,165,201,179,180,186,161])). % 7.95/7.96 cnf(366,plain, % 7.95/7.96 (~P8(a1,a6)), % 7.95/7.96 inference(scs_inference,[],[345,166,163,164,165,201,179,180,186,161,162,194])). % 7.95/7.96 cnf(368,plain, % 7.95/7.96 (~P34(a1,a6)), % 7.95/7.96 inference(scs_inference,[],[345,166,163,164,165,201,179,180,186,161,162,194,195])). % 7.95/7.96 cnf(370,plain, % 7.95/7.96 (~P48(a1,a6)), % 7.95/7.96 inference(scs_inference,[],[345,166,163,164,165,201,179,180,186,161,162,194,195,200])). % 7.95/7.96 cnf(372,plain, % 7.95/7.96 (~E(a2,a6)), % 7.95/7.96 inference(scs_inference,[],[142,345,166,163,164,165,201,179,180,186,161,162,194,195,200,22])). % 7.95/7.96 cnf(400,plain, % 7.95/7.96 (~P16(a1,a6)), % 7.95/7.96 inference(scs_inference,[],[145,147,372,362,366,368,370,199,204,226,160,192,193,28,32,197,198,159,190,191,206,158])). % 7.95/7.96 cnf(407,plain, % 7.95/7.96 (~P17(x4071,x4072)+~P37(x4071,x4072)), % 7.95/7.96 inference(scs_inference,[],[182,339])). % 7.95/7.96 cnf(452,plain, % 7.95/7.96 (~P2(x4521,x4522)+~P37(x4521,x4522)), % 7.95/7.96 inference(scs_inference,[],[184,339])). % 7.95/7.96 cnf(501,plain, % 7.95/7.96 (~P2(x5011,x5012)+~P29(x5011,x5012)), % 7.95/7.96 inference(scs_inference,[],[202,337])). % 7.95/7.96 cnf(634,plain, % 7.95/7.96 (~P29(x6341,x6342)+~P39(x6341,x6342)), % 7.95/7.96 inference(scs_inference,[],[338,196])). % 7.95/7.96 cnf(666,plain, % 7.95/7.96 (~P17(x6661,x6662)+~P16(x6661,x6662)), % 7.95/7.96 inference(scs_inference,[],[407,158])). % 7.95/7.96 cnf(698,plain, % 7.95/7.96 (~P2(x6981,x6982)+~P16(x6981,x6982)), % 7.95/7.96 inference(scs_inference,[],[452,158])). % 7.95/7.96 cnf(731,plain, % 7.95/7.96 (~P29(x7311,x7312)+~P2(x7311,x7313)+~E(x7312,x7313)), % 7.95/7.96 inference(scs_inference,[],[501,63])). % 7.95/7.96 cnf(780,plain, % 7.95/7.96 (~P29(x7801,x7802)+~P34(x7801,x7802)), % 7.95/7.96 inference(scs_inference,[],[634,195])). % 7.95/7.96 cnf(812,plain, % 7.95/7.96 (~P17(a1,x8121)+~P36(a1,x8121,a6)), % 7.95/7.96 inference(scs_inference,[],[666,216])). % 7.95/7.96 cnf(844,plain, % 7.95/7.96 (~P2(a1,x8441)+~P36(a1,x8441,a6)), % 7.95/7.96 inference(scs_inference,[],[698,216])). % 7.95/7.96 cnf(892,plain, % 7.95/7.96 (~P29(a1,a4)), % 7.95/7.96 inference(scs_inference,[],[147,780,204])). % 7.95/7.96 cnf(895,plain, % 7.95/7.96 (~P16(a1,a4)), % 7.95/7.96 inference(scs_inference,[],[892,159,158])). % 7.95/7.96 cnf(1078,plain, % 7.95/7.96 (~P36(a1,a2,a6)), % 7.95/7.96 inference(scs_inference,[],[141,812,180])). % 7.95/7.96 cnf(1094,plain, % 7.95/7.96 (~P49(a1,x10941)+~P36(a1,x10941,a6)), % 7.95/7.96 inference(scs_inference,[],[844,201])). % 7.95/7.96 cnf(1110,plain, % 7.95/7.96 (~P48(a1,x11101)+~P36(a1,x11101,a6)), % 7.95/7.96 inference(scs_inference,[],[1094,200])). % 7.95/7.96 cnf(1176,plain, % 7.95/7.96 (P52(a1,f9(x11761))), % 7.95/7.96 inference(scs_inference,[],[140,218,220])). % 7.95/7.96 cnf(1201,plain, % 7.95/7.96 (P20(a1,f10(x12011))), % 7.95/7.96 inference(scs_inference,[],[140,219,221])). % 7.95/7.96 cnf(1290,plain, % 7.95/7.96 (E(x12901,f10(x12901))+~P36(a1,x12901,a6)), % 7.95/7.96 inference(scs_inference,[],[225,226])). % 7.95/7.96 cnf(1423,plain, % 7.95/7.96 (~E(x14231,a6)+~P36(a1,x14231,a6)), % 7.95/7.96 inference(scs_inference,[],[400,61,216])). % 7.95/7.97 cnf(1457,plain, % 7.95/7.97 (P30(x14571,x14572)+~P29(x14571,x14573)+~E(x14573,x14572)), % 7.95/7.97 inference(scs_inference,[],[65,173])). % 7.95/7.97 cnf(1679,plain, % 7.95/7.97 (P7(x16791,x16792)+~P29(x16791,x16793)+~E(x16793,x16792)), % 7.95/7.97 inference(scs_inference,[],[83,174])). % 7.95/7.97 cnf(1813,plain, % 7.95/7.97 (P42(x18131,x18132)+~P39(x18131,x18133)+~E(x18133,x18132)), % 7.95/7.97 inference(scs_inference,[],[93,196])). % 7.95/7.97 cnf(1982,plain, % 7.95/7.97 (P18(x19821,x19822)+~P15(x19821,x19823)+~E(x19823,x19822)), % 7.95/7.97 inference(scs_inference,[],[103,169])). % 7.95/7.97 cnf(2371,plain, % 7.95/7.97 (~P59(x23711,x23712)+~E(x23711,a1)+~E(x23712,a3)), % 7.95/7.97 inference(scs_inference,[],[230,130,131])). % 7.95/7.97 cnf(2493,plain, % 7.95/7.97 (~E(x24931,a3)+~P36(a1,x24931,a6)), % 7.95/7.97 inference(scs_inference,[],[2371,217])). % 7.95/7.97 cnf(2540,plain, % 7.95/7.97 (P36(x25401,f8(a6,a1),a6)+~E(a1,x25401)), % 7.95/7.97 inference(scs_inference,[],[140,55,220])). % 7.95/7.97 cnf(2541,plain, % 7.95/7.97 (P36(a1,f8(a6,a1),a6)), % 7.95/7.97 inference(equality_inference,[],[2540])). % 7.95/7.97 cnf(2542,plain, % 7.95/7.97 (P28(a1,f10(x25421),f10(x25421))), % 7.95/7.97 inference(scs_inference,[],[2541,223])). % 7.95/7.97 cnf(2560,plain, % 7.95/7.97 (~E(f8(a6,a1),a3)), % 7.95/7.97 inference(scs_inference,[],[2541,216,217,812,844,1094,1110,1290,1423,2493])). % 7.95/7.97 cnf(2564,plain, % 7.95/7.97 (E(f10(f8(a6,a1)),f8(a6,a1))), % 7.95/7.97 inference(scs_inference,[],[2541,216,217,812,844,1094,1110,1290,1423,2493,324,2])). % 7.95/7.97 cnf(2569,plain, % 7.95/7.97 (~P52(a1,f8(a6,a1))), % 7.95/7.97 inference(scs_inference,[],[2541,216,217,812,844,1094,1110,1290,1423,2493,324,2,325,199,179])). % 7.95/7.97 cnf(2577,plain, % 7.95/7.97 (~E(a6,f8(a6,a1))), % 7.95/7.97 inference(scs_inference,[],[2541,157,216,217,812,844,1094,1110,1290,1423,2493,324,2,325,199,179,180,198,226,57])). % 7.95/7.97 cnf(2589,plain, % 7.95/7.97 (P30(a1,f8(a6,a1))), % 7.95/7.97 inference(scs_inference,[],[895,2541,157,216,217,812,844,1094,1110,1290,1423,2493,324,2,325,199,179,180,198,226,57,61,731,1457,1679,1982,3,65])). % 7.95/7.97 cnf(2590,plain, % 7.95/7.97 (P7(a1,f8(a6,a1))), % 7.95/7.97 inference(scs_inference,[],[895,2541,157,216,217,812,844,1094,1110,1290,1423,2493,324,2,325,199,179,180,198,226,57,61,731,1457,1679,1982,3,65,83])). % 7.95/7.97 cnf(2591,plain, % 7.95/7.97 (P18(a1,f8(a6,a1))), % 7.95/7.97 inference(scs_inference,[],[895,2541,157,216,217,812,844,1094,1110,1290,1423,2493,324,2,325,199,179,180,198,226,57,61,731,1457,1679,1982,3,65,83,103])). % 7.95/7.97 cnf(2602,plain, % 7.95/7.97 (~P48(a1,f10(f8(a6,a1)))), % 7.95/7.97 inference(scs_inference,[],[895,2541,157,216,217,812,844,1094,1110,1290,1423,2493,324,2,325,199,179,180,198,226,57,61,731,1457,1679,1982,3,65,83,103,209,211,212,186,201,200])). % 7.95/7.97 cnf(2607,plain, % 7.95/7.97 (~P17(a1,f10(f8(a6,a1)))), % 7.95/7.97 inference(scs_inference,[],[895,2541,157,216,217,812,844,1094,1110,1290,1423,2493,324,2,325,199,179,180,198,226,57,61,731,1457,1679,1982,3,65,83,103,209,211,212,186,201,200,14,1813,181])). % 7.95/7.97 cnf(2609,plain, % 7.95/7.97 (~P39(a1,f10(f8(a6,a1)))), % 7.95/7.97 inference(scs_inference,[],[895,2541,157,216,217,812,844,1094,1110,1290,1423,2493,324,2,325,199,179,180,198,226,57,61,731,1457,1679,1982,3,65,83,103,209,211,212,186,201,200,14,1813,181,196])). % 7.95/7.97 cnf(2611,plain, % 7.95/7.97 (~P8(a1,f8(a6,a1))), % 7.95/7.97 inference(scs_inference,[],[895,2541,157,216,217,812,844,1094,1110,1290,1423,2493,324,2,325,199,179,180,198,226,57,61,731,1457,1679,1982,3,65,83,103,209,211,212,186,201,200,14,1813,181,196,194])). % 7.95/7.97 cnf(2615,plain, % 7.95/7.97 (~P34(a1,f8(a6,a1))), % 7.95/7.97 inference(scs_inference,[],[895,2541,157,216,217,812,844,1094,1110,1290,1423,2493,324,2,325,199,179,180,198,226,57,61,731,1457,1679,1982,3,65,83,103,209,211,212,186,201,200,14,1813,181,196,194,193,195])). % 7.95/7.97 cnf(2666,plain, % 7.95/7.97 (~P8(a1,f10(f8(a6,a1)))), % 7.95/7.97 inference(scs_inference,[],[2589,2591,2609,2611,2615,204,211,209,192,194])). % 7.95/7.97 cnf(2676,plain, % 7.95/7.97 (~P34(a1,f10(f8(a6,a1)))), % 7.95/7.97 inference(scs_inference,[],[2589,2590,2591,2602,2609,2611,2615,204,211,209,192,194,191,212,190,199,195])). % 7.95/7.97 cnf(2680,plain, % 7.95/7.97 (~P52(a1,f10(f8(a6,a1)))), % 7.95/7.97 inference(scs_inference,[],[2589,2590,2591,2602,2607,2609,2611,2615,204,211,209,192,194,191,212,190,199,195,193,179])). % 7.95/7.97 cnf(2689,plain, % 7.95/7.97 (P28(a1,f10(x26891),f10(x26891))), % 7.95/7.97 inference(rename_variables,[],[2542])). % 7.95/7.97 cnf(2690,plain, % 7.95/7.97 (P28(a1,f8(a6,a1),f10(f8(a6,a1)))), % 7.95/7.97 inference(scs_inference,[],[2542,2689,2560,2564,2589,2590,2591,2602,2607,2609,2611,2615,204,211,209,192,194,191,212,190,199,195,193,179,180,198,226,51,50])). % 7.95/7.97 cnf(2693,plain, % 7.95/7.97 (~P50(a1,f8(a6,a1))), % 7.95/7.97 inference(scs_inference,[],[1176,2542,2689,2560,2569,2564,2589,2590,2591,2602,2607,2609,2611,2615,204,211,209,192,194,191,212,190,199,195,193,179,180,198,226,51,50,123,206])). % 7.95/7.97 cnf(2695,plain, % 7.95/7.97 (~P57(a1,f8(a6,a1))), % 7.95/7.97 inference(scs_inference,[],[1176,2542,2689,2560,2569,2564,2589,2590,2591,2602,2607,2609,2611,2615,204,211,209,192,194,191,212,190,199,195,193,179,180,198,226,51,50,123,206,189])). % 7.95/7.97 cnf(2744,plain, % 7.95/7.97 (~P50(a1,f10(f8(a6,a1)))), % 7.95/7.97 inference(scs_inference,[],[1176,1078,2541,2577,2680,2690,2564,2666,2676,2693,2695,188,187,205,204,192,191,190,226,56,51,123,206])). % 7.95/7.97 cnf(2758,plain, % 7.95/7.97 ($false), % 7.95/7.97 inference(scs_inference,[],[1201,2744,205]), % 7.95/7.97 ['proof']). % 7.95/7.97 % SZS output end Proof % 7.95/7.97 % Total time :7.280000s %------------------------------------------------------------------------------