%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN036-3 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n027.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 19:04:17 EDT 2024 % Result : Unsatisfiable 1.41s 1.48s % Output : CNFRefutation 1.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN036-3 : TPTP v8.2.0. Released v1.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n027.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Sun Jun 23 19:06:23 EDT 2024 % 0.11/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 1.40/1.47 %------------------------------------------- % 1.40/1.47 % File :CSE---1.7 % 1.40/1.47 % Problem :theBenchmark % 1.40/1.47 % Transform :cnf % 1.40/1.47 % Format :tptp:raw % 1.40/1.47 % Command :java -jar mcs_scs.jar %d %s % 1.40/1.47 % 1.40/1.47 % Result :Theorem 0.870000s % 1.40/1.47 % Output :CNFRefutation 0.870000s % 1.40/1.47 %------------------------------------------- % 1.41/1.47 %-------------------------------------------------------------------------- % 1.41/1.47 % File : SYN036-3 : TPTP v8.2.0. Released v1.0.0. % 1.41/1.47 % Domain : Syntactic % 1.41/1.47 % Problem : Andrews Challenge Problem % 1.41/1.47 % Version : Especial. % 1.41/1.47 % Theorem formulation : Different clausal form. % 1.41/1.47 % English : % 1.41/1.47 % 1.41/1.47 % Refs : [DeC79] DeChampeaux (1979), Sub-problem Finder and Instance Ch % 1.41/1.47 % : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au % 1.41/1.47 % : [AZ89] Angshuman & Zhang (1989), Andrews' Challenge Problem: % 1.41/1.47 % Source : [AZ89] % 1.41/1.47 % Names : Problem 9 [AZ89] % 1.41/1.47 % 1.41/1.47 % Status : Unsatisfiable % 1.41/1.47 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.1.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v5.1.0, 0.09 v5.0.0, 0.07 v4.1.0, 0.00 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v3.2.0, 0.00 v3.1.0, 0.17 v2.7.0, 0.25 v2.6.0, 0.00 v2.5.0, 0.20 v2.4.0, 0.00 v2.1.0, 0.00 v2.0.0 % 1.41/1.47 % Syntax : Number of clauses : 36 ( 0 unt; 11 nHn; 30 RR) % 1.41/1.47 % Number of literals : 104 ( 0 equ; 52 neg) % 1.41/1.47 % Maximal clause size : 4 ( 2 avg) % 1.41/1.47 % Maximal term depth : 2 ( 1 avg) % 1.41/1.47 % Number of predicates : 12 ( 12 usr; 8 prp; 0-1 aty) % 1.41/1.47 % Number of functors : 8 ( 8 usr; 6 con; 0-1 aty) % 1.41/1.47 % Number of variables : 18 ( 10 sgn) % 1.41/1.47 % SPC : CNF_UNS_RFO_NEQ_NHN % 1.41/1.47 % 1.41/1.47 % Comments : % 1.41/1.47 %-------------------------------------------------------------------------- % 1.41/1.47 cnf(clause_1,negated_conjecture, % 1.41/1.47 ( ~ n2 % 1.41/1.47 | ~ n9 % 1.41/1.47 | ~ n6 % 1.41/1.47 | ~ n10 ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_2,negated_conjecture, % 1.41/1.47 ( ~ n2 % 1.41/1.47 | ~ n9 % 1.41/1.47 | n6 % 1.41/1.47 | n10 ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_3,negated_conjecture, % 1.41/1.47 ( n2 % 1.41/1.47 | n9 % 1.41/1.47 | ~ n6 % 1.41/1.47 | ~ n10 ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_4,negated_conjecture, % 1.41/1.47 ( n2 % 1.41/1.47 | n9 % 1.41/1.47 | n6 % 1.41/1.47 | n10 ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_5,negated_conjecture, % 1.41/1.47 ( ~ n2 % 1.41/1.47 | n9 % 1.41/1.47 | ~ n6 % 1.41/1.47 | n10 ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_6,negated_conjecture, % 1.41/1.47 ( ~ n2 % 1.41/1.47 | n9 % 1.41/1.47 | n6 % 1.41/1.47 | ~ n10 ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_7,negated_conjecture, % 1.41/1.47 ( n2 % 1.41/1.47 | ~ n9 % 1.41/1.47 | ~ n6 % 1.41/1.47 | n10 ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_8,negated_conjecture, % 1.41/1.47 ( n2 % 1.41/1.47 | ~ n9 % 1.41/1.47 | n6 % 1.41/1.47 | ~ n10 ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_9,negated_conjecture, % 1.41/1.47 ( ~ p(s8) % 1.41/1.47 | n8 ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_10,negated_conjecture, % 1.41/1.47 ( ~ n8 % 1.41/1.47 | p(X8) ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_11,negated_conjecture, % 1.41/1.47 ( ~ p(X7) % 1.41/1.47 | n7 ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_12,negated_conjecture, % 1.41/1.47 ( ~ n7 % 1.41/1.47 | p(s7) ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_13,negated_conjecture, % 1.41/1.47 ( ~ n5(X6) % 1.41/1.47 | n6 ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_14,negated_conjecture, % 1.41/1.47 ( ~ n6 % 1.41/1.47 | n5(s6) ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_15,negated_conjecture, % 1.41/1.47 ( ~ q(X) % 1.41/1.47 | ~ q(s5(X)) % 1.41/1.47 | n5(X) ) ). % 1.41/1.47 % 1.41/1.47 cnf(clause_16,negated_conjecture, % 1.41/1.47 ( q(X) % 1.41/1.47 | q(s5(X)) % 1.41/1.48 | n5(X) ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_17,negated_conjecture, % 1.41/1.48 ( ~ n5(X) % 1.41/1.48 | ~ q(X) % 1.41/1.48 | q(X5) ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_18,negated_conjecture, % 1.41/1.48 ( ~ n5(X) % 1.41/1.48 | q(X) % 1.41/1.48 | ~ q(X5) ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_19,negated_conjecture, % 1.41/1.48 ( ~ q(s4) % 1.41/1.48 | n4 ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_20,negated_conjecture, % 1.41/1.48 ( ~ n4 % 1.41/1.48 | q(X4) ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_21,negated_conjecture, % 1.41/1.48 ( ~ q(X3) % 1.41/1.48 | n3 ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_22,negated_conjecture, % 1.41/1.48 ( ~ n3 % 1.41/1.48 | q(s3) ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_23,negated_conjecture, % 1.41/1.48 ( ~ n1(X2) % 1.41/1.48 | n2 ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_24,negated_conjecture, % 1.41/1.48 ( ~ n2 % 1.41/1.48 | n1(s2) ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_25,negated_conjecture, % 1.41/1.48 ( ~ p(X) % 1.41/1.48 | ~ p(s1(X)) % 1.41/1.48 | n1(X) ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_26,negated_conjecture, % 1.41/1.48 ( p(X) % 1.41/1.48 | p(s1(X)) % 1.41/1.48 | n1(X) ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_27,negated_conjecture, % 1.41/1.48 ( ~ n1(X) % 1.41/1.48 | ~ p(X) % 1.41/1.48 | p(X1) ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_28,negated_conjecture, % 1.41/1.48 ( ~ n1(X) % 1.41/1.48 | p(X) % 1.41/1.48 | ~ p(X1) ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_29,negated_conjecture, % 1.41/1.48 ( ~ n3 % 1.41/1.48 | ~ n4 % 1.41/1.48 | n9 ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_30,negated_conjecture, % 1.41/1.48 ( n3 % 1.41/1.48 | n4 % 1.41/1.48 | n9 ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_31,negated_conjecture, % 1.41/1.48 ( ~ n3 % 1.41/1.48 | n4 % 1.41/1.48 | ~ n9 ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_32,negated_conjecture, % 1.41/1.48 ( n3 % 1.41/1.48 | ~ n4 % 1.41/1.48 | ~ n9 ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_33,negated_conjecture, % 1.41/1.48 ( ~ n7 % 1.41/1.48 | ~ n8 % 1.41/1.48 | n10 ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_34,negated_conjecture, % 1.41/1.48 ( n7 % 1.41/1.48 | n8 % 1.41/1.48 | n10 ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_35,negated_conjecture, % 1.41/1.48 ( ~ n7 % 1.41/1.48 | n8 % 1.41/1.48 | ~ n10 ) ). % 1.41/1.48 % 1.41/1.48 cnf(clause_36,negated_conjecture, % 1.41/1.48 ( n7 % 1.41/1.48 | ~ n8 % 1.41/1.48 | ~ n10 ) ). % 1.41/1.48 % 1.41/1.48 %-------------------------------------------------------------------------- % 1.41/1.48 %------------------------------------------- % 1.41/1.48 % Proof found % 1.41/1.48 % SZS status Theorem for theBenchmark % 1.41/1.48 % SZS output start Proof % 1.41/1.48 %ClaNum:36(EqnAxiom:0) % 1.41/1.48 %VarNum:30(SingletonVarNum:18) % 1.41/1.48 %MaxLitNum:4 % 1.41/1.48 %MaxfuncDepth:1 % 1.41/1.48 %SharedTerms:29 % 1.41/1.48 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 % 1.41/1.48 [16]P11(a1)+~P8(a5000) % 1.41/1.48 [17]P10(a2)+~P9(a5000) % 1.41/1.48 [18]P12(a3)+~P3(a5000) % 1.41/1.48 [19]P5(a4)+~P6(a5000) % 1.41/1.48 [21]P7(a5000)+~P11(a8) % 1.41/1.48 [22]P2(a5000)+~P12(a6) % 1.41/1.48 [23]P11(x231)+~P7(a5000) % 1.41/1.48 [24]P12(x241)+~P2(a5000) % 1.41/1.48 [25]~P5(x251)+P6(a5000) % 1.41/1.48 [26]~P10(x261)+P9(a5000) % 1.41/1.48 [27]~P11(x271)+P8(a5000) % 1.41/1.48 [28]~P12(x281)+P3(a5000) % 1.41/1.48 [1]P1(a5000)+P2(a5000)+P3(a5000) % 1.41/1.48 [2]P4(a5000)+P7(a5000)+P8(a5000) % 1.41/1.48 [4]P1(a5000)+~P2(a5000)+~P3(a5000) % 1.41/1.48 [5]P4(a5000)+~P7(a5000)+~P8(a5000) % 1.41/1.48 [6]P7(a5000)+~P4(a5000)+~P8(a5000) % 1.41/1.48 [7]P8(a5000)+~P4(a5000)+~P7(a5000) % 1.41/1.48 [8]P2(a5000)+~P1(a5000)+~P3(a5000) % 1.41/1.48 [9]P3(a5000)+~P1(a5000)+~P2(a5000) % 1.41/1.48 [33]P5(x331)+P11(x331)+P11(f5(x331)) % 1.41/1.48 [34]P12(x341)+P10(x341)+P12(f7(x341)) % 1.41/1.48 [35]~P12(x351)+P10(x351)+~P12(f7(x351)) % 1.41/1.48 [36]~P11(x361)+P5(x361)+~P11(f5(x361)) % 1.41/1.48 [29]~P5(x292)+P11(x291)+~P11(x292) % 1.41/1.48 [30]~P5(x301)+P11(x301)+~P11(x302) % 1.41/1.48 [31]~P12(x312)+P12(x311)+~P10(x312) % 1.41/1.48 [32]~P10(x321)+P12(x321)+~P12(x322) % 1.41/1.48 [3]P6(a5000)+P1(a5000)+P9(a5000)+P4(a5000) % 1.41/1.48 [10]P6(a5000)+P1(a5000)+~P9(a5000)+~P4(a5000) % 1.41/1.48 [11]P6(a5000)+P9(a5000)+~P1(a5000)+~P4(a5000) % 1.41/1.48 [12]P6(a5000)+P4(a5000)+~P1(a5000)+~P9(a5000) % 1.41/1.48 [13]P1(a5000)+P9(a5000)+~P6(a5000)+~P4(a5000) % 1.41/1.48 [14]P1(a5000)+P4(a5000)+~P6(a5000)+~P9(a5000) % 1.41/1.48 [15]P9(a5000)+P4(a5000)+~P6(a5000)+~P1(a5000) % 1.41/1.48 [20]~P6(a5000)+~P1(a5000)+~P9(a5000)+~P4(a5000) % 1.41/1.48 %EqnAxiom % 1.41/1.48 % 1.41/1.48 %------------------------------------------- % 1.41/1.48 cnf(42,plain, % 1.41/1.48 (P12(x421)+~P12(a6)), % 1.41/1.48 inference(scs_inference,[],[22,24])). % 1.41/1.48 cnf(49,plain, % 1.41/1.48 (~P5(a1)+P11(x491)+~P8(a5000)), % 1.41/1.48 inference(scs_inference,[],[29,16])). % 1.41/1.48 cnf(50,plain, % 1.41/1.48 (~P5(x501)+~P11(x502)+P11(x503)), % 1.41/1.48 inference(scs_inference,[],[30,29])). % 1.41/1.48 cnf(51,plain, % 1.41/1.48 (~P12(x511)+P12(x512)+~P12(f7(x511))), % 1.41/1.48 inference(scs_inference,[],[31,35])). % 1.41/1.48 cnf(52,plain, % 1.41/1.48 (~P10(x521)+~P12(x522)+P12(x523)), % 1.41/1.48 inference(scs_inference,[],[32,31])). % 1.41/1.48 cnf(53,plain, % 1.41/1.48 (~P5(a1)+~P8(a5000)+P7(a5000)), % 1.41/1.48 inference(scs_inference,[],[49,21])). % 1.41/1.48 cnf(54,plain, % 1.41/1.48 (~P11(x541)+P11(x542)+~P6(a5000)), % 1.41/1.48 inference(scs_inference,[],[50,19])). % 1.41/1.48 cnf(55,plain, % 1.41/1.48 (~P12(x551)+P12(x552)+~P9(a5000)), % 1.41/1.48 inference(scs_inference,[],[52,17])). % 1.41/1.48 cnf(56,plain, % 1.41/1.48 (~P5(a1)+P4(a5000)+~P8(a5000)), % 1.41/1.48 inference(scs_inference,[],[53,5])). % 1.41/1.48 cnf(57,plain, % 1.41/1.48 (P11(x571)+~P6(a5000)+~P8(a5000)), % 1.41/1.48 inference(scs_inference,[],[54,16])). % 1.41/1.48 cnf(58,plain, % 1.41/1.48 (P12(x581)+~P9(a5000)+~P3(a5000)), % 1.41/1.48 inference(scs_inference,[],[55,18])). % 1.41/1.48 cnf(65,plain, % 1.41/1.48 (P5(a8)+P11(f5(a8))+P7(a5000)), % 1.41/1.48 inference(scs_inference,[],[33,21])). % 1.41/1.48 cnf(66,plain, % 1.41/1.48 (P12(x661)+P12(f7(x661))+P9(a5000)), % 1.41/1.48 inference(scs_inference,[],[34,26])). % 1.41/1.48 cnf(67,plain, % 1.41/1.48 (P12(x671)+P9(a5000)+P3(a5000)), % 1.41/1.48 inference(scs_inference,[],[66,28])). % 1.41/1.48 cnf(69,plain, % 1.41/1.48 (~P11(x691)+P11(a1)), % 1.41/1.48 inference(scs_inference,[],[16,27])). % 1.41/1.48 cnf(70,plain, % 1.41/1.48 (P11(x701)+P5(x701)+P11(a1)), % 1.41/1.48 inference(scs_inference,[],[69,33])). % 1.41/1.48 cnf(71,plain, % 1.41/1.48 (P11(x711)+P11(a1)+P6(a5000)), % 1.41/1.48 inference(scs_inference,[],[70,25])). % 1.41/1.48 cnf(72,plain, % 1.41/1.48 (P11(a1)+P6(a5000)), % 1.41/1.48 inference(factoring_inference,[],[71])). % 1.41/1.48 cnf(73,plain, % 1.41/1.48 (P6(a5000)+P8(a5000)), % 1.41/1.48 inference(scs_inference,[],[72,27])). % 1.41/1.48 cnf(77,plain, % 1.41/1.48 (P5(a1)+~P8(a5000)+~P11(f5(a1))), % 1.41/1.48 inference(scs_inference,[],[16,36])). % 1.41/1.48 cnf(78,plain, % 1.41/1.48 (P5(a1)+~P6(a5000)+~P8(a5000)), % 1.41/1.48 inference(scs_inference,[],[77,57])). % 1.41/1.48 cnf(79,plain, % 1.41/1.48 (~P6(a5000)+P4(a5000)+~P8(a5000)), % 1.41/1.48 inference(scs_inference,[],[78,56])). % 1.41/1.48 cnf(80,plain, % 1.41/1.48 (~P5(x801)+~P8(a5000)+P4(a5000)), % 1.41/1.48 inference(scs_inference,[],[79,25])). % 1.41/1.48 cnf(81,plain, % 1.41/1.48 (~P11(f5(a1))+P4(a5000)+~P8(a5000)), % 1.41/1.48 inference(scs_inference,[],[80,77])). % 1.41/1.48 cnf(82,plain, % 1.41/1.48 (~P11(f5(a1))+P7(a5000)+~P8(a5000)), % 1.41/1.48 inference(scs_inference,[],[81,6])). % 1.41/1.48 cnf(83,plain, % 1.41/1.48 (P11(x831)+~P11(f5(a1))+~P8(a5000)), % 1.41/1.48 inference(scs_inference,[],[82,23])). % 1.41/1.48 cnf(84,plain, % 1.41/1.48 (P11(x841)+~P11(x842)+~P11(f5(a1))), % 1.41/1.48 inference(scs_inference,[],[83,27])). % 1.41/1.48 cnf(85,plain, % 1.41/1.48 (P11(x851)+~P11(f5(a1))), % 1.41/1.48 inference(factoring_inference,[],[84])). % 1.41/1.48 cnf(95,plain, % 1.41/1.48 (P12(a3)+P1(a5000)+P2(a5000)), % 1.41/1.48 inference(scs_inference,[],[18,1])). % 1.41/1.48 cnf(96,plain, % 1.41/1.48 (P10(a3)+~P3(a5000)+~P12(f7(a3))), % 1.41/1.48 inference(scs_inference,[],[18,35])). % 1.41/1.48 cnf(97,plain, % 1.41/1.48 (P10(a3)+~P9(a5000)+~P3(a5000)), % 1.41/1.48 inference(scs_inference,[],[96,58])). % 1.41/1.48 cnf(98,plain, % 1.41/1.48 (~P10(x981)+P10(a3)+~P3(a5000)), % 1.41/1.48 inference(scs_inference,[],[97,26])). % 1.41/1.48 cnf(99,plain, % 1.41/1.48 (~P10(x991)+~P12(x992)+P10(a3)), % 1.41/1.48 inference(scs_inference,[],[98,28])). % 1.41/1.48 cnf(100,plain, % 1.41/1.48 (~P12(x1001)+P10(a3)+~P9(a5000)), % 1.41/1.48 inference(scs_inference,[],[99,17])). % 1.41/1.48 cnf(106,plain, % 1.41/1.48 (P12(x1061)+P12(a3)+P9(a5000)), % 1.41/1.48 inference(scs_inference,[],[18,67])). % 1.41/1.48 cnf(107,plain, % 1.41/1.48 (P12(a3)+P9(a5000)), % 1.41/1.48 inference(factoring_inference,[],[106])). % 1.41/1.48 cnf(108,plain, % 1.41/1.48 (P9(a5000)+P3(a5000)), % 1.41/1.48 inference(scs_inference,[],[107,28])). % 1.41/1.48 cnf(129,plain, % 1.41/1.48 (~P5(x1291)+~P11(x1292)+P7(a5000)), % 1.41/1.48 inference(scs_inference,[],[21,50])). % 1.41/1.48 cnf(130,plain, % 1.41/1.48 (~P11(x1301)+P11(f5(a8))+P7(a5000)), % 1.41/1.48 inference(scs_inference,[],[129,65])). % 1.41/1.48 cnf(131,plain, % 1.41/1.48 (P5(a1)+P11(f5(a8))+P7(a5000)), % 1.41/1.48 inference(scs_inference,[],[130,70])). % 1.41/1.49 cnf(132,plain, % 1.41/1.49 (~P5(x1321)+P5(a1)+P7(a5000)), % 1.41/1.49 inference(scs_inference,[],[131,129])). % 1.41/1.49 cnf(133,plain, % 1.41/1.49 (~P5(x1331)+P11(x1332)+P5(a1)), % 1.41/1.49 inference(scs_inference,[],[132,23])). % 1.41/1.49 cnf(138,plain, % 1.41/1.49 (P5(a8)+P7(a5000)+P11(a1)), % 1.41/1.49 inference(scs_inference,[],[21,70])). % 1.41/1.49 cnf(145,plain, % 1.41/1.49 (P10(a6)+P2(a5000)+P12(f7(a6))), % 1.41/1.49 inference(scs_inference,[],[22,34])). % 1.41/1.49 cnf(147,plain, % 1.41/1.49 (~P12(f7(x1471))+~P12(x1471)+P2(a5000)), % 1.41/1.49 inference(scs_inference,[],[22,51])). % 1.41/1.49 cnf(148,plain, % 1.41/1.49 (~P12(f7(a3))+P2(a5000)+P1(a5000)), % 1.41/1.49 inference(scs_inference,[],[147,95])). % 1.41/1.49 cnf(149,plain, % 1.41/1.49 (~P10(x1491)+~P12(x1492)+P2(a5000)), % 1.41/1.49 inference(scs_inference,[],[22,52])). % 1.41/1.49 cnf(150,plain, % 1.41/1.49 (~P12(x1501)+P12(f7(a6))+P2(a5000)), % 1.41/1.49 inference(scs_inference,[],[149,145])). % 1.41/1.49 cnf(151,plain, % 1.41/1.49 (P12(f7(a6))+P2(a5000)+P1(a5000)), % 1.41/1.49 inference(scs_inference,[],[150,95])). % 1.41/1.49 cnf(152,plain, % 1.41/1.49 (~P10(x1521)+P1(a5000)+P2(a5000)), % 1.41/1.49 inference(scs_inference,[],[151,149])). % 1.41/1.49 cnf(153,plain, % 1.41/1.49 (~P12(x1531)+P2(a5000)+~P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[22,55])). % 1.41/1.49 cnf(154,plain, % 1.41/1.49 (~P9(a5000)+P2(a5000)+P1(a5000)), % 1.41/1.49 inference(scs_inference,[],[153,95])). % 1.41/1.49 cnf(161,plain, % 1.41/1.49 (~P7(a5000)+P8(a5000)), % 1.41/1.49 inference(scs_inference,[],[23,27])). % 1.41/1.49 cnf(162,plain, % 1.41/1.49 (P8(a5000)+P4(a5000)), % 1.41/1.49 inference(scs_inference,[],[161,2])). % 1.41/1.49 cnf(163,plain, % 1.41/1.49 (P4(a5000)+P11(a1)), % 1.41/1.49 inference(scs_inference,[],[162,16])). % 1.41/1.49 cnf(164,plain, % 1.41/1.49 (P5(a1)+P4(a5000)+~P11(f5(a1))), % 1.41/1.49 inference(scs_inference,[],[163,36])). % 1.41/1.49 cnf(165,plain, % 1.41/1.49 (~P5(x1651)+P4(a5000)+P5(a1)), % 1.41/1.49 inference(scs_inference,[],[164,133])). % 1.41/1.49 cnf(166,plain, % 1.41/1.49 (P11(x1661)+~P4(a5000)+~P8(a5000)), % 1.41/1.49 inference(scs_inference,[],[23,6])). % 1.41/1.49 cnf(167,plain, % 1.41/1.49 (~P4(a5000)+P5(a1)+~P8(a5000)), % 1.41/1.49 inference(scs_inference,[],[166,77])). % 1.41/1.49 cnf(168,plain, % 1.41/1.49 (P5(a1)+~P7(a5000)+~P8(a5000)), % 1.41/1.49 inference(scs_inference,[],[167,5])). % 1.41/1.49 cnf(169,plain, % 1.41/1.49 (~P11(x1691)+P5(a1)+~P7(a5000)), % 1.41/1.49 inference(scs_inference,[],[168,27])). % 1.41/1.49 cnf(170,plain, % 1.41/1.49 (P5(a1)+~P7(a5000)), % 1.41/1.49 inference(scs_inference,[],[169,70])). % 1.41/1.49 cnf(171,plain, % 1.41/1.49 (~P7(a5000)+P6(a5000)), % 1.41/1.49 inference(scs_inference,[],[170,25])). % 1.41/1.49 cnf(172,plain, % 1.41/1.49 (P6(a5000)+~P11(a8)), % 1.41/1.49 inference(scs_inference,[],[171,21])). % 1.41/1.49 cnf(180,plain, % 1.41/1.49 (P11(x1801)+P11(f5(a8))+P5(a8)), % 1.41/1.49 inference(scs_inference,[],[23,65])). % 1.41/1.49 cnf(181,plain, % 1.41/1.49 (P11(f5(a8))+P5(a8)), % 1.41/1.49 inference(factoring_inference,[],[180])). % 1.41/1.49 cnf(182,plain, % 1.41/1.49 (P5(a8)+P8(a5000)), % 1.41/1.49 inference(scs_inference,[],[181,27])). % 1.41/1.49 cnf(183,plain, % 1.41/1.49 (P8(a5000)+P5(a1)+P7(a5000)), % 1.41/1.49 inference(scs_inference,[],[182,132])). % 1.41/1.49 cnf(184,plain, % 1.41/1.49 (P5(a1)+~P4(a5000)+P7(a5000)), % 1.41/1.49 inference(scs_inference,[],[183,6])). % 1.41/1.49 cnf(185,plain, % 1.41/1.49 (~P11(x1851)+~P4(a5000)+P7(a5000)), % 1.41/1.49 inference(scs_inference,[],[184,129])). % 1.41/1.49 cnf(186,plain, % 1.41/1.49 (~P4(a5000)+P5(a8)+P7(a5000)), % 1.41/1.49 inference(scs_inference,[],[185,138])). % 1.41/1.49 cnf(187,plain, % 1.41/1.49 (~P4(a5000)+P5(a8)+P5(a1)), % 1.41/1.49 inference(scs_inference,[],[186,170])). % 1.41/1.49 cnf(188,plain, % 1.41/1.49 (~P11(f5(a1))+P5(a8)+P5(a1)), % 1.41/1.49 inference(scs_inference,[],[187,164])). % 1.41/1.49 cnf(189,plain, % 1.41/1.49 (~P5(x1891)+P5(a8)+P5(a1)), % 1.41/1.49 inference(scs_inference,[],[188,133])). % 1.41/1.49 cnf(190,plain, % 1.41/1.49 (P5(a8)+P5(a1)+~P6(a5000)), % 1.41/1.49 inference(scs_inference,[],[189,19])). % 1.41/1.49 cnf(191,plain, % 1.41/1.49 (~P6(a5000)+P4(a5000)+P5(a1)), % 1.41/1.49 inference(scs_inference,[],[190,165])). % 1.41/1.49 cnf(192,plain, % 1.41/1.49 (P5(a1)+P4(a5000)+~P11(a8)), % 1.41/1.49 inference(scs_inference,[],[191,172])). % 1.41/1.49 cnf(193,plain, % 1.41/1.49 (~P11(a8)+P5(a1)+~P8(a5000)), % 1.41/1.49 inference(scs_inference,[],[192,167])). % 1.41/1.49 cnf(194,plain, % 1.41/1.49 (~P5(x1941)+~P8(a5000)+P5(a1)), % 1.41/1.49 inference(scs_inference,[],[193,133])). % 1.41/1.49 cnf(195,plain, % 1.41/1.49 (P11(f5(a8))+~P8(a5000)+P5(a1)), % 1.41/1.49 inference(scs_inference,[],[194,181])). % 1.41/1.49 cnf(196,plain, % 1.41/1.49 (P11(f5(a8))+~P8(a5000)+P6(a5000)), % 1.41/1.49 inference(scs_inference,[],[195,25])). % 1.41/1.49 cnf(197,plain, % 1.41/1.49 (P11(f5(a8))+P6(a5000)), % 1.41/1.49 inference(scs_inference,[],[196,73])). % 1.41/1.49 cnf(198,plain, % 1.41/1.49 (P6(a5000)+~P4(a5000)+P7(a5000)), % 1.41/1.49 inference(scs_inference,[],[197,185])). % 1.41/1.49 cnf(199,plain, % 1.41/1.49 (~P4(a5000)+P6(a5000)), % 1.41/1.49 inference(scs_inference,[],[198,171])). % 1.41/1.49 cnf(206,plain, % 1.41/1.49 (P11(x2061)+~P11(x2062)+P11(f5(a8))), % 1.41/1.49 inference(scs_inference,[],[23,130])). % 1.41/1.49 cnf(207,plain, % 1.41/1.49 (P11(f5(a8))+~P11(x2071)), % 1.41/1.49 inference(factoring_inference,[],[206])). % 1.41/1.49 cnf(208,plain, % 1.41/1.49 (P11(f5(a8))+~P8(a5000)), % 1.41/1.49 inference(scs_inference,[],[207,16])). % 1.41/1.49 cnf(247,plain, % 1.41/1.49 (~P2(a5000)+P3(a5000)), % 1.41/1.49 inference(scs_inference,[],[24,28])). % 1.41/1.49 cnf(248,plain, % 1.41/1.49 (P3(a5000)+P1(a5000)), % 1.41/1.49 inference(scs_inference,[],[247,1])). % 1.41/1.49 cnf(251,plain, % 1.41/1.49 (P12(x2511)+~P1(a5000)+~P3(a5000)), % 1.41/1.49 inference(scs_inference,[],[24,8])). % 1.41/1.49 cnf(259,plain, % 1.41/1.49 (P10(x2591)+~P12(x2591)+~P2(a5000)), % 1.41/1.49 inference(scs_inference,[],[24,35])). % 1.41/1.49 cnf(260,plain, % 1.41/1.49 (P10(x2601)+~P2(a5000)+~P12(a6)), % 1.41/1.49 inference(scs_inference,[],[259,42])). % 1.41/1.49 cnf(261,plain, % 1.41/1.49 (P10(x2611)+~P12(a6)), % 1.41/1.49 inference(scs_inference,[],[260,22])). % 1.41/1.49 cnf(275,plain, % 1.41/1.49 (P12(x2751)+~P10(x2752)+P1(a5000)), % 1.41/1.49 inference(scs_inference,[],[24,152])). % 1.41/1.49 cnf(277,plain, % 1.41/1.49 (P12(x2771)+~P9(a5000)+P1(a5000)), % 1.41/1.49 inference(scs_inference,[],[24,154])). % 1.41/1.49 cnf(278,plain, % 1.41/1.49 (P1(a5000)+P10(a3)+~P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[277,100])). % 1.41/1.49 cnf(313,plain, % 1.41/1.49 (~P12(f7(a3))+P9(a5000)+~P3(a5000)), % 1.41/1.49 inference(scs_inference,[],[26,96])). % 1.41/1.49 cnf(314,plain, % 1.41/1.49 (P9(a5000)+~P1(a5000)+~P3(a5000)), % 1.41/1.49 inference(scs_inference,[],[313,251])). % 1.41/1.49 cnf(315,plain, % 1.41/1.49 (~P1(a5000)+P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[314,108])). % 1.41/1.49 cnf(331,plain, % 1.41/1.49 (~P11(x3311)+~P11(f5(a1))+P4(a5000)), % 1.41/1.49 inference(scs_inference,[],[27,81])). % 1.41/1.49 cnf(332,plain, % 1.41/1.49 (~P11(f5(a1))+P4(a5000)), % 1.41/1.49 inference(factoring_inference,[],[331])). % 1.41/1.49 cnf(333,plain, % 1.41/1.49 (P4(a5000)+~P7(a5000)), % 1.41/1.49 inference(scs_inference,[],[332,23])). % 1.41/1.49 cnf(334,plain, % 1.41/1.49 (P4(a5000)+~P11(a8)), % 1.41/1.49 inference(scs_inference,[],[333,21])). % 1.41/1.49 cnf(360,plain, % 1.41/1.49 (~P12(x3601)+~P2(a5000)+P1(a5000)), % 1.41/1.49 inference(scs_inference,[],[28,4])). % 1.41/1.49 cnf(361,plain, % 1.41/1.49 (~P10(x3611)+~P2(a5000)+P1(a5000)), % 1.41/1.49 inference(scs_inference,[],[360,275])). % 1.41/1.49 cnf(362,plain, % 1.41/1.49 (~P2(a5000)+P1(a5000)+~P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[361,278])). % 1.41/1.49 cnf(363,plain, % 1.41/1.49 (~P12(f7(a3))+~P9(a5000)+P1(a5000)), % 1.41/1.49 inference(scs_inference,[],[362,148])). % 1.41/1.49 cnf(364,plain, % 1.41/1.49 (~P12(x3641)+P1(a5000)+~P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[363,55])). % 1.41/1.49 cnf(365,plain, % 1.41/1.49 (~P9(a5000)+P1(a5000)), % 1.41/1.49 inference(scs_inference,[],[364,277])). % 1.41/1.49 cnf(366,plain, % 1.41/1.49 (~P10(x3661)+P1(a5000)), % 1.41/1.49 inference(scs_inference,[],[365,26])). % 1.41/1.49 cnf(421,plain, % 1.41/1.49 (P4(a5000)+~P6(a5000)), % 1.41/1.49 inference(scs_inference,[],[162,79])). % 1.41/1.49 cnf(423,plain, % 1.41/1.49 (~P5(x4231)+P4(a5000)), % 1.41/1.49 inference(scs_inference,[],[162,80])). % 1.41/1.49 cnf(426,plain, % 1.41/1.49 (P1(a5000)+P9(a5000)+~P4(a5000)), % 1.41/1.49 inference(scs_inference,[],[199,13])). % 1.41/1.49 cnf(427,plain, % 1.41/1.49 (~P4(a5000)+P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[426,315])). % 1.41/1.49 cnf(428,plain, % 1.41/1.49 (P9(a5000)+P8(a5000)), % 1.41/1.49 inference(scs_inference,[],[427,162])). % 1.41/1.49 cnf(429,plain, % 1.41/1.49 (P8(a5000)+P10(a2)), % 1.41/1.49 inference(scs_inference,[],[428,17])). % 1.41/1.49 cnf(430,plain, % 1.41/1.49 (P10(a2)+P11(a1)), % 1.41/1.49 inference(scs_inference,[],[429,16])). % 1.41/1.49 cnf(431,plain, % 1.41/1.49 (P11(a1)+P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[430,26])). % 1.41/1.49 cnf(432,plain, % 1.41/1.49 (P11(f5(a8))+P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[431,207])). % 1.41/1.49 cnf(433,plain, % 1.41/1.49 (~P5(x4331)+P11(x4332)+P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[432,50])). % 1.41/1.49 cnf(434,plain, % 1.41/1.49 (P11(x4341)+P9(a5000)+~P6(a5000)), % 1.41/1.49 inference(scs_inference,[],[433,19])). % 1.41/1.49 cnf(449,plain, % 1.41/1.49 (P6(a5000)+P1(a5000)+P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[199,3])). % 1.41/1.49 cnf(450,plain, % 1.41/1.49 (P11(x4501)+P1(a5000)+P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[449,434])). % 1.41/1.49 cnf(451,plain, % 1.41/1.49 (P1(a5000)+P9(a5000)+P7(a5000)), % 1.41/1.49 inference(scs_inference,[],[450,21])). % 1.41/1.49 cnf(452,plain, % 1.41/1.49 (P7(a5000)+P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[451,315])). % 1.41/1.49 cnf(453,plain, % 1.41/1.49 (P11(x4531)+P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[452,23])). % 1.41/1.49 cnf(465,plain, % 1.41/1.49 (P6(a5000)+~P1(a5000)+~P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[199,12])). % 1.41/1.49 cnf(466,plain, % 1.41/1.49 (~P1(a5000)+~P9(a5000)+P5(a4)), % 1.41/1.49 inference(scs_inference,[],[465,19])). % 1.41/1.49 cnf(492,plain, % 1.41/1.49 (~P1(a5000)+~P9(a5000)+~P4(a5000)), % 1.41/1.49 inference(scs_inference,[],[199,20])). % 1.41/1.49 cnf(542,plain, % 1.41/1.49 (P3(a5000)+~P9(a5000)+~P4(a5000)), % 1.41/1.49 inference(scs_inference,[],[248,492])). % 1.41/1.49 cnf(543,plain, % 1.41/1.49 (P12(x5431)+~P4(a5000)+~P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[542,58])). % 1.41/1.49 cnf(586,plain, % 1.41/1.49 (P10(x5861)+~P4(a5000)+~P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[261,543])). % 1.41/1.49 cnf(587,plain, % 1.41/1.49 (P10(x5871)+~P4(a5000)), % 1.41/1.49 inference(scs_inference,[],[586,427])). % 1.41/1.49 cnf(588,plain, % 1.41/1.49 (~P4(a5000)+P1(a5000)), % 1.41/1.49 inference(scs_inference,[],[587,366])). % 1.41/1.49 cnf(589,plain, % 1.41/1.49 (~P11(f5(a1))+P1(a5000)), % 1.41/1.49 inference(scs_inference,[],[588,332])). % 1.41/1.49 cnf(590,plain, % 1.41/1.49 (P1(a5000)+~P7(a5000)), % 1.41/1.49 inference(scs_inference,[],[589,23])). % 1.41/1.49 cnf(591,plain, % 1.41/1.49 (~P7(a5000)+P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[590,315])). % 1.41/1.49 cnf(592,plain, % 1.41/1.49 (P9(a5000)+~P11(a8)), % 1.41/1.49 inference(scs_inference,[],[591,21])). % 1.41/1.49 cnf(593,plain, % 1.41/1.49 (~P11(a8)+P10(a2)), % 1.41/1.49 inference(scs_inference,[],[592,17])). % 1.41/1.49 cnf(594,plain, % 1.41/1.49 (~P11(f5(a1))+P10(a2)), % 1.41/1.49 inference(scs_inference,[],[593,85])). % 1.41/1.49 cnf(595,plain, % 1.41/1.49 (P10(a2)+P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[594,453])). % 1.41/1.49 cnf(596,plain, % 1.41/1.49 (P9(a5000)), % 1.41/1.49 inference(scs_inference,[],[595,26])). % 1.41/1.49 cnf(602,plain, % 1.41/1.49 (P1(a5000)), % 1.41/1.49 inference(scs_inference,[],[596,365])). % 1.41/1.49 cnf(605,plain, % 1.41/1.49 (~P1(a5000)+P5(a4)), % 1.41/1.49 inference(scs_inference,[],[596,466])). % 1.41/1.49 cnf(606,plain, % 1.41/1.49 (~P1(a5000)+~P4(a5000)), % 1.41/1.49 inference(scs_inference,[],[596,492])). % 1.41/1.49 cnf(637,plain, % 1.41/1.49 ($false), % 1.41/1.49 inference(scs_inference,[],[602,605,606,162,163,208,332,333,334,421,423]), % 1.41/1.49 ['proof']). % 1.41/1.49 % SZS output end Proof % 1.41/1.49 % Total time :0.870000s %------------------------------------------------------------------------------