%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MSC008-2.002 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 11:52:11 EDT 2024 % Result : Unsatisfiable 2.23s 2.33s % Output : CNFRefutation 2.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : MSC008-2.002 : TPTP v8.2.0. Released v1.0.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n018.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 05:48:24 EDT 2024 % 0.13/0.34 % CPUTime : % 0.21/0.59 start to proof:theBenchmark % 2.23/2.32 %------------------------------------------- % 2.23/2.32 % File :CSE---1.7 % 2.23/2.32 % Problem :theBenchmark % 2.23/2.32 % Transform :cnf % 2.23/2.32 % Format :tptp:raw % 2.23/2.32 % Command :java -jar mcs_scs.jar %d %s % 2.23/2.32 % 2.23/2.32 % Result :Theorem 1.690000s % 2.23/2.32 % Output :CNFRefutation 1.690000s % 2.23/2.32 %------------------------------------------- % 2.23/2.33 %-------------------------------------------------------------------------- % 2.23/2.33 % File : MSC008-2.002 : TPTP v8.2.0. Released v1.0.0. % 2.23/2.33 % Domain : Miscellaneous % 2.23/2.33 % Problem : The inconstructability of a Graeco-Latin Square % 2.23/2.33 % Version : Especial. % 2.23/2.33 % Theorem formulation : Buggy; A 2x2 square. % 2.23/2.33 % English : The constructibility of Graeco-Latin squares of order 4t+2. % 2.23/2.33 % This is impossible for t=0,1, but possible for all other % 2.23/2.33 % cases. % 2.23/2.33 % 2.23/2.33 % Refs : [Rob63] Robinson (1963), Theorem Proving on the Computer % 2.23/2.33 % Source : [SPRFN] % 2.23/2.33 % Names : LATINSQ [SPRFN] % 2.23/2.33 % : - [Rob63] % 2.23/2.33 % 2.23/2.33 % Status : Unsatisfiable % 2.23/2.33 % Rating : 0.00 v6.2.0, 0.12 v6.1.0, 0.00 v2.7.0, 0.17 v2.6.0, 0.11 v2.5.0, 0.00 v2.4.0, 0.00 v2.1.0, 0.00 v2.0.0 % 2.23/2.33 % Syntax : Number of clauses : 16 ( 2 unt; 7 nHn; 9 RR) % 2.23/2.33 % Number of literals : 40 ( 0 equ; 18 neg) % 2.23/2.33 % Maximal clause size : 6 ( 2 avg) % 2.23/2.33 % Maximal term depth : 1 ( 1 avg) % 2.23/2.33 % Number of predicates : 3 ( 3 usr; 0 prp; 2-3 aty) % 2.23/2.33 % Number of functors : 2 ( 2 usr; 2 con; 0-0 aty) % 2.23/2.33 % Number of variables : 45 ( 0 sgn) % 2.23/2.33 % SPC : CNF_UNS_EPR_NEQ_NHN % 2.23/2.33 % 2.23/2.33 % Comments : This uses the form of the theorem given in [Rob63], which fails % 2.23/2.33 % to capture the intended semantics. The error is that the clauses % 2.23/2.33 % with type "theorem" insist that two squares with the same Greek % 2.23/2.33 % and Latin elements be in the same row OR the same column. What % 2.23/2.33 % is required that the two squares be the same (i.e., there cannot % 2.23/2.33 % be two such squares) so that they are in the same row AND the % 2.23/2.33 % same column. % 2.23/2.33 %-------------------------------------------------------------------------- % 2.23/2.33 cnf(p1_is_not_p2,axiom, % 2.23/2.33 ~ eq(p1,p2) ). % 2.23/2.33 % 2.23/2.33 cnf(reflexivity,axiom, % 2.23/2.33 eq(A,A) ). % 2.23/2.33 % 2.23/2.33 cnf(symmetry,axiom, % 2.23/2.33 ( ~ eq(A,B) % 2.23/2.33 | eq(B,A) ) ). % 2.23/2.33 % 2.23/2.33 cnf(latin_element_is_unique,axiom, % 2.23/2.33 ( ~ latin(A,B,C) % 2.23/2.33 | ~ latin(A,B,D) % 2.23/2.33 | eq(D,C) ) ). % 2.23/2.33 % 2.23/2.33 cnf(latin_column_is_unique,axiom, % 2.23/2.33 ( ~ latin(A,B,C) % 2.23/2.33 | ~ latin(A,D,C) % 2.23/2.33 | eq(D,B) ) ). % 2.23/2.33 % 2.23/2.33 cnf(latin_row_is_unique,axiom, % 2.23/2.33 ( ~ latin(A,B,C) % 2.23/2.33 | ~ latin(D,B,C) % 2.23/2.33 | eq(D,A) ) ). % 2.23/2.33 % 2.23/2.33 cnf(greek_element_is_unique,axiom, % 2.23/2.33 ( ~ greek(A,B,C) % 2.23/2.33 | ~ greek(A,B,D) % 2.23/2.33 | eq(D,C) ) ). % 2.23/2.33 % 2.23/2.33 cnf(greek_column_is_unique,axiom, % 2.23/2.33 ( ~ greek(A,B,C) % 2.23/2.33 | ~ greek(A,D,C) % 2.23/2.33 | eq(D,B) ) ). % 2.23/2.33 % 2.23/2.33 cnf(greek_row_is_unique,axiom, % 2.23/2.33 ( ~ greek(A,B,C) % 2.23/2.33 | ~ greek(D,B,C) % 2.23/2.33 | eq(D,A) ) ). % 2.23/2.33 % 2.23/2.33 cnf(latin_cell_element,axiom, % 2.23/2.33 ( latin(E,F,p1) % 2.23/2.33 | latin(E,F,p2) ) ). % 2.23/2.33 % 2.23/2.33 cnf(latin_column_required,axiom, % 2.23/2.33 ( latin(G,p1,H) % 2.23/2.33 | latin(G,p2,H) ) ). % 2.23/2.33 % 2.23/2.33 cnf(latin_row_required,axiom, % 2.23/2.33 ( latin(p1,I,J) % 2.23/2.33 | latin(p2,I,J) ) ). % 2.23/2.33 % 2.23/2.33 cnf(greek_cell_element,axiom, % 2.23/2.33 ( greek(K,L,p1) % 2.23/2.33 | greek(K,L,p2) ) ). % 2.23/2.33 % 2.23/2.33 cnf(greek_column_required,axiom, % 2.23/2.33 ( greek(M,p1,N) % 2.23/2.33 | greek(M,p2,N) ) ). % 2.23/2.33 % 2.23/2.33 cnf(greek_row_required,axiom, % 2.23/2.33 ( greek(p1,O,P) % 2.23/2.33 | greek(p2,O,P) ) ). % 2.23/2.33 % 2.23/2.33 cnf(no_two_same,negated_conjecture, % 2.23/2.33 ( ~ greek(A,B,C) % 2.23/2.33 | ~ latin(A,B,D) % 2.23/2.33 | ~ greek(E,F,C) % 2.23/2.33 | ~ latin(E,F,D) % 2.23/2.33 | eq(F,B) % 2.23/2.33 | eq(E,A) ) ). % 2.23/2.33 % 2.23/2.33 %----This is the fixed version. Original is wrong I think % 2.23/2.33 %input_clause(no_two_same1,hypothesis, % 2.23/2.33 % [--greek(A,B,C), % 2.23/2.33 % --latin(A,B,D), % 2.23/2.33 % --greek(E,F,C), % 2.23/2.33 % --latin(E,F,D), % 2.23/2.33 % ++eq(F,B)]). % 2.23/2.33 %input_clause(no_two_same2,negated_conjecture, % 2.23/2.33 % [--greek(A,B,C), % 2.23/2.33 % --latin(A,B,D), % 2.23/2.33 % --greek(E,F,C), % 2.23/2.33 % --latin(E,F,D), % 2.23/2.33 % ++eq(E,A)]). % 2.23/2.33 %-------------------------------------------------------------------------- % 2.23/2.33 %------------------------------------------- % 2.23/2.33 % Proof found % 2.23/2.33 % SZS status Theorem for theBenchmark % 2.23/2.33 % SZS output start Proof % 2.23/2.33 %ClaNum:16(EqnAxiom:0) % 2.23/2.33 %VarNum:94(SingletonVarNum:45) % 2.23/2.33 %MaxLitNum:6 % 2.23/2.33 %MaxfuncDepth:0 % 2.23/2.33 %SharedTerms:3 % 2.23/2.33 %goalClause: 16 % 2.23/2.33 [2]~P1(a1,a2) % 2.23/2.33 [1]P1(x11,x11) % 2.23/2.33 [3]~P1(x32,x31)+P1(x31,x32) % 2.23/2.33 [4]P2(x41,x42,a2)+P2(x41,x42,a1) % 2.23/2.33 [5]P3(x51,x52,a2)+P3(x51,x52,a1) % 2.23/2.33 [6]P2(x61,a2,x62)+P2(x61,a1,x62) % 2.23/2.33 [7]P3(x71,a2,x72)+P3(x71,a1,x72) % 2.23/2.33 [8]P2(a2,x81,x82)+P2(a1,x81,x82) % 2.23/2.33 [9]P3(a2,x91,x92)+P3(a1,x91,x92) % 2.23/2.33 [10]~P2(x103,x104,x102)+P1(x101,x102)+~P2(x103,x104,x101) % 2.23/2.33 [11]~P3(x113,x114,x112)+P1(x111,x112)+~P3(x113,x114,x111) % 2.23/2.33 [12]~P2(x123,x122,x124)+P1(x121,x122)+~P2(x123,x121,x124) % 2.23/2.33 [13]~P3(x133,x132,x134)+P1(x131,x132)+~P3(x133,x131,x134) % 2.23/2.33 [14]~P2(x142,x143,x144)+P1(x141,x142)+~P2(x141,x143,x144) % 2.23/2.33 [15]~P3(x152,x153,x154)+P1(x151,x152)+~P3(x151,x153,x154) % 2.23/2.33 [16]~P2(x164,x162,x165)+~P3(x164,x162,x166)+P1(x161,x162)+~P2(x163,x161,x165)+P1(x163,x164)+~P3(x163,x161,x166) % 2.23/2.33 %EqnAxiom % 2.23/2.33 % 2.23/2.33 %------------------------------------------- % 2.23/2.33 cnf(17,plain, % 2.23/2.33 (~P1(a2,a1)), % 2.23/2.33 inference(scs_inference,[],[2,3])). % 2.23/2.33 cnf(19,plain, % 2.23/2.33 (~P3(a1,a1,x191)+~P2(a2,a2,x192)+~P3(a2,a2,x191)+~P2(a1,a1,x192)), % 2.23/2.33 inference(scs_inference,[],[2,3,16])). % 2.23/2.33 cnf(221,plain, % 2.23/2.33 (~P2(x2211,x2212,a2)+~P2(x2211,x2212,a1)), % 2.23/2.33 inference(scs_inference,[],[2,3,10])). % 2.23/2.33 cnf(237,plain, % 2.23/2.33 (P2(x2371,a1,a1)+~P2(x2371,a2,a2)), % 2.23/2.33 inference(scs_inference,[],[221,6])). % 2.23/2.33 cnf(253,plain, % 2.23/2.33 (P2(a1,a2,a2)+P2(a2,a1,a1)), % 2.23/2.33 inference(scs_inference,[],[237,8])). % 2.23/2.33 cnf(269,plain, % 2.23/2.33 (~P2(a1,a2,a1)+P2(a2,a1,a1)), % 2.23/2.33 inference(scs_inference,[],[253,221])). % 2.23/2.33 cnf(285,plain, % 2.23/2.34 (~P2(a2,a1,a2)+~P2(a1,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[269,221])). % 2.23/2.34 cnf(301,plain, % 2.23/2.34 (P2(a2,a2,a2)+~P2(a1,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[285,6])). % 2.23/2.34 cnf(317,plain, % 2.23/2.34 (~P2(a2,a2,a1)+~P2(a1,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[301,221])). % 2.23/2.34 cnf(333,plain, % 2.23/2.34 (P2(a1,a2,a2)+~P2(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[317,4])). % 2.23/2.34 cnf(349,plain, % 2.23/2.34 (P2(a1,a1,a1)+~P2(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[333,237])). % 2.23/2.34 cnf(365,plain, % 2.23/2.34 (~P2(a1,a1,a2)+~P2(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[349,221])). % 2.23/2.34 cnf(381,plain, % 2.23/2.34 (P2(a2,a1,a2)+~P2(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[365,8])). % 2.23/2.34 cnf(397,plain, % 2.23/2.34 (~P2(a2,a1,a1)+~P2(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[381,221])). % 2.23/2.34 cnf(413,plain, % 2.23/2.34 (P2(a2,a2,a2)+~P2(a2,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[397,4])). % 2.23/2.34 cnf(429,plain, % 2.23/2.34 (P2(a2,a2,a2)+P2(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[413,8])). % 2.23/2.34 cnf(445,plain, % 2.23/2.34 (P2(a2,a2,a2)+~P2(a1,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[429,221])). % 2.23/2.34 cnf(461,plain, % 2.23/2.34 (~P2(a1,a1,a2)+P2(a2,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[445,237])). % 2.23/2.34 cnf(477,plain, % 2.23/2.34 (~P2(a1,a1,a2)+~P2(a2,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[461,221])). % 2.23/2.34 cnf(493,plain, % 2.23/2.34 (~P2(a2,a1,a2)+P2(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[477,4])). % 2.23/2.34 cnf(524,plain, % 2.23/2.34 (~P3(x5241,x5242,a2)+~P3(x5241,x5242,a1)), % 2.23/2.34 inference(scs_inference,[],[2,3,11])). % 2.23/2.34 cnf(540,plain, % 2.23/2.34 (P3(x5401,a1,a1)+~P3(x5401,a2,a2)), % 2.23/2.34 inference(scs_inference,[],[524,7])). % 2.23/2.34 cnf(556,plain, % 2.23/2.34 (P3(a1,a2,a2)+P3(a2,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[540,9])). % 2.23/2.34 cnf(572,plain, % 2.23/2.34 (~P3(a1,a2,a1)+P3(a2,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[556,524])). % 2.23/2.34 cnf(588,plain, % 2.23/2.34 (~P3(a2,a1,a2)+~P3(a1,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[572,524])). % 2.23/2.34 cnf(604,plain, % 2.23/2.34 (P3(a2,a2,a2)+~P3(a1,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[588,7])). % 2.23/2.34 cnf(620,plain, % 2.23/2.34 (~P3(a2,a2,a1)+~P3(a1,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[604,524])). % 2.23/2.34 cnf(636,plain, % 2.23/2.34 (P3(a1,a2,a2)+~P3(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[620,5])). % 2.23/2.34 cnf(652,plain, % 2.23/2.34 (P3(a1,a1,a1)+~P3(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[636,540])). % 2.23/2.34 cnf(668,plain, % 2.23/2.34 (~P3(a1,a1,a2)+~P3(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[652,524])). % 2.23/2.34 cnf(684,plain, % 2.23/2.34 (P3(a2,a1,a2)+~P3(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[668,9])). % 2.23/2.34 cnf(700,plain, % 2.23/2.34 (~P3(a2,a1,a1)+~P3(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[684,524])). % 2.23/2.34 cnf(716,plain, % 2.23/2.34 (P3(a2,a2,a2)+~P3(a2,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[700,5])). % 2.23/2.34 cnf(732,plain, % 2.23/2.34 (P3(a2,a2,a2)+P3(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[716,9])). % 2.23/2.34 cnf(748,plain, % 2.23/2.34 (P3(a2,a2,a2)+~P3(a1,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[732,524])). % 2.23/2.34 cnf(827,plain, % 2.23/2.34 (~P2(x8271,a1,x8272)+~P2(x8271,a2,x8272)), % 2.23/2.34 inference(scs_inference,[],[17,3,12])). % 2.23/2.34 cnf(843,plain, % 2.23/2.34 (P2(x8431,a2,a1)+~P2(x8431,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[827,4])). % 2.23/2.34 cnf(859,plain, % 2.23/2.34 (P2(a1,a1,a2)+P2(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[843,8])). % 2.23/2.34 cnf(875,plain, % 2.23/2.34 (P2(a1,a1,a2)+~P2(a2,a2,a2)), % 2.23/2.34 inference(scs_inference,[],[859,221])). % 2.23/2.34 cnf(891,plain, % 2.23/2.34 (~P2(a2,a2,a2)+~P2(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[875,221])). % 2.23/2.34 cnf(907,plain, % 2.23/2.34 (P2(a2,a1,a2)+~P2(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[891,6])). % 2.23/2.34 cnf(954,plain, % 2.23/2.34 (~P3(x9541,a2,x9542)+~P3(x9541,a1,x9542)), % 2.23/2.34 inference(scs_inference,[],[2,3,13])). % 2.23/2.34 cnf(970,plain, % 2.23/2.34 (~P3(x9701,a2,a1)+P3(x9701,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[954,5])). % 2.23/2.34 cnf(986,plain, % 2.23/2.34 (P3(a1,a2,a1)+P3(a2,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[970,9])). % 2.23/2.34 cnf(1002,plain, % 2.23/2.34 (P3(a1,a2,a1)+~P3(a2,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[986,524])). % 2.23/2.34 cnf(1018,plain, % 2.23/2.34 (~P3(a2,a1,a1)+~P3(a1,a2,a2)), % 2.23/2.34 inference(scs_inference,[],[1002,524])). % 2.23/2.34 cnf(1034,plain, % 2.23/2.34 (P3(a2,a2,a1)+~P3(a1,a2,a2)), % 2.23/2.34 inference(scs_inference,[],[1018,7])). % 2.23/2.34 cnf(1050,plain, % 2.23/2.34 (P3(a2,a1,a2)+~P3(a1,a2,a2)), % 2.23/2.34 inference(scs_inference,[],[1034,970])). % 2.23/2.34 cnf(1066,plain, % 2.23/2.34 (~P3(a2,a2,a2)+~P3(a1,a2,a2)), % 2.23/2.34 inference(scs_inference,[],[1050,954])). % 2.23/2.34 cnf(1082,plain, % 2.23/2.34 (~P3(a2,a2,a2)+P3(a1,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[1066,5])). % 2.23/2.34 cnf(1098,plain, % 2.23/2.34 (~P3(a2,a2,a2)+~P3(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1082,954])). % 2.23/2.34 cnf(1114,plain, % 2.23/2.34 (~P3(a2,a1,a1)+~P3(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1098,716])). % 2.23/2.34 cnf(1130,plain, % 2.23/2.34 (P3(a1,a2,a2)+~P3(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1114,556])). % 2.23/2.34 cnf(1177,plain, % 2.23/2.34 (~P2(a1,x11771,x11772)+~P2(a2,x11771,x11772)), % 2.23/2.34 inference(scs_inference,[],[17,3,14])). % 2.23/2.34 cnf(1193,plain, % 2.23/2.34 (P2(a2,x11931,a1)+~P2(a1,x11931,a2)), % 2.23/2.34 inference(scs_inference,[],[1177,4])). % 2.23/2.34 cnf(1209,plain, % 2.23/2.34 (P2(a2,a1,a2)+~P2(a1,a2,a2)), % 2.23/2.34 inference(scs_inference,[],[1193,381])). % 2.23/2.34 cnf(1225,plain, % 2.23/2.34 (~P2(a1,a2,a2)+~P2(a2,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1209,221])). % 2.23/2.34 cnf(1241,plain, % 2.23/2.34 (~P2(a2,a1,a1)+P2(a1,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[1225,6])). % 2.23/2.34 cnf(1257,plain, % 2.23/2.34 (~P2(a2,a1,a1)+P2(a1,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[1241,843])). % 2.23/2.34 cnf(1273,plain, % 2.23/2.34 (P2(a1,a2,a1)+~P2(a2,a2,a2)), % 2.23/2.34 inference(scs_inference,[],[1257,237])). % 2.23/2.34 cnf(1289,plain, % 2.23/2.34 (P2(a1,a2,a1)+P2(a2,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[1273,6])). % 2.23/2.34 cnf(1320,plain, % 2.23/2.34 (~P3(a2,x13201,x13202)+~P3(a1,x13201,x13202)), % 2.23/2.34 inference(scs_inference,[],[2,3,15])). % 2.23/2.34 cnf(1336,plain, % 2.23/2.34 (P3(a1,x13361,a1)+~P3(a2,x13361,a2)), % 2.23/2.34 inference(scs_inference,[],[1320,5])). % 2.23/2.34 cnf(1429,plain, % 2.23/2.34 (P2(a1,a2,a2)+~P2(a2,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[4,285])). % 2.23/2.34 cnf(1445,plain, % 2.23/2.34 (P2(a1,a2,a2)+~P2(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1429,907])). % 2.23/2.34 cnf(1461,plain, % 2.23/2.34 (~P2(a1,a1,a1)+P2(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[1445,1193])). % 2.23/2.34 cnf(1477,plain, % 2.23/2.34 (~P3(a2,a2,x14771)+~P2(a1,a1,a1)+~P3(a1,a1,x14771)), % 2.23/2.34 inference(scs_inference,[],[1461,19])). % 2.23/2.34 cnf(1493,plain, % 2.23/2.34 (P2(a1,a2,a1)+~P3(a1,a1,x14931)+~P3(a2,a2,x14931)), % 2.23/2.34 inference(scs_inference,[],[1477,6])). % 2.23/2.34 cnf(1509,plain, % 2.23/2.34 (~P2(a1,a2,a2)+~P3(a2,a2,x15091)+~P3(a1,a1,x15091)), % 2.23/2.34 inference(scs_inference,[],[1493,221])). % 2.23/2.34 cnf(1525,plain, % 2.23/2.34 (P2(a2,a2,a2)+~P3(a1,a1,x15251)+~P3(a2,a2,x15251)), % 2.23/2.34 inference(scs_inference,[],[1509,8])). % 2.23/2.34 cnf(1541,plain, % 2.23/2.34 (~P3(a2,a2,x15411)+~P3(a1,a1,x15411)+P2(a2,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1525,237])). % 2.23/2.34 cnf(1557,plain, % 2.23/2.34 (~P2(a2,a2,a1)+~P3(a1,a1,x15571)+~P3(a2,a2,x15571)), % 2.23/2.34 inference(scs_inference,[],[1541,827])). % 2.23/2.34 cnf(1573,plain, % 2.23/2.34 (~P3(a2,a2,x15731)+~P2(a2,a1,a2)+~P3(a1,a1,x15731)), % 2.23/2.34 inference(scs_inference,[],[1557,843])). % 2.23/2.34 cnf(1589,plain, % 2.23/2.34 (P2(a1,a1,a2)+~P3(a1,a1,x15891)+~P3(a2,a2,x15891)), % 2.23/2.34 inference(scs_inference,[],[1573,8])). % 2.23/2.34 cnf(1605,plain, % 2.23/2.34 (P2(a1,a1,a2)+~P3(a1,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[1589,748])). % 2.23/2.34 cnf(1621,plain, % 2.23/2.34 (~P3(a1,a1,a2)+~P2(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[1605,365])). % 2.23/2.34 cnf(1637,plain, % 2.23/2.34 (~P2(a2,a2,a1)+P3(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1621,5])). % 2.23/2.34 cnf(1653,plain, % 2.23/2.34 (~P2(a2,a2,a1)+~P3(a1,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[1637,954])). % 2.23/2.34 cnf(1669,plain, % 2.23/2.34 (~P2(a2,a2,a1)+P3(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[1653,9])). % 2.23/2.34 cnf(1685,plain, % 2.23/2.34 (~P2(a2,a2,a1)+~P3(a2,a2,a2)), % 2.23/2.34 inference(scs_inference,[],[1669,524])). % 2.23/2.34 cnf(1701,plain, % 2.23/2.34 (P2(a1,a1,a2)+~P3(a2,a2,a2)), % 2.23/2.34 inference(scs_inference,[],[1685,859])). % 2.23/2.34 cnf(1717,plain, % 2.23/2.34 (P2(a2,a2,a2)+~P3(a2,a2,a2)), % 2.23/2.34 inference(scs_inference,[],[1701,445])). % 2.23/2.34 cnf(1733,plain, % 2.23/2.34 (~P3(a2,a2,a2)+~P2(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1717,891])). % 2.23/2.34 cnf(1749,plain, % 2.23/2.34 (~P2(a1,a1,a1)+P3(a2,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[1733,7])). % 2.23/2.34 cnf(1765,plain, % 2.23/2.34 (~P3(a1,a2,a1)+~P2(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1749,588])). % 2.23/2.34 cnf(1781,plain, % 2.23/2.34 (~P2(a1,a1,a1)+~P3(a2,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1765,1002])). % 2.23/2.34 cnf(1797,plain, % 2.23/2.34 (~P2(a2,a2,a1)+~P3(a2,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1781,349])). % 2.23/2.34 cnf(1813,plain, % 2.23/2.34 (~P3(a2,a1,a1)+P2(a2,a2,a2)), % 2.23/2.34 inference(scs_inference,[],[1797,4])). % 2.23/2.34 cnf(1829,plain, % 2.23/2.34 (P2(a1,a1,a2)+~P3(a2,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1813,875])). % 2.23/2.34 cnf(1845,plain, % 2.23/2.34 (~P3(a2,a1,a1)+~P2(a2,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[1829,1177])). % 2.23/2.34 cnf(1861,plain, % 2.23/2.34 (~P2(a1,a2,a2)+~P3(a2,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1845,1209])). % 2.23/2.34 cnf(1877,plain, % 2.23/2.34 (P2(a2,a1,a1)+~P3(a2,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1861,253])). % 2.23/2.34 cnf(1893,plain, % 2.23/2.34 (P2(a1,a2,a1)+~P3(a2,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1877,1257])). % 2.23/2.34 cnf(1909,plain, % 2.23/2.34 (P2(a1,a2,a1)+~P3(a2,a2,a2)), % 2.23/2.34 inference(scs_inference,[],[1893,540])). % 2.23/2.34 cnf(1925,plain, % 2.23/2.34 (~P3(a1,a2,a1)+P2(a1,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[1909,604])). % 2.23/2.34 cnf(1941,plain, % 2.23/2.34 (P3(a2,a1,a2)+P2(a1,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[1925,986])). % 2.23/2.34 cnf(1957,plain, % 2.23/2.34 (P2(a1,a2,a1)+~P3(a1,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[1941,1320])). % 2.23/2.34 cnf(1973,plain, % 2.23/2.34 (P2(a1,a2,a1)+P3(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[1957,5])). % 2.23/2.34 cnf(1989,plain, % 2.23/2.34 (P3(a1,a2,a2)+P2(a1,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[1973,1130])). % 2.23/2.34 cnf(2005,plain, % 2.23/2.34 (P3(a2,a2,a1)+P2(a1,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[1989,1034])). % 2.23/2.34 cnf(2021,plain, % 2.23/2.34 (~P2(a1,a1,a1)+P2(a1,a2,a1)+~P3(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[2005,1477])). % 2.23/2.34 cnf(2037,plain, % 2.23/2.34 (P2(a2,a2,a2)+P2(a1,a2,a1)+~P3(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[2021,429])). % 2.23/2.34 cnf(2053,plain, % 2.23/2.34 (P2(a1,a2,a1)+~P3(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[2037,1273])). % 2.23/2.34 cnf(2069,plain, % 2.23/2.34 (P2(a2,a1,a1)+~P3(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[2053,269])). % 2.23/2.34 cnf(2085,plain, % 2.23/2.34 (P2(a2,a2,a2)+~P3(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[2069,413])). % 2.23/2.34 cnf(2101,plain, % 2.23/2.34 (~P3(a1,a1,a1)+~P2(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[2085,221])). % 2.23/2.34 cnf(2117,plain, % 2.23/2.34 (~P3(a1,a1,a1)+~P2(a2,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[2101,843])). % 2.23/2.34 cnf(2133,plain, % 2.23/2.34 (~P2(a1,a1,a1)+~P3(a1,a1,a1)), % 2.23/2.34 inference(scs_inference,[],[2117,907])). % 2.23/2.34 cnf(2149,plain, % 2.23/2.34 (~P3(a1,a1,a1)+~P2(a1,a2,a2)), % 2.23/2.34 inference(scs_inference,[],[2133,237])). % 2.23/2.34 cnf(2165,plain, % 2.23/2.34 (~P3(a1,a1,a1)+P2(a1,a1,a2)), % 2.23/2.34 inference(scs_inference,[],[2149,6])). % 2.23/2.34 cnf(2181,plain, % 2.23/2.34 (P2(a1,a1,a2)+~P3(a2,a2,a1)), % 2.23/2.34 inference(scs_inference,[],[2165,652])). % 2.23/2.35 cnf(2197,plain, % 2.23/2.35 (~P3(a2,a2,a1)+~P2(a2,a2,a1)), % 2.23/2.35 inference(scs_inference,[],[2181,365])). % 2.23/2.35 cnf(2213,plain, % 2.23/2.35 (~P2(a2,a2,a1)+P3(a2,a1,a1)), % 2.23/2.35 inference(scs_inference,[],[2197,7])). % 2.23/2.35 cnf(2229,plain, % 2.23/2.35 (~P2(a2,a2,a1)+P3(a2,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2213,716])). % 2.23/2.35 cnf(2245,plain, % 2.23/2.35 (P2(a1,a1,a2)+P3(a2,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2229,859])). % 2.23/2.35 cnf(2261,plain, % 2.23/2.35 (P2(a2,a2,a2)+P3(a2,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2245,445])). % 2.23/2.35 cnf(2277,plain, % 2.23/2.35 (P3(a2,a2,a2)+~P2(a2,a1,a2)), % 2.23/2.35 inference(scs_inference,[],[2261,827])). % 2.23/2.35 cnf(2293,plain, % 2.23/2.35 (P2(a1,a2,a1)+P3(a2,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2277,1289])). % 2.23/2.35 cnf(2309,plain, % 2.23/2.35 (P2(a2,a1,a1)+P3(a2,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2293,269])). % 2.23/2.35 cnf(2325,plain, % 2.23/2.35 (~P2(a1,a2,a2)+P3(a2,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2309,1225])). % 2.23/2.35 cnf(2341,plain, % 2.23/2.35 (~P2(a1,a1,a1)+P3(a2,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2325,1445])). % 2.23/2.35 cnf(2357,plain, % 2.23/2.35 (~P2(a1,a1,a1)+P3(a1,a2,a1)), % 2.23/2.35 inference(scs_inference,[],[2341,1336])). % 2.23/2.35 cnf(2373,plain, % 2.23/2.35 (P3(a2,a1,a1)+~P2(a1,a1,a1)), % 2.23/2.35 inference(scs_inference,[],[2357,572])). % 2.23/2.35 cnf(2389,plain, % 2.23/2.35 (~P2(a1,a1,a1)+~P3(a1,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2373,1018])). % 2.23/2.35 cnf(2405,plain, % 2.23/2.35 (~P2(a2,a1,a2)+~P3(a1,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2389,493])). % 2.23/2.35 cnf(2421,plain, % 2.23/2.35 (~P2(a2,a2,a1)+~P3(a1,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2405,381])). % 2.23/2.35 cnf(2437,plain, % 2.23/2.35 (~P3(a1,a2,a2)+~P2(a1,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2421,1193])). % 2.23/2.35 cnf(2453,plain, % 2.23/2.35 (P2(a2,a1,a1)+~P3(a1,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2437,253])). % 2.23/2.35 cnf(2469,plain, % 2.23/2.35 (P2(a1,a1,a2)+~P3(a1,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2453,1241])). % 2.23/2.35 cnf(2485,plain, % 2.23/2.35 (P2(a2,a2,a2)+~P3(a1,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2469,445])). % 2.23/2.35 cnf(2501,plain, % 2.23/2.35 (P2(a1,a2,a1)+~P3(a1,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2485,1273])). % 2.23/2.35 cnf(2517,plain, % 2.23/2.35 (P3(a2,a1,a1)+P2(a1,a2,a1)), % 2.23/2.35 inference(scs_inference,[],[2501,556])). % 2.23/2.35 cnf(2533,plain, % 2.23/2.35 (P2(a1,a2,a1)+~P3(a2,a1,a2)), % 2.23/2.35 inference(scs_inference,[],[2517,524])). % 2.23/2.35 cnf(2549,plain, % 2.23/2.35 (P2(a2,a2,a2)+~P3(a2,a1,a2)), % 2.23/2.35 inference(scs_inference,[],[2533,301])). % 2.23/2.35 cnf(2565,plain, % 2.23/2.35 (P2(a1,a1,a2)+~P3(a2,a1,a2)), % 2.23/2.35 inference(scs_inference,[],[2549,875])). % 2.23/2.35 cnf(2581,plain, % 2.23/2.35 (~P3(a2,a1,a2)+~P2(a2,a1,a2)), % 2.23/2.35 inference(scs_inference,[],[2565,1177])). % 2.23/2.35 cnf(2597,plain, % 2.23/2.35 (~P2(a2,a2,a1)+~P3(a2,a1,a2)), % 2.23/2.35 inference(scs_inference,[],[2581,381])). % 2.23/2.35 cnf(2613,plain, % 2.23/2.35 (~P2(a1,a1,a1)+~P3(a2,a1,a2)), % 2.23/2.35 inference(scs_inference,[],[2597,1461])). % 2.23/2.35 cnf(2629,plain, % 2.23/2.35 (~P3(a2,a1,a2)+P2(a2,a1,a1)), % 2.23/2.35 inference(scs_inference,[],[2613,8])). % 2.23/2.35 cnf(2645,plain, % 2.23/2.35 (~P2(a1,a2,a2)+~P3(a2,a1,a2)), % 2.23/2.35 inference(scs_inference,[],[2629,1225])). % 2.23/2.35 cnf(2661,plain, % 2.23/2.35 (~P2(a1,a2,a2)+~P3(a2,a2,a1)), % 2.23/2.35 inference(scs_inference,[],[2645,970])). % 2.23/2.35 cnf(2677,plain, % 2.23/2.35 (~P2(a2,a1,a2)+~P3(a2,a2,a1)), % 2.23/2.35 inference(scs_inference,[],[2661,1429])). % 2.23/2.35 cnf(2693,plain, % 2.23/2.35 (P2(a1,a2,a1)+~P3(a2,a2,a1)), % 2.23/2.35 inference(scs_inference,[],[2677,1289])). % 2.23/2.35 cnf(2709,plain, % 2.23/2.35 (P2(a2,a2,a2)+~P3(a2,a2,a1)), % 2.23/2.35 inference(scs_inference,[],[2693,301])). % 2.23/2.35 cnf(2725,plain, % 2.23/2.35 (~P3(a2,a2,a1)+~P2(a1,a1,a1)), % 2.23/2.35 inference(scs_inference,[],[2709,891])). % 2.23/2.35 cnf(2741,plain, % 2.23/2.35 (~P2(a1,a1,a1)+~P2(a2,a2,a1)), % 2.23/2.35 inference(scs_inference,[],[2725,1669])). % 2.23/2.35 cnf(2757,plain, % 2.23/2.35 (~P2(a2,a2,a1)), % 2.23/2.35 inference(scs_inference,[],[2741,349])). % 2.23/2.35 cnf(2758,plain, % 2.23/2.35 (P2(a1,a1,a2)), % 2.23/2.35 inference(scs_inference,[],[2757,859])). % 2.23/2.35 cnf(2760,plain, % 2.23/2.35 (P2(a2,a2,a2)), % 2.23/2.35 inference(scs_inference,[],[2757,4])). % 2.23/2.35 cnf(2775,plain, % 2.23/2.35 (~P3(a1,a2,a1)), % 2.23/2.35 inference(scs_inference,[],[17,2,2757,4,237,1257,221,1177,16,5,7,572])). % 2.23/2.35 cnf(2793,plain, % 2.23/2.35 ($false), % 2.23/2.35 inference(scs_inference,[],[2760,2758,2775,9,652,1130,524,19]), % 2.23/2.35 ['proof']). % 2.23/2.35 % SZS output end Proof % 2.23/2.35 % Total time :1.690000s %------------------------------------------------------------------------------