%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COL035-1 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n008.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 04:44:51 EDT 2024 % Result : Unsatisfiable 69.01s 69.14s % Output : CNFRefutation 69.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : COL035-1 : TPTP v8.2.0. Released v1.0.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.35 % Computer : n008.cluster.edu % 0.12/0.35 % Model : x86_64 x86_64 % 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.35 % Memory : 8042.1875MB % 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.35 % CPULimit : 300 % 0.12/0.35 % WCLimit : 300 % 0.12/0.35 % DateTime : Tue Jun 18 15:58:09 EDT 2024 % 0.12/0.35 % CPUTime : % 0.53/0.57 start to proof:theBenchmark % 69.01/69.12 %------------------------------------------- % 69.01/69.12 % File :CSE---1.7 % 69.01/69.12 % Problem :theBenchmark % 69.01/69.12 % Transform :cnf % 69.01/69.12 % Format :tptp:raw % 69.01/69.12 % Command :java -jar mcs_scs.jar %d %s % 69.01/69.12 % 69.01/69.12 % Result :Theorem 68.500000s % 69.01/69.12 % Output :CNFRefutation 68.500000s % 69.01/69.12 %------------------------------------------- % 69.01/69.13 %-------------------------------------------------------------------------- % 69.01/69.13 % File : COL035-1 : TPTP v8.2.0. Released v1.0.0. % 69.01/69.13 % Domain : Combinatory Logic % 69.01/69.13 % Problem : Strong fixed point for W, Q, and L % 69.01/69.13 % Version : [WM88] (equality) axioms. % 69.01/69.13 % English : The strong fixed point property holds for the set % 69.01/69.13 % P consisting of the combinators W, Q, and L, where (Lx)y % 69.01/69.13 % = x(yy), (Wx)y = (xy)y, ((Qx)y)z = y(xz). % 69.01/69.13 % 69.01/69.13 % Refs : [Smu85] Smullyan (1978), To Mock a Mocking Bird and Other Logi % 69.01/69.14 % : [MW87] McCune & Wos (1987), A Case Study in Automated Theorem % 69.01/69.14 % : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq % 69.01/69.14 % : [MW88] McCune & Wos (1988), Some Fixed Point Problems in Comb % 69.01/69.14 % Source : [MW88] % 69.01/69.14 % Names : - [MW88] % 69.01/69.14 % 69.01/69.14 % Status : Unsatisfiable % 69.01/69.14 % Rating : 0.23 v8.2.0, 0.29 v8.1.0, 0.30 v7.5.0, 0.33 v7.4.0, 0.39 v7.3.0, 0.37 v7.1.0, 0.28 v7.0.0, 0.26 v6.4.0, 0.32 v6.3.0, 0.29 v6.1.0, 0.31 v6.0.0, 0.33 v5.5.0, 0.37 v5.4.0, 0.33 v5.3.0, 0.42 v5.2.0, 0.36 v5.1.0, 0.40 v5.0.0, 0.36 v4.1.0, 0.18 v4.0.1, 0.29 v4.0.0, 0.31 v3.7.0, 0.11 v3.4.0, 0.12 v3.3.0, 0.21 v3.2.0, 0.14 v3.1.0, 0.22 v2.7.0, 0.09 v2.6.0, 0.17 v2.5.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.00 v2.1.0, 0.25 v2.0.0 % 69.01/69.14 % Syntax : Number of clauses : 4 ( 4 unt; 0 nHn; 1 RR) % 69.01/69.14 % Number of literals : 4 ( 4 equ; 1 neg) % 69.01/69.14 % Maximal clause size : 1 ( 1 avg) % 69.01/69.14 % Maximal term depth : 4 ( 2 avg) % 69.01/69.14 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 69.01/69.14 % Number of functors : 5 ( 5 usr; 3 con; 0-2 aty) % 69.01/69.14 % Number of variables : 8 ( 0 sgn) % 69.01/69.14 % SPC : CNF_UNS_RFO_PEQ_UEQ % 69.01/69.14 % 69.01/69.14 % Comments : % 69.01/69.14 %-------------------------------------------------------------------------- % 69.01/69.14 cnf(l_definition,axiom, % 69.01/69.14 apply(apply(l,X),Y) = apply(X,apply(Y,Y)) ). % 69.01/69.14 % 69.01/69.14 cnf(w_definition,axiom, % 69.01/69.14 apply(apply(w,X),Y) = apply(apply(X,Y),Y) ). % 69.01/69.14 % 69.01/69.14 cnf(q_definition,axiom, % 69.01/69.14 apply(apply(apply(q,X),Y),Z) = apply(Y,apply(X,Z)) ). % 69.01/69.14 % 69.01/69.14 cnf(prove_fixed_point,negated_conjecture, % 69.01/69.14 apply(Y,f(Y)) != apply(f(Y),apply(Y,f(Y))) ). % 69.01/69.14 % 69.01/69.14 %-------------------------------------------------------------------------- % 69.01/69.14 %------------------------------------------- % 69.01/69.14 % Proof found % 69.01/69.14 % SZS status Theorem for theBenchmark % 69.01/69.14 % SZS output start Proof % 69.11/69.15 %ClaNum:10(EqnAxiom:6) % 69.11/69.15 %VarNum:21(SingletonVarNum:8) % 69.11/69.15 %MaxLitNum:1 % 69.11/69.15 %MaxfuncDepth:3 % 69.11/69.15 %SharedTerms:3 % 69.11/69.15 %goalClause: 10 % 69.11/69.15 %singleGoalClaCount:1 % 69.11/69.15 [10]~E(f2(f3(x101),f2(x101,f3(x101))),f2(x101,f3(x101))) % 69.11/69.15 [7]E(f2(f2(a1,x71),x72),f2(x71,f2(x72,x72))) % 69.11/69.15 [8]E(f2(f2(a4,x81),x82),f2(f2(x81,x82),x82)) % 69.11/69.15 [9]E(f2(f2(f2(a5,x91),x92),x93),f2(x92,f2(x91,x93))) % 69.11/69.15 %EqnAxiom % 69.11/69.15 [1]E(x11,x11) % 69.11/69.15 [2]E(x22,x21)+~E(x21,x22) % 69.11/69.15 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 69.11/69.15 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 69.11/69.15 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 69.11/69.15 [6]~E(x61,x62)+E(f3(x61),f3(x62)) % 69.11/69.15 % 69.11/69.15 %------------------------------------------- % 69.11/69.16 cnf(12,plain, % 69.11/69.16 (E(f2(f2(a4,a1),x121),f2(x121,f2(x121,x121)))), % 69.11/69.16 inference(scs_inference,[],[7,8,2,3])). % 69.11/69.16 cnf(15,plain, % 69.11/69.16 (E(f2(x151,f2(x151,x151)),f2(f2(a4,a1),x151))), % 69.11/69.16 inference(scs_inference,[],[12,2])). % 69.11/69.16 cnf(16,plain, % 69.11/69.16 (E(f2(x161,f2(x162,x163)),f2(f2(f2(a5,x162),x161),x163))), % 69.11/69.16 inference(scs_inference,[],[9,2])). % 69.11/69.16 cnf(17,plain, % 69.11/69.16 (E(f2(f2(x171,x172),x172),f2(f2(a4,x171),x172))), % 69.11/69.16 inference(scs_inference,[],[8,2])). % 69.11/69.16 cnf(18,plain, % 69.11/69.16 (E(f2(f2(a4,a4),a1),f2(a1,f2(a1,a1)))), % 69.11/69.16 inference(scs_inference,[],[8,12,3])). % 69.11/69.16 cnf(21,plain, % 69.11/69.16 (E(f2(a1,f2(a1,a1)),f2(f2(a4,a4),a1))), % 69.11/69.16 inference(scs_inference,[],[8,12,3,2])). % 69.11/69.16 cnf(22,plain, % 69.11/69.16 (E(f2(f2(a4,f2(a5,x221)),x222),f2(x222,f2(x221,x222)))), % 69.11/69.16 inference(scs_inference,[],[8,9,3])). % 69.11/69.16 cnf(25,plain, % 69.11/69.16 (E(f2(x251,f2(x252,x251)),f2(f2(a4,f2(a5,x252)),x251))), % 69.11/69.16 inference(scs_inference,[],[8,9,3,2])). % 69.11/69.16 cnf(28,plain, % 69.11/69.16 (E(f2(f2(a4,a4),a1),f2(f2(a4,f2(a5,a1)),a1))), % 69.11/69.16 inference(scs_inference,[],[21,22,3,2])). % 69.11/69.16 cnf(29,plain, % 69.11/69.16 (E(f2(f2(a4,a1),a1),f2(f2(a4,f2(a5,a1)),a1))), % 69.11/69.16 inference(scs_inference,[],[17,28,3])). % 69.11/69.16 cnf(35,plain, % 69.11/69.16 (E(f2(f2(a5,x351),f2(x351,f2(a5,x351))),f2(f2(a4,a4),f2(a5,x351)))), % 69.11/69.16 inference(scs_inference,[],[8,22,3,2])). % 69.11/69.16 cnf(36,plain, % 69.11/69.16 (E(f2(f2(f2(a5,x361),f2(a5,x361)),f2(a5,x361)),f2(f2(a4,a4),f2(a5,x361)))), % 69.11/69.16 inference(scs_inference,[],[9,35,3])). % 69.11/69.16 cnf(40,plain, % 69.11/69.16 (E(f2(f2(f2(a5,a1),a1),a1),f2(f2(a4,a4),a1))), % 69.11/69.16 inference(scs_inference,[],[9,21,36,2,3])). % 69.11/69.16 cnf(52,plain, % 69.11/69.16 (E(f2(f2(a4,f2(a5,a1)),a1),f2(f2(a1,a1),a1))), % 69.11/69.16 inference(scs_inference,[],[17,29,3,2])). % 69.11/69.16 cnf(55,plain, % 69.11/69.16 (E(f2(f2(a1,a1),a1),f2(f2(f2(a5,a1),a1),a1))), % 69.11/69.16 inference(scs_inference,[],[17,52,3,2])). % 69.11/69.16 cnf(56,plain, % 69.11/69.16 (E(f2(f2(a1,a1),a1),f2(f2(a4,a4),a1))), % 69.11/69.16 inference(scs_inference,[],[55,40,3])). % 69.11/69.16 cnf(89,plain, % 69.11/69.16 (~E(f2(f2(f2(a5,x891),f3(x891)),f3(x891)),f2(x891,f3(x891)))), % 69.11/69.16 inference(scs_inference,[],[7,16,10,6,4,5,2,3])). % 69.11/69.16 cnf(96,plain, % 69.11/69.16 (~E(f2(f2(a4,f2(a5,x961)),f3(x961)),f2(x961,f3(x961)))), % 69.11/69.16 inference(scs_inference,[],[18,89,25,10,6,5,4,2,3])). % 69.11/69.16 cnf(101,plain, % 69.11/69.16 (~E(f2(x1011,f3(x1011)),f2(f2(a4,f2(a5,x1011)),f3(x1011)))), % 69.11/69.16 inference(scs_inference,[],[56,96,6,4,5,2])). % 69.11/69.16 cnf(110,plain, % 69.11/69.16 (E(f2(x1101,f2(x1102,f2(x1102,x1102))),f2(x1101,f2(f2(a4,a1),x1102)))), % 69.11/69.16 inference(scs_inference,[],[15,6,4,5])). % 69.11/69.16 cnf(114,plain, % 69.11/69.16 (E(f2(x1141,f2(x1142,f2(x1143,x1143))),f2(x1141,f2(f2(a1,x1142),x1143)))), % 69.11/69.16 inference(scs_inference,[],[7,2,5])). % 69.11/69.16 cnf(451,plain, % 69.11/69.16 (~E(x4511,f2(a5,f2(a4,x4511)))), % 69.11/69.16 inference(scs_inference,[],[101,4,5])). % 69.11/69.16 cnf(452,plain, % 69.11/69.16 (~E(f2(a5,f2(a4,x4521)),x4521)), % 69.11/69.16 inference(scs_inference,[],[451,2])). % 69.11/69.16 cnf(453,plain, % 69.11/69.16 (~E(f2(f2(a4,f2(a5,a4)),a5),a5)), % 69.11/69.16 inference(scs_inference,[],[451,25,2,3])). % 69.11/69.16 cnf(457,plain, % 69.11/69.16 (~E(f2(a5,f2(f2(a4,a1),a4)),f2(a4,a4))), % 69.11/69.16 inference(scs_inference,[],[452,453,110,2,3])). % 69.11/69.16 cnf(462,plain, % 69.11/69.16 ($false), % 69.11/69.16 inference(scs_inference,[],[457,452,114,16,2,3]), % 69.11/69.16 ['proof']). % 69.11/69.16 % SZS output end Proof % 69.11/69.16 % Total time :68.500000s %------------------------------------------------------------------------------