%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PLA031-1.001 : TPTP v8.2.0. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n032.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 13:35:34 EDT 2024 % Result : Unsatisfiable 118.23s 118.32s % Output : CNFRefutation 118.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.09 % Problem : PLA031-1.001 : TPTP v8.2.0. Released v3.5.0. % 0.03/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.08/0.28 % Computer : n032.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 300 % 0.08/0.28 % DateTime : Tue Jun 18 17:14:53 EDT 2024 % 0.08/0.28 % CPUTime : % 0.13/0.45 start to proof:theBenchmark % 118.23/118.29 %------------------------------------------- % 118.23/118.29 % File :CSE---1.7 % 118.23/118.29 % Problem :theBenchmark % 118.23/118.29 % Transform :cnf % 118.23/118.29 % Format :tptp:raw % 118.23/118.29 % Command :java -jar mcs_scs.jar %d %s % 118.23/118.29 % 118.23/118.29 % Result :Theorem 117.800000s % 118.23/118.30 % Output :CNFRefutation 117.800000s % 118.23/118.30 %------------------------------------------- % 118.23/118.30 %------------------------------------------------------------------------------ % 118.23/118.30 % File : PLA031-1.001 : TPTP v8.2.0. Released v3.5.0. % 118.23/118.30 % Domain : Planning % 118.23/118.30 % Problem : Driver's log k=01 % 118.23/118.30 % Version : Especial. % 118.23/118.30 % English : A planning domain that involves driving trucks around % 118.23/118.30 % delivering packages between locations. The complication is % 118.23/118.30 % that the trucks require drivers who must walk between trucks % 118.23/118.30 % in order to drive them. The paths for walking and the roads % 118.23/118.30 % for driving form different maps on the locations. % 118.23/118.30 % Instances were semi-automatically translated from the basic % 118.23/118.30 % Strips instances used in the 2002 Planning Competition. % 118.23/118.30 % 118.23/118.31 % Refs : [LF03] Long & Fox (2003), The 3rd International Planning Compe % 118.23/118.31 % : [NV07a] Navarro (2007), Email to Geoff Sutcliffe % 118.23/118.31 % : [NV07b] Navarro & Voronkov (2007), Encoding Problems and Reaso % 118.23/118.31 % Source : [NV07a] % 118.23/118.31 % Names : driverlog01 [NV07a] % 118.23/118.31 % 118.23/118.31 % Status : Unsatisfiable % 118.23/118.31 % Rating : 0.00 v6.1.0, 0.12 v6.0.0, 0.00 v3.5.0 % 118.23/118.31 % Syntax : Number of clauses : 106 ( 84 unt; 0 nHn; 106 RR) % 118.23/118.31 % Number of literals : 138 ( 0 equ; 41 neg) % 118.23/118.31 % Maximal clause size : 3 ( 1 avg) % 118.23/118.31 % Maximal term depth : 1 ( 1 avg) % 118.23/118.31 % Number of predicates : 4 ( 4 usr; 0 prp; 2-6 aty) % 118.23/118.31 % Number of functors : 8 ( 8 usr; 8 con; 0-0 aty) % 118.23/118.31 % Number of variables : 118 ( 0 sgn) % 118.23/118.31 % SPC : CNF_UNS_EPR_NEQ_HRN % 118.23/118.31 % 118.23/118.31 % Comments : Only instances 1-4 are within reach of current provers. (2007) % 118.23/118.31 % : Translated from [LF03] using [NV07b] % 118.23/118.31 %------------------------------------------------------------------------------ % 118.23/118.31 cnf(load1,axiom, % 118.23/118.31 ( ~ s(L,O2,D1,D2,L,T2) % 118.23/118.31 | s(truck1,O2,D1,D2,L,T2) ) ). % 118.23/118.31 % 118.23/118.31 cnf(load2,axiom, % 118.23/118.31 ( s(L,O2,D1,D2,L,T2) % 118.23/118.31 | ~ s(truck1,O2,D1,D2,L,T2) ) ). % 118.23/118.31 % 118.23/118.31 cnf(load3,axiom, % 118.23/118.31 ( ~ s(L,O2,D1,D2,T1,L) % 118.23/118.31 | s(truck2,O2,D1,D2,T1,L) ) ). % 118.23/118.31 % 118.23/118.31 cnf(load4,axiom, % 118.23/118.31 ( s(L,O2,D1,D2,T1,L) % 118.23/118.31 | ~ s(truck2,O2,D1,D2,T1,L) ) ). % 118.23/118.31 % 118.23/118.31 cnf(load5,axiom, % 118.23/118.31 ( ~ s(O1,L,D1,D2,L,T2) % 118.23/118.31 | s(O1,truck1,D1,D2,L,T2) ) ). % 118.23/118.31 % 118.23/118.31 cnf(load6,axiom, % 118.23/118.31 ( s(O1,L,D1,D2,L,T2) % 118.23/118.31 | ~ s(O1,truck1,D1,D2,L,T2) ) ). % 118.23/118.31 % 118.23/118.31 cnf(load7,axiom, % 118.23/118.31 ( ~ s(O1,L,D1,D2,T1,L) % 118.23/118.31 | s(O1,truck2,D1,D2,T1,L) ) ). % 118.23/118.31 % 118.23/118.31 cnf(load8,axiom, % 118.23/118.31 ( s(O1,L,D1,D2,T1,L) % 118.23/118.31 | ~ s(O1,truck2,D1,D2,T1,L) ) ). % 118.23/118.31 % 118.23/118.31 cnf(board1,axiom, % 118.23/118.31 ( ~ s(O1,O2,L,D2,L,T2) % 118.23/118.31 | ~ neq(D2,truck1) % 118.23/118.31 | s(O1,O2,truck1,D2,L,T2) ) ). % 118.23/118.31 % 118.23/118.31 cnf(board2,axiom, % 118.23/118.31 ( s(O1,O2,L,D2,L,T2) % 118.23/118.31 | ~ s(O1,O2,truck1,D2,L,T2) ) ). % 118.23/118.31 % 118.23/118.31 cnf(board3,axiom, % 118.23/118.31 ( ~ s(O1,O2,L,D2,T1,L) % 118.23/118.31 | ~ neq(D2,truck2) % 118.23/118.31 | s(O1,O2,truck2,D2,T1,L) ) ). % 118.23/118.31 % 118.23/118.31 cnf(board4,axiom, % 118.23/118.31 ( s(O1,O2,L,D2,T1,L) % 118.23/118.31 | ~ s(O1,O2,truck2,D2,T1,L) ) ). % 118.23/118.31 % 118.23/118.31 cnf(board5,axiom, % 118.23/118.31 ( ~ s(O1,O2,D1,L,L,T2) % 118.23/118.31 | ~ neq(D1,truck1) % 118.23/118.31 | s(O1,O2,D1,truck1,L,T2) ) ). % 118.23/118.31 % 118.23/118.31 cnf(board6,axiom, % 118.23/118.31 ( s(O1,O2,D1,L,L,T2) % 118.23/118.31 | ~ s(O1,O2,D1,truck1,L,T2) ) ). % 118.23/118.31 % 118.23/118.31 cnf(board7,axiom, % 118.23/118.31 ( ~ s(O1,O2,D1,L,T1,L) % 118.23/118.31 | ~ neq(D1,truck2) % 118.23/118.31 | s(O1,O2,D1,truck2,T1,L) ) ). % 118.23/118.31 % 118.23/118.31 cnf(board8,axiom, % 118.23/118.31 ( s(O1,O2,D1,L,T1,L) % 118.23/118.31 | ~ s(O1,O2,D1,truck2,T1,L) ) ). % 118.23/118.31 % 118.23/118.31 cnf(drive1,axiom, % 118.23/118.31 ( ~ s(O1,O2,truck1,D2,S,T2) % 118.23/118.31 | ~ link(S,D) % 118.23/118.31 | s(O1,O2,truck1,D2,D,T2) ) ). % 118.23/118.31 % 118.23/118.31 cnf(drive2,axiom, % 118.23/118.31 ( ~ s(O1,O2,truck2,D2,T1,S) % 118.23/118.31 | ~ link(S,D) % 118.23/118.31 | s(O1,O2,truck2,D2,T1,D) ) ). % 118.23/118.31 % 118.23/118.31 cnf(drive3,axiom, % 118.23/118.31 ( ~ s(O1,O2,D1,truck1,S,T2) % 118.23/118.31 | ~ link(S,D) % 118.23/118.31 | s(O1,O2,D1,truck1,D,T2) ) ). % 118.23/118.31 % 118.23/118.31 cnf(drive4,axiom, % 118.23/118.31 ( ~ s(O1,O2,D1,truck2,T1,S) % 118.23/118.31 | ~ link(S,D) % 118.23/118.31 | s(O1,O2,D1,truck2,T1,D) ) ). % 118.23/118.31 % 118.23/118.31 cnf(walk1,axiom, % 118.23/118.31 ( ~ s(O1,O2,S,D2,T1,T2) % 118.23/118.31 | ~ path(S,D) % 118.23/118.31 | s(O1,O2,D,D2,T1,T2) ) ). % 118.23/118.31 % 118.23/118.31 cnf(walk2,axiom, % 118.23/118.31 ( ~ s(O1,O2,D1,S,T1,T2) % 118.23/118.31 | ~ path(S,D) % 118.23/118.31 | s(O1,O2,D1,D,T1,T2) ) ). % 118.23/118.31 % 118.23/118.31 cnf(neq1,axiom, % 118.23/118.31 ~ neq(truck1,truck1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq2,axiom, % 118.23/118.31 neq(truck1,truck2) ). % 118.23/118.31 % 118.23/118.31 cnf(neq3,axiom, % 118.23/118.31 neq(truck1,s0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq4,axiom, % 118.23/118.31 neq(truck1,s1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq5,axiom, % 118.23/118.31 neq(truck1,s2) ). % 118.23/118.31 % 118.23/118.31 cnf(neq6,axiom, % 118.23/118.31 neq(truck1,p1_0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq7,axiom, % 118.23/118.31 neq(truck1,p2_0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq8,axiom, % 118.23/118.31 neq(truck1,p2_1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq9,axiom, % 118.23/118.31 neq(truck2,truck1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq10,axiom, % 118.23/118.31 ~ neq(truck2,truck2) ). % 118.23/118.31 % 118.23/118.31 cnf(neq11,axiom, % 118.23/118.31 neq(truck2,s0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq12,axiom, % 118.23/118.31 neq(truck2,s1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq13,axiom, % 118.23/118.31 neq(truck2,s2) ). % 118.23/118.31 % 118.23/118.31 cnf(neq14,axiom, % 118.23/118.31 neq(truck2,p1_0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq15,axiom, % 118.23/118.31 neq(truck2,p2_0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq16,axiom, % 118.23/118.31 neq(truck2,p2_1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq17,axiom, % 118.23/118.31 neq(s0,truck1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq18,axiom, % 118.23/118.31 neq(s0,truck2) ). % 118.23/118.31 % 118.23/118.31 cnf(neq19,axiom, % 118.23/118.31 ~ neq(s0,s0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq20,axiom, % 118.23/118.31 neq(s0,s1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq21,axiom, % 118.23/118.31 neq(s0,s2) ). % 118.23/118.31 % 118.23/118.31 cnf(neq22,axiom, % 118.23/118.31 neq(s0,p1_0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq23,axiom, % 118.23/118.31 neq(s0,p2_0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq24,axiom, % 118.23/118.31 neq(s0,p2_1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq25,axiom, % 118.23/118.31 neq(s1,truck1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq26,axiom, % 118.23/118.31 neq(s1,truck2) ). % 118.23/118.31 % 118.23/118.31 cnf(neq27,axiom, % 118.23/118.31 neq(s1,s0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq28,axiom, % 118.23/118.31 ~ neq(s1,s1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq29,axiom, % 118.23/118.31 neq(s1,s2) ). % 118.23/118.31 % 118.23/118.31 cnf(neq30,axiom, % 118.23/118.31 neq(s1,p1_0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq31,axiom, % 118.23/118.31 neq(s1,p2_0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq32,axiom, % 118.23/118.31 neq(s1,p2_1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq33,axiom, % 118.23/118.31 neq(s2,truck1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq34,axiom, % 118.23/118.31 neq(s2,truck2) ). % 118.23/118.31 % 118.23/118.31 cnf(neq35,axiom, % 118.23/118.31 neq(s2,s0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq36,axiom, % 118.23/118.31 neq(s2,s1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq37,axiom, % 118.23/118.31 ~ neq(s2,s2) ). % 118.23/118.31 % 118.23/118.31 cnf(neq38,axiom, % 118.23/118.31 neq(s2,p1_0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq39,axiom, % 118.23/118.31 neq(s2,p2_0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq40,axiom, % 118.23/118.31 neq(s2,p2_1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq41,axiom, % 118.23/118.31 neq(p1_0,truck1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq42,axiom, % 118.23/118.31 neq(p1_0,truck2) ). % 118.23/118.31 % 118.23/118.31 cnf(neq43,axiom, % 118.23/118.31 neq(p1_0,s0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq44,axiom, % 118.23/118.31 neq(p1_0,s1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq45,axiom, % 118.23/118.31 neq(p1_0,s2) ). % 118.23/118.31 % 118.23/118.31 cnf(neq46,axiom, % 118.23/118.31 ~ neq(p1_0,p1_0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq47,axiom, % 118.23/118.31 neq(p1_0,p2_0) ). % 118.23/118.31 % 118.23/118.31 cnf(neq48,axiom, % 118.23/118.31 neq(p1_0,p2_1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq49,axiom, % 118.23/118.31 neq(p2_0,truck1) ). % 118.23/118.31 % 118.23/118.31 cnf(neq50,axiom, % 118.23/118.31 neq(p2_0,truck2) ). % 118.23/118.32 % 118.23/118.32 cnf(neq51,axiom, % 118.23/118.32 neq(p2_0,s0) ). % 118.23/118.32 % 118.23/118.32 cnf(neq52,axiom, % 118.23/118.32 neq(p2_0,s1) ). % 118.23/118.32 % 118.23/118.32 cnf(neq53,axiom, % 118.23/118.32 neq(p2_0,s2) ). % 118.23/118.32 % 118.23/118.32 cnf(neq54,axiom, % 118.23/118.32 neq(p2_0,p1_0) ). % 118.23/118.32 % 118.23/118.32 cnf(neq55,axiom, % 118.23/118.32 ~ neq(p2_0,p2_0) ). % 118.23/118.32 % 118.23/118.32 cnf(neq56,axiom, % 118.23/118.32 neq(p2_0,p2_1) ). % 118.23/118.32 % 118.23/118.32 cnf(neq57,axiom, % 118.23/118.32 neq(p2_1,truck1) ). % 118.23/118.32 % 118.23/118.32 cnf(neq58,axiom, % 118.23/118.32 neq(p2_1,truck2) ). % 118.23/118.32 % 118.23/118.32 cnf(neq59,axiom, % 118.23/118.32 neq(p2_1,s0) ). % 118.23/118.32 % 118.23/118.32 cnf(neq60,axiom, % 118.23/118.32 neq(p2_1,s1) ). % 118.23/118.32 % 118.23/118.32 cnf(neq61,axiom, % 118.23/118.32 neq(p2_1,s2) ). % 118.23/118.32 % 118.23/118.32 cnf(neq62,axiom, % 118.23/118.32 neq(p2_1,p1_0) ). % 118.23/118.32 % 118.23/118.32 cnf(neq63,axiom, % 118.23/118.32 neq(p2_1,p2_0) ). % 118.23/118.32 % 118.23/118.32 cnf(neq64,axiom, % 118.23/118.32 ~ neq(p2_1,p2_1) ). % 118.23/118.32 % 118.23/118.32 cnf(map1,axiom, % 118.23/118.32 path(s1,p1_0) ). % 118.23/118.32 % 118.23/118.32 cnf(map2,axiom, % 118.23/118.32 path(p1_0,s1) ). % 118.23/118.32 % 118.23/118.32 cnf(map3,axiom, % 118.23/118.32 path(s0,p1_0) ). % 118.23/118.32 % 118.23/118.32 cnf(map4,axiom, % 118.23/118.32 path(p1_0,s0) ). % 118.23/118.32 % 118.23/118.32 cnf(map5,axiom, % 118.23/118.32 path(s2,p2_0) ). % 118.23/118.32 % 118.23/118.32 cnf(map6,axiom, % 118.23/118.32 path(p2_0,s2) ). % 118.23/118.32 % 118.23/118.32 cnf(map7,axiom, % 118.23/118.32 path(s0,p2_0) ). % 118.23/118.32 % 118.23/118.32 cnf(map8,axiom, % 118.23/118.32 path(p2_0,s0) ). % 118.23/118.32 % 118.23/118.32 cnf(map9,axiom, % 118.23/118.32 path(s2,p2_1) ). % 118.23/118.32 % 118.23/118.32 cnf(map10,axiom, % 118.23/118.32 path(p2_1,s2) ). % 118.23/118.32 % 118.23/118.32 cnf(map11,axiom, % 118.23/118.32 path(s1,p2_1) ). % 118.23/118.32 % 118.23/118.32 cnf(map12,axiom, % 118.23/118.32 path(p2_1,s1) ). % 118.23/118.32 % 118.23/118.32 cnf(map13,axiom, % 118.23/118.32 link(s0,s1) ). % 118.23/118.32 % 118.23/118.32 cnf(map14,axiom, % 118.23/118.32 link(s1,s0) ). % 118.23/118.32 % 118.23/118.32 cnf(map15,axiom, % 118.23/118.32 link(s0,s2) ). % 118.23/118.32 % 118.23/118.32 cnf(map16,axiom, % 118.23/118.32 link(s2,s0) ). % 118.23/118.32 % 118.23/118.32 cnf(map17,axiom, % 118.23/118.32 link(s1,s2) ). % 118.23/118.32 % 118.23/118.32 cnf(map18,axiom, % 118.23/118.32 link(s2,s1) ). % 118.23/118.32 % 118.23/118.32 cnf(init,axiom, % 118.23/118.32 s(s2,s2,s0,s1,s0,s2) ). % 118.23/118.32 % 118.23/118.32 cnf(goal,negated_conjecture, % 118.23/118.32 ~ s(s2,s1,s2,s2,s2,s0) ). % 118.23/118.32 % 118.23/118.32 %------------------------------------------------------------------------------ % 118.23/118.32 %------------------------------------------- % 118.23/118.32 % Proof found % 118.23/118.32 % SZS status Theorem for theBenchmark % 118.23/118.32 % SZS output start Proof % 118.23/118.32 %ClaNum:106(EqnAxiom:0) % 118.23/118.32 %VarNum:256(SingletonVarNum:118) % 118.23/118.32 %MaxLitNum:3 % 118.23/118.32 %MaxfuncDepth:0 % 118.23/118.32 %SharedTerms:92 % 118.23/118.32 %goalClause: 84 % 118.23/118.32 %singleGoalClaCount:1 % 118.23/118.32 [1]P1(a1,a8) % 118.23/118.32 [2]P1(a1,a2) % 118.23/118.32 [3]P1(a1,a6) % 118.23/118.32 [4]P1(a1,a7) % 118.23/118.32 [5]P1(a1,a3) % 118.23/118.32 [6]P1(a1,a4) % 118.23/118.32 [7]P1(a1,a5) % 118.23/118.32 [8]P1(a8,a1) % 118.23/118.32 [9]P1(a8,a2) % 118.23/118.32 [10]P1(a8,a6) % 118.23/118.32 [11]P1(a8,a7) % 118.23/118.32 [12]P1(a8,a3) % 118.23/118.32 [13]P1(a8,a4) % 118.23/118.32 [14]P1(a8,a5) % 118.23/118.32 [15]P1(a2,a1) % 118.23/118.32 [16]P1(a2,a8) % 118.23/118.32 [17]P1(a2,a6) % 118.23/118.32 [18]P1(a2,a7) % 118.23/118.32 [19]P1(a2,a3) % 118.23/118.32 [20]P1(a2,a4) % 118.23/118.32 [21]P1(a2,a5) % 118.23/118.32 [22]P1(a6,a1) % 118.23/118.32 [23]P1(a6,a8) % 118.23/118.32 [24]P1(a6,a2) % 118.23/118.32 [25]P1(a6,a7) % 118.23/118.32 [26]P1(a6,a3) % 118.23/118.32 [27]P1(a6,a4) % 118.23/118.32 [28]P1(a6,a5) % 118.23/118.32 [29]P1(a7,a1) % 118.23/118.32 [30]P1(a7,a8) % 118.23/118.32 [31]P1(a7,a2) % 118.23/118.32 [32]P1(a7,a6) % 118.23/118.32 [33]P1(a7,a3) % 118.23/118.32 [34]P1(a7,a4) % 118.23/118.32 [35]P1(a7,a5) % 118.23/118.32 [36]P1(a3,a1) % 118.23/118.32 [37]P1(a3,a8) % 118.23/118.32 [38]P1(a3,a2) % 118.23/118.32 [39]P1(a3,a6) % 118.23/118.32 [40]P1(a3,a7) % 118.23/118.32 [41]P1(a3,a4) % 118.23/118.32 [42]P1(a3,a5) % 118.23/118.32 [43]P1(a4,a1) % 118.23/118.32 [44]P1(a4,a8) % 118.23/118.32 [45]P1(a4,a2) % 118.23/118.32 [46]P1(a4,a6) % 118.23/118.32 [47]P1(a4,a7) % 118.23/118.32 [48]P1(a4,a3) % 118.23/118.32 [49]P1(a4,a5) % 118.23/118.32 [50]P1(a5,a1) % 118.23/118.32 [51]P1(a5,a8) % 118.23/118.32 [52]P1(a5,a2) % 118.23/118.32 [53]P1(a5,a6) % 118.23/118.32 [54]P1(a5,a7) % 118.23/118.32 [55]P1(a5,a3) % 118.23/118.32 [56]P1(a5,a4) % 118.23/118.32 [57]P2(a2,a6) % 118.23/118.32 [58]P2(a2,a7) % 118.23/118.32 [59]P2(a6,a2) % 118.23/118.32 [60]P2(a6,a7) % 118.23/118.32 [61]P2(a7,a2) % 118.23/118.32 [62]P2(a7,a6) % 118.23/118.32 [63]P3(a2,a3) % 118.23/118.32 [64]P3(a2,a4) % 118.23/118.32 [65]P3(a6,a3) % 118.23/118.32 [66]P3(a6,a5) % 118.23/118.32 [67]P3(a7,a4) % 118.23/118.32 [68]P3(a7,a5) % 118.23/118.32 [69]P3(a3,a2) % 118.23/118.32 [70]P3(a3,a6) % 118.23/118.32 [71]P3(a4,a2) % 118.23/118.32 [72]P3(a4,a7) % 118.23/118.32 [73]P3(a5,a6) % 118.23/118.32 [74]P3(a5,a7) % 118.23/118.32 [75]P4(a7,a7,a2,a6,a2,a7) % 118.23/118.32 [76]~P1(a1,a1) % 118.23/118.32 [77]~P1(a8,a8) % 118.23/118.32 [78]~P1(a2,a2) % 118.23/118.32 [79]~P1(a6,a6) % 118.23/118.32 [80]~P1(a7,a7) % 118.23/118.32 [81]~P1(a3,a3) % 118.23/118.32 [82]~P1(a4,a4) % 118.23/118.32 [83]~P1(a5,a5) % 118.23/118.32 [84]~P4(a7,a6,a7,a7,a7,a2) % 118.23/118.32 [85]P4(x851,x852,x853,x854,x855,x854)+~P4(x851,x852,x853,a8,x855,x854) % 118.23/118.32 [86]P4(x861,x862,x863,x864,x864,x865)+~P4(x861,x862,x863,a1,x864,x865) % 118.23/118.32 [87]P4(x871,x872,x873,x874,x875,x873)+~P4(x871,x872,a8,x874,x875,x873) % 118.23/118.32 [88]P4(x881,x882,x883,x884,x883,x885)+~P4(x881,x882,a1,x884,x883,x885) % 118.23/118.32 [89]P4(x891,x892,x893,x894,x895,x892)+~P4(x891,a8,x893,x894,x895,x892) % 118.23/118.32 [90]P4(x901,x902,x903,x904,x902,x905)+~P4(x901,a1,x903,x904,x902,x905) % 118.23/118.32 [91]P4(x911,x912,x913,x914,x915,x911)+~P4(a8,x912,x913,x914,x915,x911) % 118.23/118.32 [92]P4(x921,x922,x923,x924,x921,x925)+~P4(a1,x922,x923,x924,x921,x925) % 118.23/118.32 [93]~P4(x931,x934,x932,x933,x934,x935)+P4(x931,a1,x932,x933,x934,x935) % 118.23/118.32 [94]~P4(x941,x945,x942,x943,x944,x945)+P4(x941,a8,x942,x943,x944,x945) % 118.23/118.32 [95]~P4(x954,x951,x952,x953,x954,x955)+P4(a1,x951,x952,x953,x954,x955) % 118.23/118.32 [96]~P4(x965,x961,x962,x963,x964,x965)+P4(a8,x961,x962,x963,x964,x965) % 118.23/118.32 [99]~P4(x991,x992,x993,x994,x994,x995)+P4(x991,x992,x993,a1,x994,x995)+~P1(x993,a1) % 118.23/118.32 [100]~P4(x1001,x1002,x1003,x1005,x1004,x1005)+P4(x1001,x1002,x1003,a8,x1004,x1005)+~P1(x1003,a8) % 118.23/118.32 [103]~P4(x1031,x1032,x1034,x1033,x1034,x1035)+P4(x1031,x1032,a1,x1033,x1034,x1035)+~P1(x1033,a1) % 118.23/118.32 [104]~P4(x1041,x1042,x1045,x1043,x1044,x1045)+P4(x1041,x1042,a8,x1043,x1044,x1045)+~P1(x1043,a8) % 118.23/118.32 [97]~P2(x976,x974)+~P4(x971,x972,x973,a1,x976,x975)+P4(x971,x972,x973,a1,x974,x975) % 118.23/118.32 [98]~P2(x986,x985)+~P4(x981,x982,x983,a8,x984,x986)+P4(x981,x982,x983,a8,x984,x985) % 118.23/118.32 [101]~P2(x1016,x1014)+~P4(x1011,x1012,a1,x1013,x1016,x1015)+P4(x1011,x1012,a1,x1013,x1014,x1015) % 118.23/118.32 [102]~P2(x1026,x1025)+~P4(x1021,x1022,a8,x1023,x1024,x1026)+P4(x1021,x1022,a8,x1023,x1024,x1025) % 118.23/118.32 [105]~P4(x1051,x1052,x1057,x1054,x1055,x1056)+P4(x1051,x1052,x1053,x1054,x1055,x1056)+~P3(x1057,x1053) % 118.23/118.32 [106]~P4(x1061,x1062,x1063,x1067,x1065,x1066)+P4(x1061,x1062,x1063,x1064,x1065,x1066)+~P3(x1067,x1064) % 118.23/118.32 %EqnAxiom % 118.23/118.32 % 118.23/118.32 %------------------------------------------- % 118.23/118.33 cnf(107,plain, % 118.23/118.33 (P4(a7,a7,a3,a6,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[63,75,105])). % 118.23/118.33 cnf(109,plain, % 118.23/118.33 (P4(a7,a7,a2,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[63,65,75,105,106])). % 118.23/118.33 cnf(111,plain, % 118.23/118.33 (P4(a7,a7,a1,a6,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[22,63,65,75,105,106,103])). % 118.23/118.33 cnf(113,plain, % 118.23/118.33 (~P4(x1131,x1132,a8,x1133,x1133,x1134)+P4(x1131,x1132,a8,a1,x1133,x1134)), % 118.23/118.33 inference(scs_inference,[],[8,22,63,65,75,105,106,103,99])). % 118.23/118.33 cnf(117,plain, % 118.23/118.33 (P4(x1171,x1172,a8,a1,x1171,x1173)+~P4(a1,x1172,a8,x1171,x1171,x1173)), % 118.23/118.33 inference(scs_inference,[],[8,22,63,65,75,105,106,103,99,86,92])). % 118.23/118.33 cnf(119,plain, % 118.23/118.33 (P4(a1,x1191,x1192,a1,x1193,x1192)+~P4(a1,x1191,a8,x1193,x1193,x1192)), % 118.23/118.33 inference(scs_inference,[],[8,22,63,65,75,105,106,103,99,86,92,87])). % 118.23/118.33 cnf(121,plain, % 118.23/118.33 (P4(a1,x1211,a8,a1,x1212,x1211)+~P4(a1,a8,a8,x1212,x1212,x1211)), % 118.23/118.33 inference(scs_inference,[],[8,22,63,65,75,105,106,103,99,86,92,87,89])). % 118.23/118.33 cnf(128,plain, % 118.23/118.33 (P4(a7,a7,a4,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[109,64,105])). % 118.23/118.33 cnf(130,plain, % 118.23/118.33 (P4(a7,a7,a1,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[109,36,64,105,103])). % 118.23/118.33 cnf(132,plain, % 118.23/118.33 (P4(a7,a7,a3,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[107,109,36,64,66,105,103,106])). % 118.23/118.33 cnf(134,plain, % 118.23/118.33 (~P4(x1341,x1342,a1,x1343,x1344,x1343)+P4(x1341,x1342,a1,a8,x1344,x1343)), % 118.23/118.33 inference(scs_inference,[],[107,109,1,36,64,66,105,103,106,100])). % 118.23/118.33 cnf(140,plain, % 118.23/118.33 (P4(a8,x1401,x1402,a8,x1402,x1403)+~P4(a8,x1401,a1,x1403,x1402,x1403)), % 118.23/118.33 inference(scs_inference,[],[107,109,1,36,64,66,105,103,106,100,85,91,88])). % 118.23/118.33 cnf(142,plain, % 118.23/118.33 (P4(a8,x1421,a1,a8,x1421,x1422)+~P4(a8,a1,a1,x1422,x1421,x1422)), % 118.23/118.33 inference(scs_inference,[],[107,109,1,36,64,66,105,103,106,100,85,91,88,90])). % 118.23/118.33 cnf(149,plain, % 118.23/118.33 (P4(a7,a7,a2,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[132,69,105])). % 118.23/118.33 cnf(151,plain, % 118.23/118.33 (P4(a7,a7,a4,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[128,132,69,105,106])). % 118.23/118.33 cnf(153,plain, % 118.23/118.33 (P4(a7,a7,a1,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[128,132,50,69,105,106,103])). % 118.23/118.33 cnf(157,plain, % 118.23/118.33 (~P4(x1571,x1572,x1573,a1,x1574,x1573)+P4(x1571,x1572,a8,a1,x1574,x1573)), % 118.23/118.33 inference(scs_inference,[],[128,132,1,43,50,69,105,106,103,99,104])). % 118.23/118.33 cnf(162,plain, % 118.23/118.33 (P4(a7,a7,a6,a6,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[107,70,105])). % 118.23/118.33 cnf(164,plain, % 118.23/118.33 (P4(a7,a7,a4,a6,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[107,128,70,105,106])). % 118.23/118.33 cnf(166,plain, % 118.23/118.33 (~P4(x1661,x1662,x1663,a6,x1664,x1663)+P4(x1661,x1662,a8,a6,x1664,x1663)), % 118.23/118.33 inference(scs_inference,[],[107,128,23,70,105,106,104])). % 118.23/118.33 cnf(193,plain, % 118.23/118.33 (P4(a7,a7,a2,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[151,71,105])). % 118.23/118.33 cnf(197,plain, % 118.23/118.33 (~P4(a7,a6,a7,a4,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[84,151,71,72,15,105,103,106])). % 118.23/118.33 cnf(199,plain, % 118.23/118.33 (P4(a7,a7,a2,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[84,151,71,72,15,105,103,106,99])). % 118.23/118.33 cnf(225,plain, % 118.23/118.33 (~P4(a7,a6,a5,a7,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[84,74,105])). % 118.23/118.33 cnf(227,plain, % 118.23/118.33 (P4(a7,a7,a2,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[84,149,74,105,106])). % 118.23/118.33 cnf(229,plain, % 118.23/118.33 (~P4(x2291,x2292,x2293,a3,x2294,x2293)+P4(x2291,x2292,a8,a3,x2294,x2293)), % 118.23/118.33 inference(scs_inference,[],[84,149,37,74,105,106,104])). % 118.23/118.33 cnf(233,plain, % 118.23/118.33 (P4(a7,a7,a1,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[84,149,37,74,16,29,105,106,104,100,103])). % 118.23/118.33 cnf(260,plain, % 118.23/118.33 (P4(a7,a7,a3,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[193,63,105])). % 118.23/118.33 cnf(264,plain, % 118.23/118.33 (P4(a7,a7,a3,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[193,233,1,36,63,105,100,99])). % 118.23/118.33 cnf(266,plain, % 118.23/118.33 (P4(a7,a7,a2,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[193,227,233,1,36,67,63,105,100,99,106])). % 118.23/118.33 cnf(268,plain, % 118.23/118.33 (~P4(x2681,x2682,x2683,a4,x2684,x2683)+P4(x2681,x2682,a8,a4,x2684,x2683)), % 118.23/118.33 inference(scs_inference,[],[193,227,233,1,36,44,67,63,105,100,99,106,104])). % 118.23/118.33 cnf(270,plain, % 118.23/118.33 (P4(a7,a7,a1,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[193,227,233,1,36,43,44,67,63,105,100,99,106,104,103])). % 118.23/118.33 cnf(293,plain, % 118.23/118.33 (P4(a7,a7,a4,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[266,64,105])). % 118.23/118.33 cnf(295,plain, % 118.23/118.33 (P4(a7,a7,a3,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[260,266,64,105,106])). % 118.23/118.33 cnf(297,plain, % 118.23/118.33 (~P4(x2971,x2972,x2973,a5,x2974,x2973)+P4(x2971,x2972,a8,a5,x2974,x2973)), % 118.23/118.33 inference(scs_inference,[],[260,266,51,64,105,106,104])). % 118.23/118.33 cnf(325,plain, % 118.23/118.33 (P4(a7,a7,a5,a6,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[162,66,105])). % 118.23/118.33 cnf(327,plain, % 118.23/118.33 (P4(a7,a7,a6,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[162,65,66,105,106])). % 118.23/118.33 cnf(329,plain, % 118.23/118.33 (~P4(x3291,x3292,x3293,a2,x3294,x3293)+P4(x3291,x3292,a8,a2,x3294,x3293)), % 118.23/118.33 inference(scs_inference,[],[162,16,65,66,105,106,104])). % 118.23/118.33 cnf(333,plain, % 118.23/118.33 (P4(x3331,x3332,a8,a2,a2,x3331)+~P4(a8,x3332,x3331,a2,a2,x3331)), % 118.23/118.33 inference(scs_inference,[],[162,8,16,65,66,105,106,104,99,91])). % 118.23/118.33 cnf(356,plain, % 118.23/118.33 (P4(a7,a7,a7,a6,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[164,72,105])). % 118.23/118.33 cnf(358,plain, % 118.23/118.33 (P4(a7,a7,a8,a6,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[164,72,23,105,104])). % 118.23/118.33 cnf(360,plain, % 118.23/118.33 (P4(a7,a7,a4,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[164,293,72,23,105,104,106])). % 118.23/118.33 cnf(362,plain, % 118.23/118.33 (~P4(x3621,x3622,a7,x3623,x3624,x3623)+P4(x3621,x3622,a7,a8,x3624,x3623)), % 118.23/118.33 inference(scs_inference,[],[164,293,30,72,23,105,104,106,100])). % 118.23/118.33 cnf(373,plain, % 118.23/118.33 (P4(a7,a7,a3,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[327,65,105])). % 118.23/118.33 cnf(377,plain, % 118.23/118.33 (P4(a7,a7,a4,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[327,360,68,44,65,105,100,106])). % 118.23/118.33 cnf(379,plain, % 118.23/118.33 (~P4(x3791,x3792,a6,x3793,x3793,x3794)+P4(x3791,x3792,a6,a1,x3793,x3794)), % 118.23/118.33 inference(scs_inference,[],[327,360,22,68,44,65,105,100,106,99])). % 118.23/118.33 cnf(394,plain, % 118.23/118.33 (P4(a7,a7,a7,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[356,327,66,105,106])). % 118.23/118.33 cnf(396,plain, % 118.23/118.33 (P4(a7,a7,a8,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[356,327,51,66,105,106,104])). % 118.23/118.33 cnf(404,plain, % 118.23/118.33 (P4(a8,x4041,a3,a8,x4042,x4041)+~P4(a8,a8,a3,x4041,x4042,x4041)), % 118.23/118.33 inference(scs_inference,[],[356,327,37,51,66,105,106,104,100,85,91,89])). % 118.23/118.33 cnf(411,plain, % 118.23/118.33 (P4(a7,a7,a5,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[394,68,105])). % 118.23/118.33 cnf(413,plain, % 118.23/118.33 (P4(a7,a7,a7,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[394,68,74,105,106])). % 118.23/118.33 cnf(419,plain, % 118.23/118.33 (~P4(x4191,x4192,a5,x4193,x4193,x4194)+P4(x4191,x4192,a5,a1,x4193,x4194)), % 118.23/118.33 inference(scs_inference,[],[394,50,30,68,74,105,106,104,100,99])). % 118.23/118.33 cnf(431,plain, % 118.23/118.33 (P4(a7,a7,a5,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[413,68,105])). % 118.23/118.33 cnf(433,plain, % 118.23/118.33 (P4(a7,a7,a5,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[413,51,68,105,100])). % 118.23/118.33 cnf(435,plain, % 118.23/118.33 (P4(a7,a7,a7,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[413,51,67,68,105,100,106])). % 118.23/118.33 cnf(437,plain, % 118.23/118.33 (P4(a7,a7,a8,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[413,44,51,67,68,105,100,106,104])). % 118.23/118.33 cnf(441,plain, % 118.23/118.33 (~P4(x4411,x4412,a7,x4413,x4413,x4411)+P4(a8,x4412,a7,a1,x4413,x4411)), % 118.23/118.33 inference(scs_inference,[],[413,29,44,51,67,68,105,100,106,104,99,96])). % 118.23/118.33 cnf(443,plain, % 118.23/118.33 (~P4(a8,x4431,a7,x4431,x4431,x4432)+P4(a8,a1,a7,a1,x4431,x4432)), % 118.23/118.33 inference(scs_inference,[],[413,29,44,51,67,68,105,100,106,104,99,96,93])). % 118.23/118.33 cnf(449,plain, % 118.23/118.33 (P4(a7,a7,a6,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[295,70,105])). % 118.23/118.33 cnf(451,plain, % 118.23/118.33 (P4(a7,a7,a7,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[435,295,71,70,105,106])). % 118.23/118.33 cnf(453,plain, % 118.23/118.33 (P4(a7,a7,a8,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[435,295,16,71,70,105,106,104])). % 118.23/118.33 cnf(455,plain, % 118.23/118.33 (P4(a7,a7,a7,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[435,295,29,16,71,70,105,106,104,99])). % 118.23/118.33 cnf(457,plain, % 118.23/118.33 (~P4(x4571,x4572,a6,x4573,x4574,x4573)+P4(x4571,x4572,a6,a8,x4574,x4573)), % 118.23/118.33 inference(scs_inference,[],[435,295,29,16,71,70,23,105,106,104,99,100])). % 118.23/118.33 cnf(466,plain, % 118.23/118.33 (P4(a7,a7,a6,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[431,73,105])). % 118.23/118.33 cnf(468,plain, % 118.23/118.33 (P4(a7,a7,a8,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[431,455,1,73,105,104])). % 118.23/118.33 cnf(470,plain, % 118.23/118.33 (P4(a7,a7,a6,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[431,455,1,73,23,105,104,100])). % 118.23/118.33 cnf(472,plain, % 118.23/118.33 (P4(a7,a7,a7,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[431,451,455,1,73,63,23,105,104,100,106])). % 118.23/118.33 cnf(474,plain, % 118.23/118.33 (P4(a7,a8,a8,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[453,113,94])). % 118.23/118.33 cnf(475,plain, % 118.23/118.33 (P4(a7,a8,a7,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[474,87])). % 118.23/118.33 cnf(477,plain, % 118.23/118.33 (P4(a7,a8,a8,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[474,87,86])). % 118.23/118.33 cnf(481,plain, % 118.23/118.33 (P4(a7,a7,a8,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[466,472,474,37,65,87,86,105,104])). % 118.23/118.33 cnf(483,plain, % 118.23/118.33 (P4(a7,a7,a3,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[466,472,474,37,65,87,86,105,104,100])). % 118.23/118.33 cnf(485,plain, % 118.23/118.33 (P4(a7,a7,a6,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[466,472,449,474,37,71,65,87,86,105,104,100,106])). % 118.23/118.33 cnf(487,plain, % 118.23/118.33 (P4(a7,a7,a6,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[466,472,449,474,22,37,71,65,87,86,105,104,100,106,99])). % 118.23/118.33 cnf(489,plain, % 118.23/118.33 (P4(a7,a8,a7,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[477,87])). % 118.23/118.33 cnf(491,plain, % 118.23/118.33 (P4(a7,a7,a5,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[477,485,66,87,105])). % 118.23/118.33 cnf(493,plain, % 118.23/118.33 (P4(a7,a7,a5,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[477,485,50,66,87,105,99])). % 118.23/118.33 cnf(495,plain, % 118.23/118.33 (P4(a7,a8,a8,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[477,485,50,63,66,87,105,99,106])). % 118.23/118.33 cnf(497,plain, % 118.23/118.33 (P4(a7,a8,a7,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[495,87])). % 118.23/118.33 cnf(499,plain, % 118.23/118.33 (P4(a7,a8,a8,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[477,495,64,87,106])). % 118.23/118.33 cnf(501,plain, % 118.23/118.33 (P4(a7,a8,a7,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[499,87])). % 118.23/118.33 cnf(503,plain, % 118.23/118.33 (P4(a7,a8,a8,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[499,72,87,106])). % 118.23/118.33 cnf(505,plain, % 118.23/118.33 (P4(a7,a8,a7,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[503,87])). % 118.23/118.33 cnf(508,plain, % 118.23/118.33 (P4(a7,a8,a1,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[233,134,94])). % 118.23/118.33 cnf(509,plain, % 118.23/118.33 (P4(a7,a8,a1,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[508,85])). % 118.23/118.33 cnf(511,plain, % 118.23/118.33 (P4(a7,a8,a2,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[508,85,88])). % 118.23/118.33 cnf(513,plain, % 118.23/118.33 (P4(a7,a8,a2,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[511,85])). % 118.23/118.33 cnf(515,plain, % 118.23/118.33 (P4(a7,a8,a3,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[511,63,85,105])). % 118.23/118.33 cnf(520,plain, % 118.23/118.33 (P4(a7,a8,a4,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[513,515,64,85,105])). % 118.23/118.33 cnf(522,plain, % 118.23/118.33 (P4(a8,a8,a2,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[509,140,96])). % 118.23/118.33 cnf(523,plain, % 118.23/118.33 (P4(a8,a8,a2,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[522,85])). % 118.23/118.33 cnf(525,plain, % 118.23/118.33 (P4(a8,a7,a2,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[522,85,89])). % 118.23/118.33 cnf(527,plain, % 118.23/118.33 (P4(a8,a8,a1,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[522,8,85,89,103])). % 118.23/118.33 cnf(529,plain, % 118.23/118.33 (P4(a8,a8,a3,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[522,8,63,85,89,103,105])). % 118.23/118.33 cnf(531,plain, % 118.23/118.33 (P4(a7,a8,a4,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[520,522,8,44,63,85,89,103,105,100])). % 118.23/118.33 cnf(534,plain, % 118.23/118.33 (P4(a8,a8,a3,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[529,85])). % 118.23/118.33 cnf(538,plain, % 118.23/118.33 (P4(a8,a8,a1,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[523,529,29,85,89,103])). % 118.23/118.33 cnf(540,plain, % 118.23/118.33 (P4(a8,a8,a4,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[523,529,29,64,85,89,103,105])). % 118.23/118.33 cnf(542,plain, % 118.23/118.33 (P4(a8,a7,a3,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[523,529,29,64,85,89,103,105,404])). % 118.23/118.33 cnf(549,plain, % 118.23/118.33 (P4(a8,a8,a4,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[540,542,44,85,89,100])). % 118.23/118.33 cnf(551,plain, % 118.23/118.33 (P4(a8,a7,a8,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[451,157,441])). % 118.23/118.33 cnf(552,plain, % 118.23/118.33 (P4(a8,a7,a7,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[551,87])). % 118.23/118.33 cnf(554,plain, % 118.23/118.33 (P4(a8,a7,a8,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[551,87,86])). % 118.23/118.33 cnf(556,plain, % 118.23/118.33 (P4(a8,a7,a4,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[549,551,87,86,89])). % 118.23/118.33 cnf(559,plain, % 118.23/118.33 (P4(a8,a7,a7,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[554,87])). % 118.23/118.33 cnf(561,plain, % 118.23/118.33 (P4(a8,a7,a1,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[554,538,87,89])). % 118.23/118.33 cnf(563,plain, % 118.23/118.33 (P4(a8,a7,a8,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[554,538,63,87,89,106])). % 118.23/118.33 cnf(565,plain, % 118.23/118.33 (P4(a7,a8,a8,a6,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[356,166,94])). % 118.23/118.33 cnf(566,plain, % 118.23/118.33 (P4(a8,a7,a7,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[563,87])). % 118.23/118.33 cnf(568,plain, % 118.23/118.33 (P4(a8,a7,a1,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[563,527,87,89])). % 118.23/118.33 cnf(572,plain, % 118.23/118.33 (P4(a8,a7,a8,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[554,563,435,527,68,64,87,89,105,106])). % 118.23/118.33 cnf(575,plain, % 118.23/118.33 (P4(a8,a7,a7,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[572,87])). % 118.23/118.33 cnf(583,plain, % 118.23/118.33 (P4(a7,a8,a7,a6,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[565,87])). % 118.23/118.33 cnf(603,plain, % 118.23/118.33 (P4(a7,a7,a8,a3,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[472,61,229,102])). % 118.23/118.33 cnf(604,plain, % 118.23/118.33 (P4(a7,a7,a2,a3,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[603,87])). % 118.23/118.33 cnf(617,plain, % 118.23/118.33 (P4(a7,a7,a8,a4,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[435,62,268,102])). % 118.23/118.33 cnf(618,plain, % 118.23/118.33 (P4(a7,a7,a6,a4,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[617,87])). % 118.23/118.33 cnf(625,plain, % 118.23/118.33 (P4(a7,a7,a6,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[132,70,105])). % 118.23/118.33 cnf(630,plain, % 118.23/118.33 (P4(a7,a8,a8,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[394,297,94])). % 118.23/118.33 cnf(631,plain, % 118.23/118.33 (P4(a7,a8,a7,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[630,87])). % 118.23/118.33 cnf(645,plain, % 118.23/118.33 (P4(a7,a7,a8,a2,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[451,61,329,102])). % 118.23/118.33 cnf(646,plain, % 118.23/118.33 (P4(a7,a7,a2,a2,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[645,87])). % 118.23/118.33 cnf(649,plain, % 118.23/118.33 (P4(a7,a7,a8,a2,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[559,62,333,102])). % 118.23/118.33 cnf(650,plain, % 118.23/118.33 (P4(a7,a7,a6,a2,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[649,87])). % 118.23/118.33 cnf(661,plain, % 118.23/118.33 (P4(a8,a7,a7,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[413,362,96])). % 118.23/118.33 cnf(665,plain, % 118.23/118.33 (P4(a7,a8,a6,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[485,379,94])). % 118.23/118.33 cnf(666,plain, % 118.23/118.33 (P4(a7,a8,a6,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[665,86])). % 118.23/118.33 cnf(669,plain, % 118.23/118.33 (P4(a7,a8,a3,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[666,65,105])). % 118.23/118.33 cnf(671,plain, % 118.23/118.33 (P4(a7,a8,a6,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[666,65,63,105,106])). % 118.23/118.33 cnf(675,plain, % 118.23/118.33 (P4(a7,a8,a3,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[666,669,36,66,105,99])). % 118.23/118.33 cnf(677,plain, % 118.23/118.33 (P4(a7,a8,a6,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[666,669,36,66,64,105,99,106])). % 118.23/118.33 cnf(680,plain, % 118.23/118.33 (P4(a7,a8,a6,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[677,72,106])). % 118.23/118.33 cnf(683,plain, % 118.23/118.33 (P4(a7,a8,a6,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[680,23,100])). % 118.23/118.33 cnf(685,plain, % 118.23/118.33 (~P4(a7,a6,a7,a5,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[84,680,74,23,100,106])). % 118.23/118.33 cnf(687,plain, % 118.23/118.33 (~P4(a7,a6,a7,a6,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[685,66,106])). % 118.23/118.33 cnf(690,plain, % 118.23/118.33 (~P4(a7,a6,a7,a3,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[687,70,106])). % 118.23/118.33 cnf(693,plain, % 118.23/118.33 (~P4(a7,a6,a7,a2,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[690,63,106])). % 118.23/118.33 cnf(696,plain, % 118.23/118.33 (P4(a7,a8,a5,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[491,419,94])). % 118.23/118.33 cnf(703,plain, % 118.23/118.33 (~P4(a8,a7,a1,a7,a7,x7031)+P4(a8,a1,a7,a1,a7,x7031)), % 118.23/118.33 inference(scs_inference,[],[443,88])). % 118.23/118.33 cnf(706,plain, % 118.23/118.33 (P4(a8,a7,a6,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[466,457,96])). % 118.23/118.33 cnf(715,plain, % 118.23/118.33 (P4(a7,a8,a4,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[475,67,105])). % 118.23/118.33 cnf(717,plain, % 118.23/118.33 (P4(a7,a8,a4,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[475,67,105,86])). % 118.23/118.33 cnf(720,plain, % 118.23/118.33 (P4(a7,a8,a2,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[717,71,105])). % 118.23/118.33 cnf(723,plain, % 118.23/118.33 (P4(a7,a8,a1,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[720,15,103])). % 118.23/118.33 cnf(739,plain, % 118.23/118.33 (P4(a7,a8,a4,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[497,67,105])). % 118.23/118.33 cnf(742,plain, % 118.23/118.33 (P4(a7,a8,a5,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[497,68,105])). % 118.23/118.33 cnf(747,plain, % 118.23/118.33 (P4(a7,a8,a4,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[501,67,105])). % 118.23/118.33 cnf(750,plain, % 118.23/118.33 (P4(a7,a8,a5,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[501,68,105])). % 118.23/118.33 cnf(755,plain, % 118.23/118.33 (P4(a7,a8,a5,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[505,68,105])). % 118.23/118.33 cnf(760,plain, % 118.23/118.33 (P4(a7,a8,a5,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[755,51,100])). % 118.23/118.33 cnf(775,plain, % 118.23/118.33 (P4(a8,a8,a6,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[529,70,105])). % 118.23/118.33 cnf(785,plain, % 118.23/118.33 (P4(a8,a8,a7,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[540,72,105])). % 118.23/118.33 cnf(788,plain, % 118.23/118.33 (P4(a8,a8,a8,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[785,30,104])). % 118.23/118.33 cnf(790,plain, % 118.23/118.33 (P4(a8,a8,a5,a7,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[785,30,68,104,105])). % 118.23/118.33 cnf(792,plain, % 118.23/118.33 (P4(a8,a8,a7,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[785,30,68,104,105,100])). % 118.23/118.33 cnf(797,plain, % 118.23/118.33 (P4(a8,a8,a5,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[790,51,100])). % 118.23/118.33 cnf(799,plain, % 118.23/118.33 (P4(a8,a7,a5,a8,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[790,51,100,89])). % 118.23/118.33 cnf(808,plain, % 118.23/118.33 (P4(a8,a7,a4,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[552,67,105])). % 118.23/118.33 cnf(810,plain, % 118.23/118.33 (P4(a8,a7,a4,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[552,67,105,86])). % 118.23/118.33 cnf(813,plain, % 118.23/118.33 (P4(a8,a7,a2,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[810,71,105])). % 118.23/118.33 cnf(816,plain, % 118.23/118.33 (P4(a8,a7,a1,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[813,15,103])). % 118.23/118.33 cnf(818,plain, % 118.23/118.33 (P4(a8,a7,a5,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[552,813,15,68,103,105])). % 118.23/118.33 cnf(820,plain, % 118.23/118.33 (P4(a8,a7,a2,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[552,813,15,68,103,105,99])). % 118.23/118.33 cnf(822,plain, % 118.23/118.33 (P4(a8,a7,a5,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[552,813,15,68,103,105,99,86])). % 118.23/118.33 cnf(825,plain, % 118.23/118.33 (P4(a8,a7,a6,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[822,73,105])). % 118.23/118.33 cnf(835,plain, % 118.23/118.33 (P4(a8,a7,a4,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[566,67,105])). % 118.23/118.33 cnf(838,plain, % 118.23/118.33 (P4(a8,a7,a5,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[566,68,105])). % 118.23/118.33 cnf(845,plain, % 118.23/118.33 (P4(a8,a7,a4,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[575,67,105])). % 118.23/118.33 cnf(848,plain, % 118.23/118.33 (P4(a8,a7,a5,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[575,68,105])). % 118.23/118.33 cnf(854,plain, % 118.23/118.33 (P4(a7,a8,a4,a6,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[583,67,105])). % 118.23/118.33 cnf(860,plain, % 118.23/118.33 (P4(a8,a1,a8,a1,a7,a7)+~P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[703,157])). % 118.23/118.33 cnf(862,plain, % 118.23/118.33 (P4(a7,a7,a1,a3,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[604,36,103])). % 118.23/118.33 cnf(864,plain, % 118.23/118.33 (P4(a7,a7,a4,a3,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[604,36,64,103,105])). % 118.23/118.33 cnf(867,plain, % 118.23/118.33 (P4(a7,a7,a3,a3,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[604,63,105])). % 118.23/118.33 cnf(872,plain, % 118.23/118.33 (P4(a7,a7,a3,a4,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[618,65,105])). % 118.23/118.33 cnf(875,plain, % 118.23/118.33 (P4(a7,a7,a5,a4,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[618,66,105])). % 118.23/118.33 cnf(881,plain, % 118.23/118.33 (P4(a7,a8,a4,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[631,67,105])). % 118.23/118.33 cnf(884,plain, % 118.23/118.33 (P4(a7,a8,a5,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[631,68,105])). % 118.23/118.33 cnf(888,plain, % 118.23/118.33 (P4(a7,a7,a8,a1,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[645,8,99])). % 118.23/118.33 cnf(894,plain, % 118.23/118.33 (P4(a7,a7,a1,a2,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[646,15,103])). % 118.23/118.33 cnf(896,plain, % 118.23/118.33 (P4(a7,a7,a2,a8,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[646,15,16,103,100])). % 118.23/118.33 cnf(898,plain, % 118.23/118.33 (P4(a7,a7,a4,a2,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[646,15,16,64,103,100,105])). % 118.23/118.33 cnf(901,plain, % 118.23/118.33 (P4(a7,a7,a4,a8,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[898,44,100])). % 118.23/118.33 cnf(903,plain, % 118.23/118.33 (P4(a7,a7,a3,a2,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[646,898,44,63,100,105])). % 118.23/118.33 cnf(906,plain, % 118.23/118.33 (P4(a7,a7,a3,a1,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[903,36,99])). % 118.23/118.33 cnf(910,plain, % 118.23/118.33 (P4(a7,a7,a8,a1,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[649,8,99])). % 118.23/118.33 cnf(912,plain, % 118.23/118.33 (P4(a7,a7,a6,a1,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[649,8,99,87])). % 118.23/118.33 cnf(916,plain, % 118.23/118.33 (P4(a7,a7,a3,a2,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[650,65,105])). % 118.23/118.33 cnf(919,plain, % 118.23/118.33 (P4(a7,a7,a3,a1,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[916,36,99])). % 118.23/118.33 cnf(921,plain, % 118.23/118.33 (P4(a7,a7,a5,a2,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[650,916,36,66,99,105])). % 118.23/118.33 cnf(929,plain, % 118.23/118.33 (P4(a7,a8,a3,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[671,65,105])). % 118.23/118.33 cnf(953,plain, % 118.23/118.33 (P4(a7,a8,a2,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[739,71,105])). % 118.23/118.33 cnf(956,plain, % 118.23/118.33 (P4(a7,a8,a1,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[953,36,103])). % 118.23/118.33 cnf(961,plain, % 118.23/118.33 (P4(a7,a8,a2,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[747,71,105])). % 118.23/118.33 cnf(964,plain, % 118.23/118.33 (P4(a7,a8,a1,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[961,43,103])). % 118.23/118.33 cnf(983,plain, % 118.23/118.33 (P4(a8,a7,a3,a2,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[813,63,105])). % 118.23/118.33 cnf(986,plain, % 118.23/118.33 (P4(a8,a7,a3,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[983,36,99])). % 118.23/118.33 cnf(991,plain, % 118.23/118.33 (P4(a8,a7,a6,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[818,73,105])). % 118.23/118.33 cnf(996,plain, % 118.23/118.33 (P4(a8,a7,a8,a1,a7,a7)+~P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[860,90])). % 118.23/118.33 cnf(998,plain, % 118.23/118.33 (P4(a8,a7,a2,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[835,71,105])). % 118.23/118.33 cnf(1001,plain, % 118.23/118.33 (P4(a8,a7,a1,a3,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[998,36,103])). % 118.23/118.33 cnf(1003,plain, % 118.23/118.33 (~P4(a7,a6,a4,a7,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[84,998,36,72,103,105])). % 118.23/118.33 cnf(1006,plain, % 118.23/118.33 (~P4(a7,a6,a6,a7,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[225,66,105])). % 118.23/118.33 cnf(1009,plain, % 118.23/118.33 (~P4(a7,a6,a3,a7,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1006,70,105])). % 118.23/118.33 cnf(1011,plain, % 118.23/118.33 (~P4(a7,a6,a2,a7,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1003,64,105])). % 118.23/118.33 cnf(1029,plain, % 118.23/118.33 (P4(a7,a7,a1,a8,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[894,1,100])). % 118.23/118.33 cnf(1034,plain, % 118.23/118.33 (P4(a7,a7,a4,a1,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[898,43,99])). % 118.23/118.33 cnf(1048,plain, % 118.23/118.33 (P4(a7,a7,a5,a1,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[921,50,99])). % 118.23/118.33 cnf(1063,plain, % 118.23/118.33 (~P4(a7,a6,a4,a5,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1003,74,106])). % 118.23/118.33 cnf(1066,plain, % 118.23/118.33 (~P4(a7,a6,a4,a4,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1003,72,106])). % 118.23/118.33 cnf(1069,plain, % 118.23/118.33 (~P4(a7,a6,a4,a6,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1063,66,106])). % 118.23/118.33 cnf(1072,plain, % 118.23/118.33 (~P4(a7,a6,a4,a3,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1069,70,106])). % 118.23/118.33 cnf(1075,plain, % 118.23/118.33 (~P4(a7,a6,a4,a2,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1072,63,106])). % 118.23/118.33 cnf(1079,plain, % 118.23/118.33 (~P4(a7,a6,a6,a5,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1006,74,106])). % 118.23/118.33 cnf(1081,plain, % 118.23/118.33 (~P4(a7,a6,a2,a4,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1006,1066,74,64,106,105])). % 118.23/118.33 cnf(1084,plain, % 118.23/118.33 (~P4(a7,a6,a6,a4,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1006,72,106])). % 118.23/118.33 cnf(1086,plain, % 118.23/118.33 (~P4(a7,a6,a2,a2,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1006,1075,72,64,106,105])). % 118.23/118.33 cnf(1089,plain, % 118.23/118.33 (~P4(a7,a6,a6,a6,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1079,66,106])). % 118.23/118.33 cnf(1091,plain, % 118.23/118.33 (~P4(a7,a6,a2,a5,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1079,1063,66,64,106,105])). % 118.23/118.33 cnf(1094,plain, % 118.23/118.33 (~P4(a7,a6,a6,a3,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1089,70,106])). % 118.23/118.33 cnf(1097,plain, % 118.23/118.33 (~P4(a7,a6,a2,a6,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1091,66,106])). % 118.23/118.33 cnf(1100,plain, % 118.23/118.33 (~P4(a7,a6,a2,a3,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1097,70,106])). % 118.23/118.33 cnf(1103,plain, % 118.23/118.33 (~P4(a7,a6,a6,a2,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1094,63,106])). % 118.23/118.33 cnf(1107,plain, % 118.23/118.33 (~P4(a7,a6,a5,a4,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1084,73,105])). % 118.23/118.33 cnf(1109,plain, % 118.23/118.33 (~P4(a7,a6,a3,a5,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1009,1084,73,74,105,106])). % 118.23/118.33 cnf(1112,plain, % 118.23/118.33 (~P4(a7,a6,a5,a2,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1103,73,105])). % 118.23/118.33 cnf(1114,plain, % 118.23/118.33 (~P4(a7,a6,a3,a4,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1009,1103,73,72,105,106])). % 118.23/118.33 cnf(1117,plain, % 118.23/118.33 (~P4(a7,a6,a5,a5,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1079,73,105])). % 118.23/118.33 cnf(1119,plain, % 118.23/118.33 (~P4(a7,a6,a3,a6,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1109,1079,73,66,105,106])). % 118.23/118.33 cnf(1122,plain, % 118.23/118.33 (~P4(a7,a6,a3,a3,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1119,70,106])). % 118.23/118.33 cnf(1125,plain, % 118.23/118.33 (~P4(a7,a6,a5,a6,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1117,66,106])). % 118.23/118.33 cnf(1128,plain, % 118.23/118.33 (~P4(a7,a6,a5,a3,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1125,70,106])). % 118.23/118.33 cnf(1139,plain, % 118.23/118.33 (P4(a8,a7,a8,a7,a7,a7)+~P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[996,86])). % 118.23/118.33 cnf(1145,plain, % 118.23/118.33 (~P4(a7,a6,a3,a2,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1086,69,105])). % 118.23/118.33 cnf(1215,plain, % 118.23/118.33 (P4(a7,a7,a8,a7,a7,a7)+~P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[1139,91])). % 118.23/118.33 cnf(1288,plain, % 118.23/118.33 (P4(a7,a7,a8,a1,a7,a7)+~P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[1215,113])). % 118.23/118.33 cnf(1361,plain, % 118.23/118.33 (P4(a7,a1,a8,a1,a7,a7)+~P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[1288,93])). % 118.23/118.33 cnf(1433,plain, % 118.23/118.33 (P4(a1,a1,a8,a1,a7,a7)+~P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[1361,95])). % 118.23/118.33 cnf(1505,plain, % 118.23/118.33 (P4(a1,a1,a7,a1,a7,a7)+~P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[1433,87])). % 118.23/118.33 cnf(1577,plain, % 118.23/118.33 (P4(a1,a7,a7,a1,a7,a7)+~P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[1505,90])). % 118.23/118.33 cnf(1649,plain, % 118.23/118.33 (P4(a1,a7,a8,a1,a7,a7)+~P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[1577,157])). % 118.23/118.33 cnf(1721,plain, % 118.23/118.33 (P4(a1,a8,a8,a1,a7,a7)+~P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[1649,94])). % 118.23/118.33 cnf(1792,plain, % 118.23/118.33 (P4(a7,a8,a8,a1,a7,a7)+~P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[1721,92])). % 118.23/118.33 cnf(1859,plain, % 118.23/118.33 (P4(a7,a8,a7,a1,a7,a7)+~P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[1792,87])). % 118.23/118.33 cnf(1924,plain, % 118.23/118.33 (P4(a7,a7,a7,a1,a7,a7)+~P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[1859,89])). % 118.23/118.33 cnf(2011,plain, % 118.23/118.33 (P4(a8,a7,a5,a6,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[325,489,441,96])). % 118.23/118.33 cnf(2015,plain, % 118.23/118.33 (~P4(a7,a6,a7,a8,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[325,489,693,825,441,96,94,85])). % 118.23/118.33 cnf(2017,plain, % 118.23/118.33 (~P4(a1,a6,a7,a4,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[197,325,489,693,825,441,96,94,85,92])). % 118.23/118.33 cnf(2021,plain, % 118.23/118.33 (~P4(a7,a6,a8,a7,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[197,325,489,693,825,1011,441,96,94,85,92,88,87])). % 118.23/118.33 cnf(2023,plain, % 118.23/118.33 (~P4(a7,a6,a2,a1,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[197,325,489,693,825,1011,441,96,94,85,92,88,87,86])). % 118.23/118.33 cnf(2025,plain, % 118.23/118.33 (P4(a7,a7,a8,a1,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,489,693,825,1011,58,441,96,94,85,92,88,87,86,97])). % 118.23/118.33 cnf(2027,plain, % 118.23/118.33 (P4(a8,a7,a1,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,489,561,693,825,1011,58,441,96,94,85,92,88,87,86,97,101])). % 118.23/118.33 cnf(2029,plain, % 118.23/118.33 (P4(a7,a7,a6,a8,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,470,489,561,693,825,1011,58,62,441,96,94,85,92,88,87,86,97,101,98])). % 118.23/118.33 cnf(2031,plain, % 118.23/118.33 (P4(a8,a8,a6,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,470,489,561,693,825,1011,58,62,22,441,96,94,85,92,88,87,86,97,101,98,99])). % 118.23/118.33 cnf(2037,plain, % 118.23/118.33 (P4(a8,a7,a1,a8,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,470,489,534,561,693,825,1011,919,58,62,22,69,67,441,96,94,85,92,88,87,86,97,101,98,99,105,106,134])). % 118.23/118.33 cnf(2039,plain, % 118.23/118.33 (P4(a8,a8,a8,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,470,489,534,561,693,825,1011,919,58,62,22,69,67,441,96,94,85,92,88,87,86,97,101,98,99,105,106,134,157])). % 118.23/118.33 cnf(2043,plain, % 118.23/118.33 (P4(a8,a1,a8,a1,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,470,489,534,561,693,825,1011,919,58,62,22,69,67,441,96,94,85,92,88,87,86,97,101,98,99,105,106,134,157,703,860])). % 118.23/118.33 cnf(2044,plain, % 118.23/118.33 (P4(a8,a7,a8,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,470,489,534,561,693,825,1011,919,58,62,22,69,67,441,96,94,85,92,88,87,86,97,101,98,99,105,106,134,157,703,860,1139])). % 118.23/118.33 cnf(2045,plain, % 118.23/118.33 (P4(a7,a7,a8,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,470,489,534,561,693,825,1011,919,58,62,22,69,67,441,96,94,85,92,88,87,86,97,101,98,99,105,106,134,157,703,860,1139,1215])). % 118.23/118.33 cnf(2047,plain, % 118.23/118.33 (P4(a1,a8,a8,a1,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,470,489,534,561,693,825,1011,919,58,62,22,69,67,441,96,94,85,92,88,87,86,97,101,98,99,105,106,134,157,703,860,1139,1215,1505,1721])). % 118.23/118.33 cnf(2048,plain, % 118.23/118.33 (P4(a7,a8,a8,a1,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,470,489,534,561,693,825,1011,919,58,62,22,69,67,441,96,94,85,92,88,87,86,97,101,98,99,105,106,134,157,703,860,1139,1215,1505,1721,1792])). % 118.23/118.33 cnf(2049,plain, % 118.23/118.33 (P4(a7,a8,a7,a1,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,470,489,534,561,693,825,1011,919,58,62,22,69,67,441,96,94,85,92,88,87,86,97,101,98,99,105,106,134,157,703,860,1139,1215,1505,1721,1792,1859])). % 118.23/118.33 cnf(2050,plain, % 118.23/118.33 (P4(a1,a7,a8,a1,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,470,489,534,561,693,825,1011,919,58,62,22,69,67,441,96,94,85,92,88,87,86,97,101,98,99,105,106,134,157,703,860,1139,1215,1505,1721,1792,1859,95])). % 118.23/118.33 cnf(2052,plain, % 118.23/118.33 (P4(a7,a1,a8,a1,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,470,489,534,561,693,825,1011,919,58,62,22,69,67,441,96,94,85,92,88,87,86,97,101,98,99,105,106,134,157,703,860,1139,1215,1505,1721,1792,1859,95,93])). % 118.23/118.33 cnf(2056,plain, % 118.23/118.33 (P4(a8,a7,a8,a1,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[197,325,468,470,489,534,561,661,693,825,1011,919,58,62,22,69,67,441,96,94,85,92,88,87,86,97,101,98,99,105,106,134,157,703,860,1139,1215,1505,1721,1792,1859,95,93,104,113])). % 118.23/118.33 cnf(2060,plain, % 118.23/118.33 (P4(a1,a1,a8,a1,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[2027,1433])). % 118.23/118.33 cnf(2062,plain, % 118.23/118.33 (P4(a7,a7,a7,a1,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[2027,1924])). % 118.23/118.33 cnf(2065,plain, % 118.23/118.33 (P4(a1,a7,a8,a7,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[2045,95])). % 118.23/118.33 cnf(2071,plain, % 118.23/118.33 (P4(a7,a8,a6,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[373,625,2027,2045,95,96,93,94])). % 118.23/118.33 cnf(2075,plain, % 118.23/118.33 (~P4(a1,a6,a2,a4,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[373,1081,1145,625,2027,2045,95,96,93,94,85,92])). % 118.23/118.33 cnf(2077,plain, % 118.23/118.33 (~P4(a7,a6,a1,a8,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[373,1081,1145,625,2015,2027,2045,95,96,93,94,85,92,88])). % 118.23/118.33 cnf(2083,plain, % 118.23/118.33 (P4(a7,a7,a8,a3,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[373,481,1081,1145,625,2015,2021,2027,2045,62,95,96,93,94,85,92,88,87,86,102])). % 118.23/118.33 cnf(2085,plain, % 118.23/118.33 (P4(a8,a7,a1,a8,a6,a7)), % 118.23/118.33 inference(scs_inference,[],[373,481,568,1081,1145,625,2015,2021,2027,2045,57,62,95,96,93,94,85,92,88,87,86,102,101])). % 118.23/118.33 cnf(2087,plain, % 118.23/118.33 (P4(a7,a7,a6,a1,a6,a7)), % 118.23/118.33 inference(scs_inference,[],[373,481,487,568,1081,1145,625,2015,2021,2027,2045,57,62,95,96,93,94,85,92,88,87,86,102,101,97])). % 118.23/118.33 cnf(2089,plain, % 118.23/118.33 (P4(a7,a7,a2,a8,a2,a6)), % 118.23/118.33 inference(scs_inference,[],[373,481,487,568,896,1081,1145,625,2015,2021,2027,2045,57,62,95,96,93,94,85,92,88,87,86,102,101,97,98])). % 118.23/118.33 cnf(2091,plain, % 118.23/118.33 (P4(a8,a1,a1,a8,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[1,373,481,487,568,896,1081,1145,625,2015,2021,2027,2045,57,62,95,96,93,94,85,92,88,87,86,102,101,97,98,100])). % 118.23/118.33 cnf(2095,plain, % 118.23/118.33 (~P4(a1,a6,a7,a7,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1,373,481,487,568,896,1081,1145,625,2015,2017,2021,2027,2045,57,62,74,67,95,96,93,94,85,92,88,87,86,102,101,97,98,100,105,106])). % 118.23/118.33 cnf(2097,plain, % 118.23/118.33 (~P4(a1,a6,a8,a7,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1,373,481,487,568,896,1081,1145,625,2015,2017,2021,2027,2045,57,62,74,67,95,96,93,94,85,92,88,87,86,102,101,97,98,100,105,106,117])). % 118.23/118.33 cnf(2099,plain, % 118.23/118.33 (~P4(a1,a6,a2,a7,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1,373,481,487,568,896,1081,1145,625,2015,2017,2021,2027,2045,57,62,30,74,67,95,96,93,94,85,92,88,87,86,102,101,97,98,100,105,106,117,104])). % 118.23/118.33 cnf(2102,plain, % 118.23/118.33 (P4(a1,a8,a7,a1,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[2049,95])). % 118.23/118.33 cnf(2104,plain, % 118.23/118.33 (P4(a8,a7,a4,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[377,2049,95,96])). % 118.23/118.33 cnf(2108,plain, % 118.23/118.33 (P4(a8,a8,a4,a1,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[377,808,2065,2049,95,96,93,94])). % 118.23/118.33 cnf(2110,plain, % 118.23/118.33 (~P4(a7,a6,a2,a8,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[377,808,2065,2049,1086,95,96,93,94,85])). % 118.23/118.33 cnf(2112,plain, % 118.23/118.33 (~P4(a1,a6,a5,a4,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[377,1107,808,2065,2049,1086,95,96,93,94,85,92])). % 118.23/118.33 cnf(2114,plain, % 118.23/118.33 (~P4(a1,a6,a1,a7,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[377,1107,808,2065,2049,2095,1086,95,96,93,94,85,92,88])). % 118.23/118.33 cnf(2118,plain, % 118.23/118.33 (~P4(a1,a6,a2,a1,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[377,1107,1100,808,2065,2099,2049,2095,1086,95,96,93,94,85,92,88,87,86])). % 118.23/118.33 cnf(2120,plain, % 118.23/118.33 (P4(a8,a8,a8,a7,a2,a2)), % 118.23/118.33 inference(scs_inference,[],[377,1107,1100,808,788,2065,2099,2049,2095,1086,61,95,96,93,94,85,92,88,87,86,102])). % 118.23/118.33 cnf(2122,plain, % 118.23/118.33 (P4(a7,a7,a6,a1,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[377,1107,1100,808,788,2065,2099,2049,2087,2095,1086,60,61,95,96,93,94,85,92,88,87,86,102,97])). % 118.23/118.33 cnf(2124,plain, % 118.23/118.33 (P4(a7,a8,a1,a3,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[377,956,1107,1100,808,788,2065,2099,2049,2087,2095,1086,60,58,61,95,96,93,94,85,92,88,87,86,102,97,101])). % 118.23/118.33 cnf(2128,plain, % 118.23/118.33 (~P4(a7,a6,a1,a2,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[1,377,531,956,1107,1100,808,788,2065,2099,2049,2077,2087,2095,1086,60,58,61,95,96,93,94,85,92,88,87,86,102,97,101,98,100])). % 118.23/118.33 cnf(2130,plain, % 118.23/118.33 (P4(a7,a8,a2,a5,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[1,377,531,956,1107,1100,808,788,881,2065,2099,2049,2077,2087,2095,1086,60,58,61,71,95,96,93,94,85,92,88,87,86,102,97,101,98,100,105])). % 118.23/118.33 cnf(2132,plain, % 118.23/118.33 (P4(a8,a8,a8,a4,a2,a7)), % 118.23/118.33 inference(scs_inference,[],[1,377,531,956,1107,1100,808,788,881,2065,2099,2049,2077,2087,2095,1086,60,58,61,71,67,95,96,93,94,85,92,88,87,86,102,97,101,98,100,105,106])). % 118.23/118.33 cnf(2137,plain, % 118.23/118.33 (P4(a1,a7,a6,a1,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[2122,95])). % 118.23/118.33 cnf(2141,plain, % 118.23/118.33 (P4(a7,a1,a6,a1,a7,a7)), % 118.23/118.33 inference(scs_inference,[],[411,2122,95,96,93])). % 118.23/118.33 cnf(2147,plain, % 118.23/118.33 (~P4(a1,a6,a3,a4,a7,a2)), % 118.23/118.33 inference(scs_inference,[],[411,1114,820,2122,1103,95,96,93,94,85,92])). % 118.23/118.33 cnf(2149,plain, % 118.23/118.33 (~P4(a7,a6,a1,a5,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[411,1114,820,2122,685,1103,95,96,93,94,85,92,88])). % 118.23/118.34 cnf(2153,plain, % 118.23/118.34 (~P4(a1,a6,a8,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[411,1114,820,2097,2075,2122,685,1103,95,96,93,94,85,92,88,87,86])). % 118.23/118.34 cnf(2155,plain, % 118.23/118.34 (P4(a7,a7,a8,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[411,1114,820,2025,2097,2075,2122,685,1103,62,95,96,93,94,85,92,88,87,86,102])). % 118.23/118.34 cnf(2157,plain, % 118.23/118.34 (P4(a7,a7,a1,a8,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[411,1114,1029,820,2025,2097,2075,2122,685,1103,58,62,95,96,93,94,85,92,88,87,86,102,101])). % 118.23/118.34 cnf(2159,plain, % 118.23/118.34 (P4(a7,a7,a5,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[411,493,1114,1029,820,2025,2097,2075,2122,685,1103,58,62,95,96,93,94,85,92,88,87,86,102,101,97])). % 118.23/118.34 cnf(2163,plain, % 118.23/118.34 (~P4(a1,a6,a3,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[411,493,1114,1029,820,2025,2097,2029,2075,2118,2122,685,1103,59,58,62,69,95,96,93,94,85,92,88,87,86,102,101,97,98,105])). % 118.23/118.34 cnf(2165,plain, % 118.23/118.34 (~P4(a1,a6,a2,a2,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[411,493,1114,1029,820,2025,2097,2029,2075,2118,2122,685,1103,59,58,62,69,64,95,96,93,94,85,92,88,87,86,102,101,97,98,105,106])). % 118.23/118.34 cnf(2172,plain, % 118.23/118.34 (P4(a1,a8,a1,a3,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2124,95])). % 118.23/118.34 cnf(2176,plain, % 118.23/118.34 (P4(a1,a1,a6,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[696,2124,2137,95,96,93])). % 118.23/118.34 cnf(2178,plain, % 118.23/118.34 (P4(a8,a8,a3,a1,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[696,986,2124,2137,95,96,93,94])). % 118.23/118.34 cnf(2180,plain, % 118.23/118.34 (~P4(a1,a6,a2,a8,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[696,986,2124,2137,2165,95,96,93,94,85])). % 118.23/118.34 cnf(2182,plain, % 118.23/118.34 (~P4(a1,a6,a3,a3,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[696,1122,986,2124,2137,2165,95,96,93,94,85,92])). % 118.23/118.34 cnf(2184,plain, % 118.23/118.34 (~P4(a7,a6,a1,a6,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[696,1122,986,2124,2137,2165,687,95,96,93,94,85,92,88])). % 118.23/118.34 cnf(2188,plain, % 118.23/118.34 (~P4(a1,a6,a1,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[696,1122,986,2110,2114,2124,2137,2165,687,95,96,93,94,85,92,88,87,86])). % 118.23/118.34 cnf(2190,plain, % 118.23/118.34 (P4(a1,a7,a8,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[696,1122,2050,986,2110,2114,2124,2137,2165,687,61,95,96,93,94,85,92,88,87,86,102])). % 118.23/118.34 cnf(2192,plain, % 118.23/118.34 (P4(a7,a8,a5,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[696,1122,2050,986,2110,2114,2124,2137,2165,687,57,61,95,96,93,94,85,92,88,87,86,102,97])). % 118.23/118.34 cnf(2194,plain, % 118.23/118.34 (P4(a8,a7,a1,a2,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[696,1122,2050,986,816,2110,2114,2124,2137,2165,687,57,61,95,96,93,94,85,92,88,87,86,102,97,101])). % 118.23/118.34 cnf(2198,plain, % 118.23/118.34 (P4(a8,a7,a2,a4,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[556,696,1122,2050,986,816,845,2110,2114,2124,2137,2165,687,57,61,71,95,96,93,94,85,92,88,87,86,102,97,101,98,105])). % 118.23/118.34 cnf(2207,plain, % 118.23/118.34 (P4(a8,a8,a1,a2,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[723,96])). % 118.23/118.34 cnf(2209,plain, % 118.23/118.34 (P4(a1,a7,a8,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[723,2155,96,95])). % 118.23/118.34 cnf(2211,plain, % 118.23/118.34 (P4(a7,a1,a8,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[723,2155,96,95,93])). % 118.23/118.34 cnf(2213,plain, % 118.23/118.34 (P4(a8,a8,a8,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2056,723,2155,96,95,93,94])). % 118.23/118.34 cnf(2215,plain, % 118.23/118.34 (~P4(a7,a6,a4,a8,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2056,723,2155,1075,96,95,93,94,85])). % 118.23/118.34 cnf(2217,plain, % 118.23/118.34 (~P4(a1,a6,a5,a2,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[1112,2056,723,2155,1075,96,95,93,94,85,92])). % 118.23/118.34 cnf(2219,plain, % 118.23/118.34 (~P4(a7,a6,a1,a3,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[1112,2056,723,2155,690,1075,96,95,93,94,85,92,88])). % 118.23/118.34 cnf(2225,plain, % 118.23/118.34 (P4(a1,a1,a8,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[1112,2060,2056,723,2155,2180,225,690,1075,62,96,95,93,94,85,92,88,87,86,102])). % 118.23/118.34 cnf(2227,plain, % 118.23/118.34 (P4(a7,a7,a1,a3,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[1112,2060,2056,862,723,2155,2180,225,690,1075,62,58,96,95,93,94,85,92,88,87,86,102,101])). % 118.23/118.34 cnf(2229,plain, % 118.23/118.34 (P4(a7,a8,a4,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[715,1112,2060,2056,862,723,2155,2180,225,690,1075,62,58,96,95,93,94,85,92,88,87,86,102,101,97])). % 118.23/118.34 cnf(2235,plain, % 118.23/118.34 (~P4(a1,a6,a3,a2,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[483,715,1112,2060,2056,862,723,2147,2155,2180,225,690,1075,62,58,65,64,96,95,93,94,85,92,88,87,86,102,101,97,98,105,106])). % 118.23/118.34 cnf(2242,plain, % 118.23/118.34 (P4(a1,a7,a1,a8,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2157,95])). % 118.23/118.34 cnf(2246,plain, % 118.23/118.34 (P4(a7,a1,a1,a8,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[742,2157,95,96,93])). % 118.23/118.34 cnf(2248,plain, % 118.23/118.34 (P4(a8,a8,a1,a8,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2037,742,2157,95,96,93,94])). % 118.23/118.34 cnf(2250,plain, % 118.23/118.34 (~P4(a1,a6,a5,a8,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2037,742,2157,2217,95,96,93,94,85])). % 118.23/118.34 cnf(2254,plain, % 118.23/118.34 (~P4(a1,a6,a1,a4,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[1128,2037,742,2157,2217,2017,95,96,93,94,85,92,88])). % 118.23/118.34 cnf(2256,plain, % 118.23/118.34 (~P4(a7,a6,a8,a6,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[1128,2037,742,2157,2217,1097,2017,95,96,93,94,85,92,88,87])). % 118.23/118.34 cnf(2262,plain, % 118.23/118.34 (P4(a7,a8,a5,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[1128,2052,2037,742,2157,2192,2217,1097,2095,2017,60,61,95,96,93,94,85,92,88,87,86,102,97])). % 118.23/118.34 cnf(2264,plain, % 118.23/118.34 (P4(a7,a8,a1,a4,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[1128,2052,2037,742,964,2157,2192,2217,1097,2095,2017,60,57,61,95,96,93,94,85,92,88,87,86,102,97,101])). % 118.23/118.34 cnf(2266,plain, % 118.23/118.34 (P4(a7,a8,a6,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[683,1128,2052,2037,742,964,2157,2192,2217,1097,2095,2017,60,57,61,95,96,93,94,85,92,88,87,86,102,97,101,98])). % 118.23/118.34 cnf(2268,plain, % 118.23/118.34 (P4(a7,a7,a1,a8,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[683,1128,2052,2037,742,964,2089,2157,2192,2217,1097,2095,2017,60,57,61,8,95,96,93,94,85,92,88,87,86,102,97,101,98,103])). % 118.23/118.34 cnf(2270,plain, % 118.23/118.34 (P4(a8,a7,a6,a3,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[683,1128,2052,2037,742,964,838,2089,2157,2192,2217,1097,2095,2017,60,57,61,8,73,95,96,93,94,85,92,88,87,86,102,97,101,98,103,105])). % 118.23/118.34 cnf(2272,plain, % 118.23/118.34 (P4(a7,a8,a6,a6,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[683,1128,2052,2037,742,964,838,2071,2089,2157,2192,2217,1097,2095,2017,60,57,61,8,73,95,96,93,94,85,92,88,87,86,102,97,101,98,103,105,106])). % 118.23/118.34 cnf(2279,plain, % 118.23/118.34 (P4(a8,a8,a5,a4,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[750,96])). % 118.23/118.34 cnf(2281,plain, % 118.23/118.34 (P4(a1,a7,a5,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[750,2159,96,95])). % 118.23/118.34 cnf(2283,plain, % 118.23/118.34 (P4(a7,a1,a5,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[750,2159,96,95,93])). % 118.23/118.34 cnf(2285,plain, % 118.23/118.34 (P4(a8,a8,a1,a3,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[750,1001,2159,96,95,93,94])). % 118.23/118.34 cnf(2287,plain, % 118.23/118.34 (~P4(a1,a6,a3,a8,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[750,1001,2159,2235,96,95,93,94,85])). % 118.23/118.34 cnf(2289,plain, % 118.23/118.34 (~P4(a1,a6,a1,a2,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[750,1001,2128,2159,2235,96,95,93,94,85,92])). % 118.23/118.34 cnf(2291,plain, % 118.23/118.34 (~P4(a7,a6,a1,a7,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[750,1001,2128,2159,2235,84,96,95,93,94,85,92,88])). % 118.23/118.34 cnf(2293,plain, % 118.23/118.34 (~P4(a7,a6,a8,a5,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[750,1001,2128,2159,2235,1091,84,96,95,93,94,85,92,88,87])). % 118.23/118.34 cnf(2297,plain, % 118.23/118.34 (P4(a8,a1,a8,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[2043,750,1001,2128,2159,2235,1091,1009,84,62,96,95,93,94,85,92,88,87,86,102])). % 118.23/118.34 cnf(2299,plain, % 118.23/118.34 (P4(a8,a1,a1,a8,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[2043,2091,750,1001,2128,2159,2235,1091,1009,84,62,96,95,93,94,85,92,88,87,86,102,101])). % 118.23/118.34 cnf(2301,plain, % 118.23/118.34 (P4(a7,a7,a8,a1,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[888,2043,2091,750,1001,2128,2159,2235,1091,1009,84,62,57,96,95,93,94,85,92,88,87,86,102,101,97])). % 118.23/118.34 cnf(2303,plain, % 118.23/118.34 (P4(a7,a8,a5,a8,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[760,888,2043,2091,750,1001,2128,2159,2235,1091,1009,84,62,57,96,95,93,94,85,92,88,87,86,102,101,97,98])). % 118.23/118.34 cnf(2305,plain, % 118.23/118.34 (~P4(a1,a6,a7,a2,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[760,888,2043,2091,750,1001,2128,2159,2235,1091,1009,84,62,57,15,96,95,93,94,85,92,88,87,86,102,101,97,98,103])). % 118.23/118.34 cnf(2309,plain, % 118.23/118.34 (~P4(a1,a6,a5,a7,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[760,888,2043,2091,750,1001,2128,2163,2112,2159,2235,1091,1009,84,62,57,15,65,67,96,95,93,94,85,92,88,87,86,102,101,97,98,103,105,106])). % 118.23/118.34 cnf(2316,plain, % 118.23/118.34 (P4(a1,a7,a1,a3,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2227,95])). % 118.23/118.34 cnf(2318,plain, % 118.23/118.34 (P4(a8,a8,a3,a3,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[929,2227,95,96])). % 118.23/118.34 cnf(2320,plain, % 118.23/118.34 (P4(a1,a1,a8,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[929,2190,2227,95,96,93])). % 118.23/118.34 cnf(2326,plain, % 118.23/118.34 (~P4(a1,a6,a1,a3,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[929,2219,2085,2190,2227,2289,95,96,93,94,85,92])). % 118.23/118.34 cnf(2328,plain, % 118.23/118.34 (~P4(a1,a6,a8,a2,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[929,2219,2085,2190,2227,2289,2165,95,96,93,94,85,92,87])). % 118.23/118.34 cnf(2336,plain, % 118.23/118.34 (P4(a8,a8,a1,a2,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2047,929,2219,2085,2190,2207,2227,2289,2291,2301,2165,60,58,61,95,96,93,94,85,92,87,86,102,97,101])). % 118.23/118.34 cnf(2340,plain, % 118.23/118.34 (P4(a7,a8,a1,a5,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[799,2047,929,2219,2085,2130,2190,2207,2227,2289,2291,2301,2165,60,50,58,61,95,96,93,94,85,92,87,86,102,97,101,98,103])). % 118.23/118.34 cnf(2342,plain, % 118.23/118.34 (P4(a7,a7,a7,a1,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[799,1048,2047,929,2219,2085,2130,2190,2207,2227,2289,2291,2301,2165,60,50,58,61,74,95,96,93,94,85,92,87,86,102,97,101,98,103,105])). % 118.23/118.34 cnf(2344,plain, % 118.23/118.34 (P4(a8,a8,a8,a5,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[799,1048,2047,929,2219,2085,2120,2130,2190,2207,2227,2289,2291,2301,2165,60,50,58,61,74,68,95,96,93,94,85,92,87,86,102,97,101,98,103,105,106])). % 118.23/118.34 cnf(2351,plain, % 118.23/118.34 (P4(a1,a8,a4,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2229,95])). % 118.23/118.34 cnf(2355,plain, % 118.23/118.34 (P4(a1,a1,a1,a8,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[884,2229,2242,95,96,93])). % 118.23/118.34 cnf(2365,plain, % 118.23/118.34 (~P4(a1,a6,a5,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[884,2184,2011,2229,2242,2309,2305,1086,95,96,93,94,85,92,87,86])). % 118.23/118.34 cnf(2367,plain, % 118.23/118.34 (P4(a7,a8,a8,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[2048,884,2184,2011,2229,2242,2309,2305,1086,62,95,96,93,94,85,92,87,86,102])). % 118.23/118.34 cnf(2369,plain, % 118.23/118.34 (P4(a7,a7,a8,a1,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[910,2048,884,2184,2011,2229,2242,2309,2305,1086,57,62,95,96,93,94,85,92,87,86,102,97])). % 118.23/118.34 cnf(2371,plain, % 118.23/118.34 (P4(a1,a8,a1,a3,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[910,2048,884,2184,2011,2172,2229,2242,2309,2305,1086,57,62,95,96,93,94,85,92,87,86,102,97,101])). % 118.23/118.34 cnf(2373,plain, % 118.23/118.34 (P4(a8,a8,a6,a8,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[775,910,2048,884,2184,2011,2172,2229,2242,2309,2305,1086,57,62,95,96,93,94,85,92,87,86,102,97,101,98])). % 118.23/118.34 cnf(2379,plain, % 118.23/118.34 (~P4(a1,a6,a8,a3,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[775,910,2048,884,2184,2328,2011,2172,2182,2229,2242,2309,2326,2305,1086,69,57,62,36,65,95,96,93,94,85,92,87,86,102,97,101,98,103,105,106])). % 118.23/118.34 cnf(2386,plain, % 118.23/118.34 (~P4(a1,a6,a1,a5,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2149,92])). % 118.23/118.34 cnf(2390,plain, % 118.23/118.34 (P4(a1,a8,a5,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2149,854,2262,92,96,95])). % 118.23/118.34 cnf(2392,plain, % 118.23/118.34 (P4(a1,a1,a5,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2149,854,2262,2281,92,96,95,93])). % 118.23/118.34 cnf(2396,plain, % 118.23/118.34 (~P4(a7,a6,a4,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2149,854,2104,2262,2281,1003,92,96,95,93,94,86])). % 118.23/118.34 cnf(2398,plain, % 118.23/118.34 (P4(a8,a8,a8,a1,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2039,2149,854,2104,2262,2281,1003,61,92,96,95,93,94,86,102])). % 118.23/118.34 cnf(2400,plain, % 118.23/118.34 (P4(a8,a7,a1,a2,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2039,2149,854,2104,2194,2262,2281,1003,60,61,92,96,95,93,94,86,102,101])). % 118.23/118.34 cnf(2402,plain, % 118.23/118.34 (P4(a8,a7,a6,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[991,2039,2149,854,2104,2194,2262,2281,1003,60,58,61,92,96,95,93,94,86,102,101,97])). % 118.23/118.34 cnf(2404,plain, % 118.23/118.34 (P4(a8,a8,a5,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[991,797,2039,2149,854,2104,2194,2262,2281,1003,60,58,61,92,96,95,93,94,86,102,101,97,98])). % 118.23/118.34 cnf(2406,plain, % 118.23/118.34 (P4(a8,a7,a6,a4,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[991,797,2039,848,2149,854,2104,2194,2262,2281,1003,60,58,61,73,92,96,95,93,94,86,102,101,97,98,105])). % 118.23/118.34 cnf(2410,plain, % 118.23/118.34 (P4(a8,a7,a1,a4,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[991,797,2039,848,2149,854,2279,2104,2194,2198,2262,2281,1003,60,43,58,71,61,73,92,96,95,93,94,86,102,101,97,98,105,106,103])). % 118.23/118.34 cnf(2419,plain, % 118.23/118.34 (P4(a8,a1,a6,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2141,2396,92,96])). % 118.23/118.34 cnf(2421,plain, % 118.23/118.34 (P4(a1,a8,a8,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[2141,2367,2396,92,96,95])). % 118.23/118.34 cnf(2423,plain, % 118.23/118.34 (P4(a1,a1,a1,a3,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2141,2316,2367,2396,92,96,95,93])). % 118.23/118.34 cnf(2429,plain, % 118.23/118.34 (P4(a8,a8,a8,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2213,2141,2270,2316,2367,2396,1006,61,92,96,95,93,94,86,102])). % 118.23/118.34 cnf(2431,plain, % 118.23/118.34 (P4(a1,a1,a1,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2213,2355,2141,2270,2316,2367,2396,1006,61,92,96,95,93,94,86,102,101])). % 118.23/118.34 cnf(2435,plain, % 118.23/118.34 (P4(a8,a8,a1,a8,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2031,2213,2355,2141,2248,2270,2316,2367,2396,1006,57,61,92,96,95,93,94,86,102,101,97,98])). % 118.23/118.34 cnf(2437,plain, % 118.23/118.34 (~P4(a1,a6,a6,a8,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2031,2213,2355,2141,2248,2270,2316,2367,2396,2250,1006,57,61,66,92,96,95,93,94,86,102,101,97,98,105])). % 118.23/118.34 cnf(2448,plain, % 118.23/118.34 (P4(a8,a8,a1,a4,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[2264,2215,92,96])). % 118.23/118.34 cnf(2450,plain, % 118.23/118.34 (P4(a8,a1,a1,a2,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2264,2400,2215,92,96,93])). % 118.23/118.34 cnf(2456,plain, % 118.23/118.34 (P4(a8,a8,a8,a4,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[2132,2264,2400,2402,2215,84,62,92,96,93,94,86,102])). % 118.23/118.34 cnf(2458,plain, % 118.23/118.34 (P4(a7,a8,a1,a4,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2132,2264,2400,2402,2215,60,84,62,92,96,93,94,86,102,101])). % 118.23/118.34 cnf(2460,plain, % 118.23/118.34 (P4(a7,a8,a3,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[675,2132,2264,2400,2402,2215,60,84,58,62,92,96,93,94,86,102,101,97])). % 118.23/118.34 cnf(2464,plain, % 118.23/118.34 (P4(a7,a1,a1,a8,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[675,2132,2246,2264,2400,2402,2215,60,84,44,58,62,92,96,93,94,86,102,101,97,100,98])). % 118.23/118.34 cnf(2466,plain, % 118.23/118.34 (P4(a7,a7,a7,a1,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[675,1034,2132,2246,2264,2400,2402,2215,60,84,44,58,72,62,92,96,93,94,86,102,101,97,100,98,105])). % 118.23/118.34 cnf(2470,plain, % 118.23/118.34 (P4(a1,a8,a1,a4,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[675,1034,872,2132,2246,2264,2400,2402,2215,60,84,44,58,72,62,92,96,93,94,86,102,101,97,100,98,105,106,95])). % 118.23/118.34 cnf(2477,plain, % 118.23/118.34 (~P4(a1,a6,a8,a5,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2293,92])). % 118.23/118.34 cnf(2479,plain, % 118.23/118.34 (P4(a8,a8,a1,a5,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2340,2293,92,96])). % 118.23/118.34 cnf(2481,plain, % 118.23/118.34 (P4(a1,a8,a3,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2340,2460,2293,92,96,95])). % 118.23/118.34 cnf(2483,plain, % 118.23/118.34 (P4(a7,a1,a1,a3,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2340,2460,2293,2227,92,96,95,93])). % 118.23/118.34 cnf(2489,plain, % 118.23/118.34 (P4(a7,a7,a1,a8,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[2268,2340,2410,2460,437,2293,2227,57,61,92,96,95,93,94,102,101])). % 118.23/118.34 cnf(2491,plain, % 118.23/118.34 (P4(a7,a7,a3,a1,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[906,2268,2340,2410,2460,437,2293,2227,57,61,92,96,95,93,94,102,101,97])). % 118.23/118.34 cnf(2493,plain, % 118.23/118.34 (P4(a8,a1,a1,a8,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[906,2268,2340,2410,2299,2460,437,2293,2227,57,62,61,92,96,95,93,94,102,101,97,98])). % 118.23/118.34 cnf(2508,plain, % 118.23/118.34 (P4(a8,a8,a6,a6,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2272,2256,92,96])). % 118.23/118.34 cnf(2510,plain, % 118.23/118.34 (P4(a1,a1,a1,a8,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2272,2464,2256,92,96,95])). % 118.23/118.34 cnf(2512,plain, % 118.23/118.34 (P4(a8,a1,a8,a7,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2272,2464,2256,2044,92,96,95,93])). % 118.23/118.34 cnf(2516,plain, % 118.23/118.34 (P4(a8,a1,a8,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2272,2297,2406,2464,2256,2044,59,92,96,95,93,94,102])). % 118.23/118.34 cnf(2518,plain, % 118.23/118.34 (P4(a8,a8,a1,a3,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2272,2285,2297,2406,2464,2256,2044,59,58,92,96,95,93,94,102,101])). % 118.23/118.34 cnf(2522,plain, % 118.23/118.34 (P4(a1,a1,a3,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2178,2176,2272,2285,2297,2406,2464,2256,2044,59,58,65,92,96,95,93,94,102,101,97,105])). % 118.23/118.34 cnf(2526,plain, % 118.23/118.34 (P4(a1,a1,a1,a2,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2178,2176,2423,2272,2285,2297,2303,2406,2464,2256,2044,59,69,58,65,92,96,95,93,94,102,101,97,105,98,106])). % 118.23/118.34 cnf(2535,plain, % 118.23/118.34 (P4(a8,a1,a5,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2283,1119,92,96])). % 118.23/118.34 cnf(2537,plain, % 118.23/118.34 (P4(a7,a1,a8,a7,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2283,1119,2045,92,96,93])). % 118.23/118.34 cnf(2539,plain, % 118.23/118.34 (P4(a7,a8,a1,a6,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2283,111,1119,2045,92,96,93,94])). % 118.23/118.34 cnf(2541,plain, % 118.23/118.34 (P4(a8,a1,a8,a7,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[2512,2283,111,1119,2045,62,92,96,93,94,102])). % 118.23/118.34 cnf(2562,plain, % 118.23/118.34 (P4(a8,a8,a8,a3,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2458,563,1069,92,96,94])). % 118.23/118.34 cnf(2566,plain, % 118.23/118.34 (P4(a1,a8,a1,a3,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2537,2371,2458,563,1069,59,61,92,96,94,102,101])). % 118.23/118.34 cnf(2568,plain, % 118.23/118.34 (P4(a8,a8,a4,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[2108,2537,2371,2458,563,1069,59,57,61,92,96,94,102,101,97])). % 118.23/118.34 cnf(2570,plain, % 118.23/118.34 (P4(a8,a8,a2,a3,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2318,2108,2537,2371,2458,563,1069,59,69,57,61,92,96,94,102,101,97,105])). % 118.23/118.34 cnf(2574,plain, % 118.23/118.34 (P4(a8,a1,a1,a3,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[901,2318,2450,2108,2537,2371,2458,563,1069,59,69,63,57,61,92,96,94,102,101,97,105,98,106])). % 118.23/118.34 cnf(2585,plain, % 118.23/118.34 (P4(a8,a8,a1,a6,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2539,1072,92,96])). % 118.23/118.34 cnf(2589,plain, % 118.23/118.34 (P4(a8,a8,a8,a3,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2539,2562,1072,845,61,92,96,94,102])). % 118.23/118.34 cnf(2593,plain, % 118.23/118.34 (P4(a1,a1,a8,a1,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[2225,2510,2539,2562,1072,845,61,92,96,94,102,101,97])). % 118.23/118.34 cnf(2604,plain, % 118.23/118.34 (P4(a8,a7,a8,a5,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[396,1089,92,96])). % 118.23/118.34 cnf(2608,plain, % 118.23/118.34 (P4(a8,a8,a8,a5,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2344,396,1089,835,58,92,96,94,102])). % 118.23/118.34 cnf(2610,plain, % 118.23/118.34 (P4(a1,a1,a1,a8,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[2344,2431,396,1089,835,58,57,92,96,94,102,101])). % 118.23/118.34 cnf(2616,plain, % 118.23/118.34 (P4(a7,a7,a1,a8,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[2351,2342,2344,2431,2489,396,1089,835,59,71,58,57,92,96,94,102,101,97,105,98])). % 118.23/118.34 cnf(2622,plain, % 118.23/118.34 (P4(a7,a1,a7,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[2351,2483,2342,2344,2431,2489,396,1089,835,59,69,71,58,57,92,96,94,102,101,97,105,98,106,95,93])). % 118.23/118.34 cnf(2627,plain, % 118.23/118.34 (P4(a8,a7,a8,a6,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[358,96])). % 118.23/118.34 cnf(2629,plain, % 118.23/118.34 (P4(a1,a1,a7,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[2622,358,96,95])). % 118.23/118.34 cnf(2633,plain, % 118.23/118.34 (P4(a8,a7,a8,a5,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[2604,2622,358,2087,62,96,95,94,102])). % 118.23/118.34 cnf(2637,plain, % 118.23/118.34 (P4(a1,a1,a8,a1,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[2320,2336,2604,2622,358,2087,62,96,95,94,102,101,97])). % 118.23/118.34 cnf(2646,plain, % 118.23/118.34 (P4(a8,a7,a1,a5,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[153,96])). % 118.23/118.34 cnf(2648,plain, % 118.23/118.34 (P4(a8,a8,a8,a6,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2627,153,96,94])). % 118.23/118.34 cnf(2650,plain, % 118.23/118.34 (P4(a7,a7,a8,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[2369,2627,153,60,96,94,102])). % 118.23/118.34 cnf(2656,plain, % 118.23/118.34 (P4(a8,a1,a3,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2419,2518,2369,2398,2627,153,60,65,57,62,96,94,102,101,97,105])). % 118.23/118.34 cnf(2658,plain, % 118.23/118.34 (P4(a1,a1,a1,a8,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[2419,2518,2369,2398,2610,2627,153,60,65,58,57,62,96,94,102,101,97,105,98])). % 118.23/118.34 cnf(2665,plain, % 118.23/118.34 (P4(a8,a7,a8,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[2650,96])). % 118.23/118.34 cnf(2667,plain, % 118.23/118.34 (P4(a7,a8,a8,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[2650,96,94])). % 118.23/118.34 cnf(2669,plain, % 118.23/118.34 (P4(a8,a8,a8,a5,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[2608,2650,62,96,94,102])). % 118.23/118.34 cnf(2671,plain, % 118.23/118.34 (P4(a8,a8,a1,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2608,2435,2650,61,62,96,94,102,101])). % 118.23/118.34 cnf(2673,plain, % 118.23/118.34 (P4(a1,a1,a5,a1,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2392,2608,2435,2650,61,62,96,94,102,101,97])). % 118.23/118.34 cnf(2677,plain, % 118.23/118.34 (P4(a7,a7,a4,a6,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2392,864,2608,2435,2650,2658,70,61,62,96,94,102,101,97,98,106])). % 118.23/118.34 cnf(2684,plain, % 118.23/118.34 (P4(a8,a8,a8,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[2667,96])). % 118.23/118.34 cnf(2692,plain, % 118.23/118.34 (P4(a1,a8,a6,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2390,2456,2491,2667,2198,59,60,73,96,94,102,97,105])). % 118.23/118.34 cnf(2694,plain, % 118.23/118.34 (P4(a8,a1,a1,a8,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[2390,2456,2491,2493,2667,2198,59,60,73,96,94,102,97,105,98])). % 118.23/118.34 cnf(2696,plain, % 118.23/118.34 (P4(a1,a7,a3,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2390,2456,2491,2493,2667,2198,59,60,73,96,94,102,97,105,98,95])). % 118.23/118.34 cnf(2698,plain, % 118.23/118.34 (P4(a7,a1,a3,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2390,2456,2491,2493,2667,2198,59,60,73,96,94,102,97,105,98,95,93])). % 118.23/118.34 cnf(2700,plain, % 118.23/118.34 (P4(a8,a8,a1,a5,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2390,2479,2456,2491,2493,2667,2198,59,60,73,58,96,94,102,97,105,98,95,93,101])). % 118.23/118.34 cnf(2705,plain, % 118.23/118.34 (P4(a1,a1,a3,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2698,95])). % 118.23/118.34 cnf(2707,plain, % 118.23/118.34 (P4(a8,a7,a7,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2698,2062,95,96])). % 118.23/118.34 cnf(2713,plain, % 118.23/118.34 (P4(a1,a8,a8,a1,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[2421,2684,2698,2062,810,61,62,95,96,94,102,97])). % 118.23/118.34 cnf(2715,plain, % 118.23/118.34 (P4(a7,a7,a5,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2421,2684,2698,433,2062,810,61,62,95,96,94,102,97,98])). % 118.23/118.34 cnf(2722,plain, % 118.23/118.34 (P4(a8,a7,a2,a5,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[149,96])). % 118.23/118.34 cnf(2728,plain, % 118.23/118.34 (P4(a7,a7,a7,a1,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[2429,2466,2707,149,57,96,94,102,97])). % 118.23/118.34 cnf(2730,plain, % 118.23/118.34 (P4(a1,a1,a4,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[2629,2429,2466,2707,149,67,57,96,94,102,97,105])). % 118.23/118.34 cnf(2739,plain, % 118.23/118.34 (P4(a8,a7,a4,a6,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[164,96])). % 118.23/118.34 cnf(2747,plain, % 118.23/118.34 (P4(a8,a7,a2,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2481,2648,2722,525,164,61,96,94,102,97,98])). % 118.23/118.34 cnf(2751,plain, % 118.23/118.34 (P4(a8,a7,a1,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2481,2570,2648,2722,525,164,8,69,61,96,94,102,97,98,106,103])). % 118.23/118.34 cnf(2764,plain, % 118.23/118.34 (P4(a1,a1,a6,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2705,2593,295,2065,60,70,57,96,94,97,102,105])). % 118.23/118.34 cnf(2766,plain, % 118.23/118.34 (P4(a7,a7,a1,a8,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[2705,2593,2616,295,2065,60,70,58,57,96,94,97,102,105,98])). % 118.23/118.34 cnf(2768,plain, % 118.23/118.34 (P4(a8,a7,a1,a5,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2705,2646,2593,2616,295,2065,60,70,58,57,96,94,97,102,105,98,101])). % 118.23/118.34 cnf(2772,plain, % 118.23/118.34 (P4(a8,a1,a1,a5,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2705,2646,2593,2616,2287,295,2065,60,70,58,57,96,94,97,102,105,98,101,106,93])). % 118.23/118.34 cnf(2779,plain, % 118.23/118.34 (P4(a7,a8,a1,a8,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[2766,625,96,94])). % 118.23/118.34 cnf(2794,plain, % 118.23/118.34 (P4(a8,a8,a1,a7,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2071,2027,96,94])). % 118.23/118.34 cnf(2798,plain, % 118.23/118.34 (P4(a8,a7,a8,a5,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2637,2633,2071,2027,59,96,94,97,102])). % 118.23/118.34 cnf(2802,plain, % 118.23/118.34 (P4(a7,a8,a1,a8,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[2508,2637,2633,2779,2071,2027,59,65,61,96,94,97,102,105,98])). % 118.23/118.34 cnf(2817,plain, % 118.23/118.34 (P4(a8,a1,a1,a6,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2772,2692,515,2229,559,73,62,96,94,97,98,106])). % 118.23/118.34 cnf(2819,plain, % 118.23/118.34 (P4(a8,a8,a8,a2,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2772,2692,515,2229,559,73,62,96,94,97,98,106,329])). % 118.23/118.34 cnf(2821,plain, % 118.23/118.34 (P4(a8,a7,a8,a1,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[2772,2692,2665,515,2229,559,73,62,96,94,97,98,106,329,102])). % 118.23/118.34 cnf(2828,plain, % 118.23/118.34 (P4(a7,a8,a3,a5,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2262,132,96,94])). % 118.23/118.34 cnf(2832,plain, % 118.23/118.34 (P4(a1,a1,a5,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[2585,2673,2262,132,58,57,96,94,101,97])). % 118.23/118.34 cnf(2850,plain, % 118.23/118.34 (P4(a8,a1,a5,a1,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2535,2751,2828,107,58,61,96,94,101,97])). % 118.23/118.34 cnf(2852,plain, % 118.23/118.34 (P4(a7,a8,a3,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2535,2751,2266,2828,107,65,58,61,96,94,101,97,105])). % 118.23/118.34 cnf(2862,plain, % 118.23/118.34 (P4(a8,a7,a1,a6,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[111,96])). % 118.23/118.34 cnf(2910,plain, % 118.23/118.34 (P4(a8,a8,a8,a7,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2159,2044,96,94])). % 118.23/118.34 cnf(2914,plain, % 118.23/118.34 (P4(a8,a1,a8,a1,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2671,2516,2159,2044,57,61,96,94,101,97])). % 118.23/118.34 cnf(2916,plain, % 118.23/118.34 (P4(a7,a7,a6,a3,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[867,2671,2516,2159,2044,70,57,61,96,94,101,97,105])). % 118.23/118.34 cnf(2924,plain, % 118.23/118.34 (P4(a7,a8,a8,a7,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[356,2045,96,94])). % 118.23/118.34 cnf(2926,plain, % 118.23/118.34 (P4(a8,a8,a1,a5,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[2700,356,2045,62,96,94,101])). % 118.23/118.34 cnf(2930,plain, % 118.23/118.34 (P4(a1,a1,a3,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[2700,2522,527,356,2045,62,96,94,101,98,97])). % 118.23/118.34 cnf(2949,plain, % 118.23/118.34 (P4(a1,a8,a1,a2,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2739,2862,2566,583,75,71,69,58,96,94,101,105,106])). % 118.23/118.34 cnf(2957,plain, % 118.23/118.34 (P4(a8,a1,a1,a6,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2817,631,61,96,101])). % 118.23/118.34 cnf(2966,plain, % 118.23/118.34 (P4(a8,a8,a2,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[2568,132,71,96,105])). % 118.23/118.34 cnf(2968,plain, % 118.23/118.34 (P4(a8,a1,a8,a1,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2568,2914,132,71,58,96,105,102])). % 118.23/118.34 cnf(2980,plain, % 118.23/118.34 (P4(a8,a1,a1,a3,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2448,2574,2949,107,72,61,96,106,99,101])). % 118.23/118.34 cnf(2986,plain, % 118.23/118.34 (P4(a8,a1,a1,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2694,394,59,96,101])). % 118.23/118.34 cnf(2998,plain, % 118.23/118.34 (P4(a7,a8,a1,a8,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2802,60,101])). % 118.23/118.34 cnf(3002,plain, % 118.23/118.34 (P4(a1,a8,a1,a8,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2083,2802,60,70,101,106,95])). % 118.23/118.34 cnf(3021,plain, % 118.23/118.34 (P4(a1,a8,a1,a8,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3002,2589,69,62,106,101])). % 118.23/118.34 cnf(3023,plain, % 118.23/118.34 (P4(a8,a7,a8,a1,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3002,2589,2821,59,69,62,106,101,102])). % 118.23/118.34 cnf(3029,plain, % 118.23/118.34 (P4(a8,a8,a6,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2404,73,105])). % 118.23/118.34 cnf(3040,plain, % 118.23/118.34 (P4(a7,a7,a7,a4,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[875,2669,2373,74,106,104,105])). % 118.23/118.34 cnf(3042,plain, % 118.23/118.34 (P4(a8,a1,a3,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[875,2656,2669,2373,74,62,106,104,105,97])). % 118.23/118.34 cnf(3046,plain, % 118.23/118.34 (P4(a8,a1,a8,a1,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[2968,62,102])). % 118.23/118.34 cnf(3050,plain, % 118.23/118.34 (P4(a8,a1,a1,a8,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2850,2968,2986,58,57,62,102,97,98])). % 118.23/118.34 cnf(3059,plain, % 118.23/118.34 (P4(a8,a7,a8,a6,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2798,73,106])). % 118.23/118.34 cnf(3069,plain, % 118.23/118.34 (P4(a1,a7,a7,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2966,2728,2798,3050,2910,60,63,73,61,62,106,102,97,98,105,95])). % 118.23/118.34 cnf(3075,plain, % 118.23/118.34 (P4(a1,a1,a7,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3069,93])). % 118.23/118.34 cnf(3079,plain, % 118.23/118.34 (P4(a8,a1,a8,a1,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[3021,3046,3069,59,57,93,101,97])). % 118.23/118.34 cnf(3081,plain, % 118.23/118.34 (P4(a1,a8,a1,a8,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[3021,3046,3069,59,58,57,93,101,97,98])). % 118.23/118.34 cnf(3092,plain, % 118.23/118.34 (P4(a7,a7,a6,a6,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2916,70,106])). % 118.23/118.34 cnf(3094,plain, % 118.23/118.34 (P4(a1,a1,a7,a1,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3075,2916,70,61,106,97])). % 118.23/118.34 cnf(3096,plain, % 118.23/118.34 (P4(a1,a8,a1,a8,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[3075,2916,3081,70,61,62,106,97,98])). % 118.23/118.34 cnf(3098,plain, % 118.23/118.34 (P4(a1,a1,a5,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3075,2916,3081,70,68,61,62,106,97,98,105])). % 118.23/118.34 cnf(3102,plain, % 118.23/118.34 (P4(a8,a1,a8,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[3079,60,102])). % 118.23/118.34 cnf(3104,plain, % 118.23/118.34 (P4(a1,a1,a7,a1,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3079,3094,60,57,102,97])). % 118.23/118.34 cnf(3114,plain, % 118.23/118.34 (P4(a1,a1,a4,a1,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[2730,3102,61,102,97])). % 118.23/118.34 cnf(3129,plain, % 118.23/118.34 (P4(a1,a1,a4,a1,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[2926,3114,2541,59,73,57,106,102,97])). % 118.23/118.34 cnf(3131,plain, % 118.23/118.34 (P4(a7,a8,a1,a8,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[2926,3114,2998,2541,59,73,58,57,106,102,97,98])). % 118.23/118.34 cnf(3133,plain, % 118.23/118.34 (P4(a7,a8,a2,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2852,2926,3114,2998,2541,59,69,73,58,57,106,102,97,98,105])). % 118.23/118.34 cnf(3143,plain, % 118.23/118.34 (P4(a1,a1,a6,a1,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2764,3096,60,61,101,97])). % 118.23/118.34 cnf(3145,plain, % 118.23/118.34 (P4(a7,a8,a1,a8,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[2764,3096,3131,60,61,62,101,97,98])). % 118.23/118.34 cnf(3156,plain, % 118.23/118.34 (P4(a8,a1,a1,a2,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2980,3133,8,69,103,106])). % 118.23/118.34 cnf(3162,plain, % 118.23/118.34 (P4(a7,a7,a7,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2715,2980,3133,3143,2085,8,69,74,57,61,103,106,97,98,105])). % 118.23/118.34 cnf(3166,plain, % 118.23/118.34 (P4(a1,a1,a3,a1,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2930,59,97])). % 118.23/118.34 cnf(3177,plain, % 118.23/118.34 (P4(a1,a1,a5,a1,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3040,3098,71,62,106,97])). % 118.23/118.34 cnf(3179,plain, % 118.23/118.34 (P4(a8,a8,a3,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3029,3040,3098,71,65,62,106,97,105])). % 118.23/118.34 cnf(3183,plain, % 118.23/118.34 (P4(a1,a8,a8,a1,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[2713,60,102])). % 118.23/118.34 cnf(3185,plain, % 118.23/118.34 (P4(a8,a7,a8,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3023,2713,60,102,97])). % 118.23/118.34 cnf(3199,plain, % 118.23/118.34 (P4(a7,a8,a1,a8,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3059,3183,3145,65,61,106,102,101])). % 118.23/118.34 cnf(3203,plain, % 118.23/118.34 (P4(a7,a7,a2,a6,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2677,3059,3183,3185,3145,71,65,61,106,102,101,97,105])). % 118.23/118.34 cnf(3205,plain, % 118.23/118.34 (P4(a7,a7,a8,a6,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[2677,3059,3183,3185,3145,71,65,61,106,102,101,97,105,166])). % 118.23/118.34 cnf(3213,plain, % 118.23/118.34 (P4(a8,a1,a3,a1,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[3042,2819,59,62,102,97])). % 118.23/118.34 cnf(3226,plain, % 118.23/118.34 (P4(a7,a7,a1,a6,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3203,22,103])). % 118.23/118.34 cnf(3230,plain, % 118.23/118.34 (P4(a8,a1,a1,a6,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[3205,2957,3203,22,66,57,103,106,101])). % 118.23/118.34 cnf(3236,plain, % 118.23/118.34 (P4(a7,a7,a1,a6,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3226,58,101])). % 118.23/118.34 cnf(3240,plain, % 118.23/118.34 (P4(a7,a1,a1,a6,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2832,3226,73,58,101,105,93])). % 118.23/118.34 cnf(3242,plain, % 118.23/118.34 (P4(a1,a7,a1,a6,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[2832,3226,73,58,101,105,93,95])). % 118.23/118.34 cnf(3248,plain, % 118.23/118.34 (P4(a1,a1,a1,a6,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3242,93])). % 118.23/118.34 cnf(3256,plain, % 118.23/118.34 (P4(a1,a1,a1,a6,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3248,62,101])). % 118.23/118.34 cnf(3270,plain, % 118.23/118.34 (P4(a1,a7,a1,a8,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3177,3230,3199,495,2242,59,65,58,57,61,106,102,101,97,98])). % 118.23/118.34 cnf(3276,plain, % 118.23/118.34 (P4(a1,a7,a1,a8,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[3270,62,101])). % 118.23/118.34 cnf(3278,plain, % 118.23/118.34 (P4(a1,a7,a1,a8,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3270,62,101,98])). % 118.23/118.34 cnf(3280,plain, % 118.23/118.34 (P4(a7,a7,a5,a6,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3092,3270,66,62,101,98,105])). % 118.23/118.34 cnf(3286,plain, % 118.23/118.34 (P4(a1,a1,a1,a3,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3256,65,106])). % 118.23/118.34 cnf(3288,plain, % 118.23/118.34 (P4(a1,a7,a1,a8,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3256,3276,65,61,106,98])). % 118.23/118.34 cnf(3294,plain, % 118.23/118.34 (P4(a1,a7,a1,a8,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[3288,57,98])). % 118.23/118.34 cnf(3296,plain, % 118.23/118.34 (P4(a1,a1,a4,a1,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3104,3288,67,57,98,105])). % 118.23/118.34 cnf(3320,plain, % 118.23/118.34 (P4(a1,a7,a1,a8,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3278,61,101])). % 118.23/118.34 cnf(3322,plain, % 118.23/118.34 (P4(a1,a1,a4,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3296,3278,60,61,101,97])). % 118.23/118.34 cnf(3324,plain, % 118.23/118.34 (P4(a8,a7,a7,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3296,3278,661,60,61,101,97,98])). % 118.23/118.34 cnf(3331,plain, % 118.23/118.34 (P4(a7,a7,a5,a5,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3280,66,106])). % 118.23/118.34 cnf(3333,plain, % 118.23/118.34 (P4(a1,a1,a4,a1,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3280,3322,66,61,106,97])). % 118.23/118.34 cnf(3335,plain, % 118.23/118.34 (P4(a8,a7,a7,a8,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3280,3322,3324,66,57,61,106,97,98])). % 118.23/118.34 cnf(3337,plain, % 118.23/118.34 (P4(a1,a1,a2,a1,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[3129,3280,3322,3324,71,66,57,61,106,97,98,105])). % 118.23/118.34 cnf(3343,plain, % 118.23/118.34 (P4(a1,a7,a1,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3320,3337,59,97,98])). % 118.23/118.34 cnf(3357,plain, % 118.23/118.34 (P4(a1,a1,a2,a1,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[3166,3286,3343,69,58,106,98,105])). % 118.23/118.34 cnf(3363,plain, % 118.23/118.34 (P4(a7,a8,a6,a8,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[683,62,98])). % 118.23/118.34 cnf(3367,plain, % 118.23/118.34 (P4(a8,a8,a8,a6,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[2648,683,2747,62,98,104,102])). % 118.23/118.34 cnf(3371,plain, % 118.23/118.34 (P4(a7,a7,a5,a7,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3331,74,106])). % 118.23/118.34 cnf(3375,plain, % 118.23/118.34 (P4(a7,a1,a1,a6,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3294,3331,3240,74,62,106,105,101])). % 118.23/118.34 cnf(3377,plain, % 118.23/118.34 (P4(a7,a1,a1,a6,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3375,59,101])). % 118.23/118.34 cnf(3388,plain, % 118.23/118.34 (P4(a7,a7,a5,a4,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3213,3371,67,70,105,106])). % 118.23/118.34 cnf(3392,plain, % 118.23/118.34 (P4(a7,a7,a1,a8,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3213,3371,2526,2157,67,70,58,61,105,106,101,98])). % 118.23/118.34 cnf(3396,plain, % 118.23/118.34 (P4(a1,a1,a2,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3367,3213,3357,3371,2526,2157,67,70,58,61,105,106,101,98,100,97])). % 118.23/118.34 cnf(3400,plain, % 118.23/118.34 (P4(a1,a1,a2,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[3396,62,97])). % 118.23/118.34 cnf(3402,plain, % 118.23/118.34 (P4(a8,a8,a3,a8,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3396,3179,57,62,97,98])). % 118.23/118.34 cnf(3411,plain, % 118.23/118.34 (P4(a8,a7,a4,a8,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3335,67,105])). % 118.23/118.34 cnf(3413,plain, % 118.23/118.34 (P4(a7,a1,a1,a3,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3335,3377,67,65,105,106])). % 118.23/118.34 cnf(3415,plain, % 118.23/118.34 (P4(a1,a7,a3,a1,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3335,3377,2696,67,65,61,105,106,97])). % 118.23/118.34 cnf(3421,plain, % 118.23/118.34 (P4(a7,a8,a8,a5,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3335,3363,3377,2696,630,792,67,65,61,105,106,97,98,104,102])). % 118.23/118.34 cnf(3423,plain, % 118.23/118.34 (P4(a7,a8,a8,a5,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3421,57,102])). % 118.23/118.34 cnf(3425,plain, % 118.23/118.34 (P4(a7,a1,a1,a3,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3421,3413,57,102,101])). % 118.23/118.34 cnf(3432,plain, % 118.23/118.34 (P4(a7,a7,a6,a4,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3388,73,105])). % 118.23/118.34 cnf(3434,plain, % 118.23/118.34 (P4(a7,a8,a8,a1,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[3388,2667,73,62,105,102])). % 118.23/118.34 cnf(3440,plain, % 118.23/118.34 (P4(a7,a1,a1,a8,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3388,3392,3236,2667,73,62,105,102,101,98,93])). % 118.23/118.34 cnf(3447,plain, % 118.23/118.34 (P4(a7,a8,a8,a7,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3423,74,106])). % 118.23/118.34 cnf(3449,plain, % 118.23/118.34 (P4(a7,a7,a7,a8,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3423,3162,74,57,106,98])). % 118.23/118.34 cnf(3456,plain, % 118.23/118.34 (P4(a7,a8,a8,a1,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3402,3434,69,59,105,102])). % 118.23/118.34 cnf(3460,plain, % 118.23/118.34 (P4(a8,a8,a2,a8,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3402,3434,3440,522,69,59,61,105,102,101,98])). % 118.23/118.34 cnf(3479,plain, % 118.23/118.34 (P4(a1,a7,a6,a1,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3415,70,105])). % 118.23/118.34 cnf(3481,plain, % 118.23/118.34 (P4(a7,a7,a6,a7,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3415,3432,72,70,105,106])). % 118.23/118.34 cnf(3485,plain, % 118.23/118.34 (P4(a7,a8,a8,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3415,3432,3447,3456,72,60,70,59,105,106,102,97])). % 118.23/118.34 cnf(3497,plain, % 118.23/118.34 (P4(a7,a7,a1,a4,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3485,270,2924,58,61,102,97,101])). % 118.23/118.34 cnf(3501,plain, % 118.23/118.34 (P4(a1,a8,a8,a7,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3485,270,2924,58,61,102,97,101,93,95])). % 118.23/118.34 cnf(3503,plain, % 118.23/118.34 (P4(a8,a7,a1,a4,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3485,270,2924,58,61,102,97,101,93,95,96])). % 118.23/118.34 cnf(3512,plain, % 118.23/118.34 (P4(a8,a1,a1,a4,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3503,93])). % 118.23/118.34 cnf(3514,plain, % 118.23/118.34 (P4(a1,a7,a1,a4,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3497,3503,93,95])). % 118.23/118.34 cnf(3516,plain, % 118.23/118.34 (P4(a8,a7,a2,a8,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3411,3497,3503,71,93,95,105])). % 118.23/118.34 cnf(3520,plain, % 118.23/118.34 (P4(a1,a7,a6,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3411,3425,3479,3497,3503,71,69,58,93,95,105,106,97])). % 118.23/118.34 cnf(3533,plain, % 118.23/118.34 (P4(a1,a1,a1,a4,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3514,93])). % 118.23/118.34 cnf(3537,plain, % 118.23/118.34 (P4(a1,a8,a8,a7,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3501,3514,3516,8,57,93,103,102])). % 118.23/118.34 cnf(3539,plain, % 118.23/118.34 (P4(a1,a7,a6,a1,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3501,3514,3516,3520,8,57,62,93,103,102,97])). % 118.23/118.34 cnf(3541,plain, % 118.23/118.34 (P4(a8,a1,a1,a4,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[3512,3501,3514,3516,3520,8,57,62,93,103,102,97,101])). % 118.23/118.34 cnf(3552,plain, % 118.23/118.34 (P4(a1,a7,a5,a1,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3539,66,105])). % 118.23/118.34 cnf(3556,plain, % 118.23/118.34 (P4(a7,a8,a8,a4,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3533,3539,499,72,66,61,105,106,102])). % 118.23/118.34 cnf(3558,plain, % 118.23/118.34 (P4(a1,a7,a8,a1,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3533,3539,2209,499,72,66,61,105,106,102,97])). % 118.23/118.34 cnf(3577,plain, % 118.23/118.34 (P4(a7,a7,a3,a7,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3481,65,105])). % 118.23/118.34 cnf(3583,plain, % 118.23/118.34 (P4(a8,a1,a1,a4,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[3481,3541,3556,3558,71,60,65,59,105,106,102,101])). % 118.23/118.34 cnf(3585,plain, % 118.23/118.34 (P4(a8,a7,a6,a8,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3481,3541,3556,3558,706,71,60,65,59,62,105,106,102,101,98])). % 118.23/118.34 cnf(3602,plain, % 118.23/118.34 (P4(a7,a7,a2,a7,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3577,69,105])). % 118.23/118.34 cnf(3604,plain, % 118.23/118.34 (P4(a8,a1,a1,a7,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[3583,3577,72,69,105,106])). % 118.23/118.34 cnf(3606,plain, % 118.23/118.34 (P4(a8,a7,a8,a6,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3583,3577,2627,72,69,62,105,106,102])). % 118.23/118.34 cnf(3612,plain, % 118.23/118.34 (P4(a7,a7,a1,a7,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3602,29,103])). % 118.23/118.34 cnf(3622,plain, % 118.23/118.34 (P4(a7,a7,a1,a4,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3612,67,106])). % 118.23/118.34 cnf(3624,plain, % 118.23/118.34 (P4(a1,a7,a5,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3612,3552,67,60,106,97])). % 118.23/118.34 cnf(3626,plain, % 118.23/118.34 (P4(a7,a7,a1,a7,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3612,3552,67,60,58,106,97,101])). % 118.23/118.34 cnf(3630,plain, % 118.23/118.34 (P4(a1,a7,a1,a7,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3612,3552,67,60,58,106,97,101,93,95])). % 118.23/118.34 cnf(3637,plain, % 118.23/118.34 (P4(a1,a1,a1,a7,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3630,93])). % 118.23/118.34 cnf(3641,plain, % 118.23/118.34 (P4(a1,a7,a5,a1,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3624,3630,3449,68,61,93,105,97])). % 118.23/118.34 cnf(3643,plain, % 118.23/118.34 (P4(a7,a7,a1,a4,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3622,3624,3630,3449,68,58,61,93,105,97,101])). % 118.23/118.34 cnf(3645,plain, % 118.23/118.34 (P4(a1,a7,a1,a4,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3622,3624,3630,3449,68,58,61,93,105,97,101,95])). % 118.23/118.34 cnf(3649,plain, % 118.23/118.34 (P4(a7,a7,a1,a5,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3606,3622,3624,3626,3630,3449,68,58,61,93,105,97,101,95,100,106])). % 118.23/118.34 cnf(3651,plain, % 118.23/118.34 (P4(a8,a7,a8,a4,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3606,3622,3624,3626,3630,3449,572,68,58,61,93,105,97,101,95,100,106,102])). % 118.23/118.34 cnf(3655,plain, % 118.23/118.34 (P4(a1,a7,a1,a5,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3643,3649,93,95])). % 118.23/118.34 cnf(3657,plain, % 118.23/118.34 (P4(a8,a7,a8,a4,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3651,3643,3649,57,93,95,102])). % 118.23/118.34 cnf(3659,plain, % 118.23/118.34 (P4(a7,a1,a8,a1,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[3651,3643,3649,2211,57,62,93,95,102,97])). % 118.23/118.34 cnf(3661,plain, % 118.23/118.34 (P4(a1,a1,a1,a7,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3637,3651,3643,3649,2211,57,62,93,95,102,97,101])). % 118.23/118.34 cnf(3672,plain, % 118.23/118.34 (P4(a1,a7,a7,a1,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3645,3641,74,93,105])). % 118.23/118.34 cnf(3674,plain, % 118.23/118.34 (P4(a8,a7,a8,a7,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3645,3641,3657,72,74,93,105,106])). % 118.23/118.34 cnf(3676,plain, % 118.23/118.34 (P4(a7,a1,a8,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[3645,3641,3657,3659,72,74,60,93,105,106,102])). % 118.23/118.34 cnf(3678,plain, % 118.23/118.34 (P4(a1,a1,a1,a7,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3645,3641,3657,3659,3661,72,74,60,59,93,105,106,102,101])). % 118.23/118.34 cnf(3684,plain, % 118.23/118.34 (P4(a1,a1,a1,a5,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3655,93])). % 118.23/118.34 cnf(3688,plain, % 118.23/118.34 (P4(a1,a7,a1,a5,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3655,3674,59,61,93,102,101])). % 118.23/118.34 cnf(3703,plain, % 118.23/118.34 (P4(a1,a1,a4,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[3400,3649,542,64,62,93,98,105])). % 118.23/118.34 cnf(3707,plain, % 118.23/118.34 (P4(a7,a7,a8,a5,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3400,3678,3649,396,542,64,67,62,93,98,105,106,102])). % 118.23/118.34 cnf(3713,plain, % 118.23/118.34 (P4(a7,a1,a8,a1,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3676,61,102])). % 118.23/118.34 cnf(3715,plain, % 118.23/118.34 (P4(a1,a1,a4,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3703,3676,60,61,102,97])). % 118.23/118.34 cnf(3717,plain, % 118.23/118.34 (P4(a1,a1,a1,a5,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3684,3703,3676,60,61,102,97,101])). % 118.23/118.34 cnf(3728,plain, % 118.23/118.34 (P4(a1,a7,a4,a1,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3672,67,105])). % 118.23/118.34 cnf(3734,plain, % 118.23/118.34 (P4(a1,a1,a4,a1,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[3672,3688,3715,2065,67,73,61,105,106,102,97])). % 118.23/118.34 cnf(3741,plain, % 118.23/118.34 (P4(a7,a1,a8,a1,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[3713,59,97])). % 118.23/118.34 cnf(3756,plain, % 118.23/118.34 (P4(a1,a7,a4,a1,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3707,3728,71,74,58,105,106,97])). % 118.23/118.34 cnf(3764,plain, % 118.23/118.34 (P4(a1,a7,a4,a1,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3756,62,97])). % 118.23/118.34 cnf(3777,plain, % 118.23/118.34 (P4(a1,a8,a7,a1,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[3717,3764,2102,71,73,61,105,106,97])). % 118.23/118.34 cnf(3779,plain, % 118.23/118.34 (P4(a1,a7,a8,a1,a6,a2)), % 118.23/118.34 inference(scs_inference,[],[3717,3764,2102,71,73,61,105,106,97,157])). % 118.23/118.34 cnf(3781,plain, % 118.23/118.34 (P4(a7,a1,a8,a1,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[3741,58,102])). % 118.23/118.34 cnf(3792,plain, % 118.23/118.34 (P4(a1,a7,a8,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[3779,3333,71,58,105,102])). % 118.23/118.34 cnf(3808,plain, % 118.23/118.34 (P4(a7,a7,a1,a3,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[130,2077,554,58,61,102,105,101])). % 118.23/118.34 cnf(3819,plain, % 118.23/118.34 (P4(a1,a7,a1,a3,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3808,95])). % 118.23/118.34 cnf(3821,plain, % 118.23/118.34 (P4(a7,a1,a1,a3,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3808,95,93])). % 118.23/118.34 cnf(3825,plain, % 118.23/118.34 (P4(a1,a1,a7,a1,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[3734,3808,72,95,93,96,105])). % 118.23/118.34 cnf(3829,plain, % 118.23/118.34 (P4(a7,a7,a1,a3,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[3734,3808,3781,72,62,95,93,96,105,102,101])). % 118.23/118.34 cnf(3831,plain, % 118.23/118.34 (P4(a7,a8,a1,a3,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[3734,3808,3781,72,62,95,93,96,105,102,101,94])). % 118.23/118.34 cnf(3837,plain, % 118.23/118.34 (P4(a1,a1,a1,a3,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3821,95])). % 118.23/118.34 cnf(3841,plain, % 118.23/118.34 (P4(a8,a7,a8,a7,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3821,3829,2044,61,95,96,102])). % 118.23/118.34 cnf(3845,plain, % 118.23/118.34 (P4(a1,a7,a1,a3,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[3819,3821,3825,3829,2044,57,61,95,96,102,97,101])). % 118.23/118.34 cnf(3856,plain, % 118.23/118.34 (P4(a1,a8,a5,a1,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[3777,68,105])). % 118.23/118.34 cnf(3860,plain, % 118.23/118.34 (P4(a7,a8,a1,a6,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[3831,3841,3777,68,70,57,105,102,106])). % 118.23/118.34 cnf(3862,plain, % 118.23/118.34 (P4(a7,a7,a6,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3831,3841,3777,912,68,70,58,57,105,102,106,97])). % 118.23/118.34 cnf(3868,plain, % 118.23/118.34 (P4(a7,a1,a6,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3831,3841,3845,3777,912,68,70,58,57,105,102,106,97,101,113,93])). % 118.23/118.34 cnf(3870,plain, % 118.23/118.34 (P4(a1,a7,a6,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3831,3841,3845,3777,912,68,70,58,57,105,102,106,97,101,113,93,95])). % 118.23/118.34 cnf(3872,plain, % 118.23/118.34 (P4(a1,a1,a6,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3868,95])). % 118.23/118.34 cnf(3874,plain, % 118.23/118.34 (P4(a7,a7,a8,a7,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3868,2045,61,95,102])). % 118.23/118.34 cnf(3876,plain, % 118.23/118.34 (P4(a1,a7,a6,a1,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3870,3868,2045,61,95,102,97])). % 118.23/118.34 cnf(3878,plain, % 118.23/118.34 (P4(a1,a1,a1,a3,a2,a7)), % 118.23/118.34 inference(scs_inference,[],[3837,3870,3868,2045,61,95,102,97,101])). % 118.23/118.34 cnf(3885,plain, % 118.23/118.34 (P4(a7,a7,a8,a7,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3874,57,102])). % 118.23/118.34 cnf(3887,plain, % 118.23/118.34 (P4(a1,a1,a6,a1,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[3872,3874,57,62,102,97])). % 118.23/118.34 cnf(3889,plain, % 118.23/118.34 (P4(a1,a1,a1,a3,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[3872,3874,3878,57,62,102,97,101])). % 118.23/118.34 cnf(3893,plain, % 118.23/118.34 (P4(a1,a7,a8,a7,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3872,3874,3878,57,62,102,97,101,93,95])). % 118.23/118.34 cnf(3906,plain, % 118.23/118.34 (P4(a1,a1,a5,a1,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[3887,3893,66,93,105])). % 118.23/118.34 cnf(3908,plain, % 118.23/118.34 (P4(a7,a7,a8,a4,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3887,3885,3893,66,67,93,105,106])). % 118.23/118.34 cnf(3914,plain, % 118.23/118.34 (P4(a7,a8,a1,a6,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3887,3885,3893,3860,3792,66,67,60,59,62,93,105,106,102,97,101])). % 118.23/118.34 cnf(3916,plain, % 118.23/118.34 (P4(a1,a7,a8,a4,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3887,3885,3893,3860,3792,66,67,60,59,62,93,105,106,102,97,101,95])). % 118.23/118.34 cnf(3923,plain, % 118.23/118.34 (P4(a7,a1,a8,a4,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3908,93])). % 118.23/118.34 cnf(3925,plain, % 118.23/118.34 (P4(a1,a8,a1,a6,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3908,3914,93,95])). % 118.23/118.34 cnf(3927,plain, % 118.23/118.34 (P4(a1,a1,a5,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3906,3908,3914,60,93,95,97])). % 118.23/118.34 cnf(3942,plain, % 118.23/118.34 (P4(a1,a7,a8,a4,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3916,3856,73,60,93,105,102])). % 118.23/118.34 cnf(3944,plain, % 118.23/118.34 (P4(a1,a7,a8,a2,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3916,3856,71,73,60,93,105,102,106])). % 118.23/118.34 cnf(3946,plain, % 118.23/118.34 (P4(a1,a1,a5,a1,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3916,3856,3927,71,73,60,61,93,105,102,106,97])). % 118.23/118.34 cnf(3950,plain, % 118.23/118.34 (P4(a1,a8,a8,a4,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3916,3856,3925,3927,71,73,60,62,61,93,105,102,106,97,101,94])). % 118.23/118.34 cnf(3959,plain, % 118.23/118.34 (P4(a7,a1,a8,a4,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3923,3942,60,93,102])). % 118.23/118.34 cnf(3961,plain, % 118.23/118.34 (P4(a7,a7,a6,a1,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[3923,3942,3862,60,62,93,102,97])). % 118.23/118.34 cnf(3965,plain, % 118.23/118.34 (P4(a8,a1,a8,a4,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3923,3942,3862,2768,60,62,93,102,97,101,96])). % 118.23/118.34 cnf(3971,plain, % 118.23/118.34 (P4(a1,a1,a8,a2,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3944,93])). % 118.23/118.34 cnf(3973,plain, % 118.23/118.34 (P4(a7,a7,a3,a1,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[3944,3961,65,93,105])). % 118.23/118.34 cnf(3986,plain, % 118.23/118.34 (P4(a1,a8,a8,a2,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3950,71,61,102,106])). % 118.23/118.34 cnf(3990,plain, % 118.23/118.34 (P4(a1,a7,a3,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3950,3973,71,60,61,102,106,97,95])). % 118.23/118.34 cnf(3992,plain, % 118.23/118.34 (P4(a7,a1,a3,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3950,3973,71,60,61,102,106,97,95,93])). % 118.23/118.34 cnf(4001,plain, % 118.23/118.34 (P4(a1,a7,a5,a1,a2,a6)), % 118.23/118.34 inference(scs_inference,[],[3992,3876,66,95,105])). % 118.23/118.34 cnf(4003,plain, % 118.23/118.34 (P4(a1,a1,a8,a2,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[3971,3992,3876,66,59,95,105,102])). % 118.23/118.34 cnf(4010,plain, % 118.23/118.34 (P4(a8,a1,a8,a4,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3965,62,102])). % 118.23/118.34 cnf(4012,plain, % 118.23/118.34 (P4(a1,a1,a1,a6,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[3965,3889,70,62,102,106])). % 118.23/118.34 cnf(4020,plain, % 118.23/118.34 (P4(a1,a7,a5,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[4001,58,97])). % 118.23/118.34 cnf(4026,plain, % 118.23/118.34 (P4(a1,a8,a8,a3,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[3986,4001,4012,3460,63,60,58,97,101,104,106])). % 118.23/118.34 cnf(4031,plain, % 118.23/118.34 (P4(a1,a1,a8,a2,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[4003,58,102])). % 118.23/118.34 cnf(4033,plain, % 118.23/118.34 (P4(a1,a7,a5,a1,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[4003,4020,58,62,102,97])). % 118.23/118.34 cnf(4041,plain, % 118.23/118.34 (P4(a8,a1,a8,a4,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[4010,59,102])). % 118.23/118.34 cnf(4054,plain, % 118.23/118.34 (P4(a1,a8,a8,a3,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[4026,4033,73,61,105,102])). % 118.23/118.34 cnf(4063,plain, % 118.23/118.34 (P4(a1,a1,a8,a3,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[4031,3959,63,61,102,106])). % 118.23/118.34 cnf(4071,plain, % 118.23/118.34 (P4(a1,a1,a8,a3,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[3946,4063,74,62,105,102])). % 118.23/118.34 cnf(4073,plain, % 118.23/118.34 (P4(a1,a7,a3,a1,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[3946,4063,3990,74,62,105,102,97])). % 118.23/118.34 cnf(4080,plain, % 118.23/118.34 (P4(a1,a1,a8,a3,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[4063,61,102])). % 118.23/118.34 cnf(4082,plain, % 118.23/118.34 (P4(a1,a8,a8,a6,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[4054,4063,70,61,102,106])). % 118.23/118.34 cnf(4097,plain, % 118.23/118.34 (P4(a1,a1,a8,a6,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[4071,70,106])). % 118.23/118.34 cnf(4120,plain, % 118.23/118.34 (P4(a1,a7,a2,a1,a6,a6)), % 118.23/118.34 inference(scs_inference,[],[4041,4073,69,71,106,105])). % 118.23/118.34 cnf(4122,plain, % 118.23/118.34 (P4(a1,a8,a8,a6,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[4041,4082,4073,69,71,58,106,105,102])). % 118.23/118.34 cnf(4126,plain, % 118.23/118.34 (P4(a1,a7,a2,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[4120,60,97])). % 118.23/118.34 cnf(4128,plain, % 118.23/118.34 (P4(a1,a8,a8,a6,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[4120,4122,60,62,97,102])). % 118.23/118.34 cnf(4145,plain, % 118.23/118.34 (P4(a1,a1,a8,a6,a7,a2)), % 118.23/118.34 inference(scs_inference,[],[4080,4126,70,61,97,106])). % 118.23/118.34 cnf(4155,plain, % 118.23/118.34 (P4(a1,a1,a8,a6,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[4145,58,102])). % 118.23/118.34 cnf(4173,plain, % 118.23/118.34 (P4(a7,a7,a3,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[4128,264,65,58,106,97])). % 118.23/118.34 cnf(4179,plain, % 118.23/118.34 (P4(a1,a7,a3,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[4128,264,199,2470,65,58,61,106,97,101,103,95])). % 118.23/118.34 cnf(4188,plain, % 118.23/118.34 (P4(a8,a7,a3,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[4173,96])). % 118.23/118.34 cnf(4190,plain, % 118.23/118.34 (P4(a7,a7,a3,a1,a6,a7)), % 118.23/118.34 inference(scs_inference,[],[4173,62,96,97])). % 118.23/118.34 cnf(4211,plain, % 118.23/118.34 (P4(a8,a1,a2,a1,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[4188,4155,4190,4179,66,69,61,96,97,106,105,93])). % 118.23/118.34 cnf(4365,plain, % 118.23/118.34 (~P4(a1,a6,a1,a1,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[61,58,69,2023,2029,2373,3808,2044,2379,2087,2188,2949,3357,2794,3501,3604,86,85,91,92,119,121,88,87,89,90,142,140,106,97,102,101])). % 118.23/118.34 cnf(4373,plain, % 118.23/118.34 (~P4(a1,a6,a6,a7,a7,a7)), % 118.23/118.34 inference(scs_inference,[],[61,58,69,2023,2029,2373,3808,2044,2379,2437,2087,2188,2949,3357,2794,3501,3604,86,85,91,92,119,121,88,87,89,90,142,140,106,97,102,101,98,95,229,457])). % 118.23/118.34 cnf(4385,plain, % 118.23/118.34 (P4(a1,a6,a8,a1,a7,a6)), % 118.23/118.34 inference(scs_inference,[],[2373,3585,3357,4373,3537,85,95,91,92,119,121])). % 118.23/118.34 cnf(4441,plain, % 118.23/118.34 (~P4(a1,a6,a5,a2,a2,a2)), % 118.23/118.34 inference(scs_inference,[],[61,58,68,2045,3363,2949,4097,2747,2085,2122,4063,2477,2254,2250,2365,3604,4365,85,95,91,92,88,87,89,90,140,86,106,97,102,101,98,419])). % 118.23/118.34 cnf(4535,plain, % 118.23/118.34 ($false), % 118.23/118.34 inference(scs_inference,[],[58,59,3460,3156,3916,3501,4211,3986,3230,2386,2153,4441,4385,95,88,89,90,87,85,91,86,92,333,119,117,101,102]), % 118.23/118.34 ['proof']). % 118.23/118.34 % SZS output end Proof % 118.23/118.34 % Total time :117.800000s %------------------------------------------------------------------------------