%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL257-1 : TPTP v9.3.1. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:18:54 AM UTC 2026 % Result : Unsatisfiable 11.36s 11.58s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL257-1 : TPTP v9.3.1. Released v2.0.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.08/0.34 % Computer : n016.cluster.edu % 0.08/0.34 % Model : x86_64 x86_64 % 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.34 % Memory : 8046.5625MB % 0.08/0.34 % OS : Linux 6.8.0-71-generic % 0.08/0.34 % CPULimit : 300 % 0.08/0.34 % WCLimit : 300 % 0.08/0.34 % DateTime : Sat Sep 5 21:53:30 UTC 2026 % 0.08/0.34 % CPUTime : % 0.24/0.51 start to proof:theBenchmark % 11.36/11.57 %------------------------------------------- % 11.36/11.57 % File :CSE---1.7 % 11.36/11.57 % Problem :theBenchmark % 11.36/11.57 % Transform :cnf % 11.36/11.57 % Format :tptp:raw % 11.36/11.57 % Command :java -jar mcs_scs.jar %d %s % 11.36/11.57 % 11.36/11.57 % Result :Theorem 11.079452s % 11.36/11.57 % Output :CNFRefutation 11.079452s % 11.36/11.57 %------------------------------------------- % 11.36/11.57 %-------------------------------------------------------------------------- % 11.36/11.57 % File : LCL257-1 : TPTP v9.3.1. Released v2.0.0. % 11.36/11.57 % Domain : Logic Calculi (Equivalential) % 11.36/11.57 % Problem : XHN depends on YQL % 11.36/11.57 % Version : [TPTP] axioms. % 11.36/11.57 % English : Show that XHN can be derived from the single Lukasiewicz % 11.36/11.57 % axiom YQL. % 11.36/11.57 % 11.36/11.57 % Refs : [MW92] McCune & Wos (1992), Experiments in Automated Deductio % 11.36/11.57 % : [McC92] McCune (1992), Email to G. Sutcliffe % 11.36/11.57 % : [Wos95] Wos (1995), Searching for Circles of Pure Proofs % 11.36/11.57 % Source : [TPTP] % 11.36/11.57 % Names : % 11.36/11.57 % 11.36/11.57 % Status : Unsatisfiable % 11.36/11.57 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.10 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.00 v2.1.0 % 11.36/11.57 % Syntax : Number of clauses : 3 ( 2 unt; 0 nHn; 2 RR) % 11.36/11.57 % Number of literals : 5 ( 0 equ; 3 neg) % 11.36/11.57 % Maximal clause size : 3 ( 1 avg) % 11.36/11.57 % Maximal term depth : 5 ( 2 avg) % 11.36/11.57 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty) % 11.36/11.57 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty) % 11.36/11.57 % Number of variables : 5 ( 0 sgn) % 11.36/11.57 % SPC : CNF_UNS_RFO_NEQ_HRN % 11.36/11.57 % 11.36/11.57 % Comments : This completes the loop of single axioms' dependence in % 11.36/11.57 % problems LCL010 to LCL021. % 11.36/11.57 % : Thought to be LCLunsatisfiable. % 11.36/11.57 %-------------------------------------------------------------------------- % 11.36/11.57 cnf(condensed_detachment,axiom, % 11.36/11.57 ( ~ is_a_theorem(equivalent(X,Y)) % 11.36/11.57 | ~ is_a_theorem(X) % 11.36/11.57 | is_a_theorem(Y) ) ). % 11.36/11.57 % 11.36/11.57 %----Axiom by Lukasiewicz % 11.36/11.57 cnf(yql,axiom, % 11.36/11.57 is_a_theorem(equivalent(equivalent(X,Y),equivalent(equivalent(Z,Y),equivalent(X,Z)))) ). % 11.36/11.57 % 11.36/11.57 %----Axiom of symmetry % 11.36/11.58 cnf(prove_xhn,negated_conjecture, % 11.36/11.58 ~ is_a_theorem(equivalent(x,equivalent(equivalent(y,z),equivalent(equivalent(z,x),y)))) ). % 11.36/11.58 % 11.36/11.58 %-------------------------------------------------------------------------- % 11.36/11.58 %------------------------------------------- % 11.36/11.58 % Proof found % 11.36/11.58 % SZS status Theorem for theBenchmark % 11.36/11.58 % SZS output start Proof % 11.36/11.58 %ClaNum:3(EqnAxiom:0) % 11.36/11.58 %VarNum:10(SingletonVarNum:5) % 11.36/11.58 %MaxLitNum:3 % 11.36/11.58 %MaxfuncDepth:4 % 11.36/11.58 %SharedTerms:9 % 11.36/11.58 %goalClause: 2 % 11.36/11.58 %singleGoalClaCount:1 % 11.36/11.58 [2]~P1(f1(a2,f1(f1(a3,a4),f1(f1(a4,a2),a3)))) % 11.36/11.58 [1]P1(f1(f1(x11,x12),f1(f1(x13,x12),f1(x11,x13)))) % 11.36/11.58 [3]P1(x31)+~P1(x32)+~P1(f1(x32,x31)) % 11.36/11.58 %EqnAxiom % 11.36/11.58 % 11.36/11.58 %------------------------------------------- % 11.36/11.58 cnf(4,plain, % 11.36/11.58 (P1(f1(f1(x41,x42),f1(x43,x41)))+~P1(f1(x43,x42))), % 11.36/11.58 inference(scs_inference,[],[1,3])). % 11.36/11.58 cnf(6,plain, % 11.36/11.58 (P1(f1(f1(x61,f1(f1(x62,x63),f1(x64,x62))),f1(f1(x64,x63),x61)))), % 11.36/11.58 inference(scs_inference,[],[1,4])). % 11.36/11.58 cnf(8,plain, % 11.36/11.58 (P1(f1(f1(x81,x82),f1(x81,x82)))), % 11.36/11.58 inference(scs_inference,[],[1,4,3])). % 11.36/11.58 cnf(10,plain, % 11.36/11.58 (P1(f1(f1(x101,f1(x102,x103)),f1(f1(x102,x103),x101)))), % 11.36/11.58 inference(scs_inference,[],[8,4])). % 11.36/11.58 cnf(12,plain, % 11.36/11.58 (P1(f1(f1(x121,x122),f1(f1(x121,x123),f1(x123,x122))))), % 11.36/11.58 inference(scs_inference,[],[6,10,3])). % 11.36/11.58 cnf(16,plain, % 11.36/11.58 (P1(f1(f1(x161,f1(f1(x162,x163),f1(x163,x164))),f1(f1(x162,x164),x161)))), % 11.36/11.58 inference(scs_inference,[],[6,10,3,4])). % 11.36/11.58 cnf(18,plain, % 11.36/11.58 (P1(f1(f1(x181,x181),f1(x182,x182)))), % 11.36/11.58 inference(scs_inference,[],[12,6,3])). % 11.36/11.58 cnf(22,plain, % 11.36/11.58 (P1(f1(f1(x221,f1(x222,x222)),f1(f1(x223,x223),x221)))), % 11.36/11.58 inference(scs_inference,[],[12,6,3,4])). % 11.36/11.58 cnf(24,plain, % 11.36/11.58 (P1(f1(x241,x241))), % 11.36/11.58 inference(scs_inference,[],[18,22,3])). % 11.36/11.58 cnf(28,plain, % 11.36/11.58 (P1(f1(f1(x281,x282),f1(x282,x281)))), % 11.36/11.58 inference(scs_inference,[],[18,22,3,4])). % 11.36/11.58 cnf(30,plain, % 11.36/11.58 (P1(f1(f1(x301,f1(x302,x303)),f1(f1(x303,x302),x301)))), % 11.36/11.58 inference(scs_inference,[],[28,4])). % 11.36/11.58 cnf(38,plain, % 11.36/11.58 (P1(f1(f1(f1(x381,x382),x383),f1(x383,f1(f1(x384,x382),f1(x381,x384)))))), % 11.36/11.58 inference(scs_inference,[],[1,12,3])). % 11.36/11.58 cnf(41,plain, % 11.36/11.58 (~P1(f1(f1(f1(a4,a2),a4),a2))), % 11.36/11.58 inference(scs_inference,[],[38,2,3])). % 11.36/11.58 cnf(55,plain, % 11.36/11.58 (P1(f1(f1(f1(x551,x551),x552),f1(x552,f1(x553,x553))))), % 11.36/11.58 inference(scs_inference,[],[18,12,3])). % 11.36/11.58 cnf(68,plain, % 11.36/11.58 (P1(f1(f1(f1(x681,x682),x683),f1(x683,f1(x682,x681))))), % 11.36/11.58 inference(scs_inference,[],[28,12,3])). % 11.36/11.58 cnf(74,plain, % 11.36/11.58 (P1(f1(f1(f1(x741,x742),f1(x742,x741)),f1(x743,x743)))), % 11.36/11.58 inference(scs_inference,[],[30,55,3])). % 11.36/11.58 cnf(92,plain, % 11.36/11.58 (P1(f1(f1(x921,f1(f1(x922,x923),f1(x923,x922))),f1(f1(x924,x924),x921)))), % 11.36/11.58 inference(scs_inference,[],[30,22,3,4])). % 11.36/11.58 cnf(106,plain, % 11.36/11.58 (~P1(f1(a2,f1(f1(a4,a2),a4)))), % 11.36/11.58 inference(scs_inference,[],[41,28,3])). % 11.36/11.58 cnf(115,plain, % 11.36/11.58 (~P1(f1(f1(a4,f1(a4,a2)),a2))), % 11.36/11.58 inference(scs_inference,[],[68,106,3])). % 11.36/11.58 cnf(128,plain, % 11.36/11.58 (P1(f1(f1(x1281,f1(f1(x1282,x1282),f1(x1283,x1283))),f1(f1(x1284,x1284),x1281)))), % 11.36/11.58 inference(scs_inference,[],[55,92,3,4])). % 11.36/11.58 cnf(155,plain, % 11.36/11.58 (P1(f1(f1(f1(f1(x1551,x1552),f1(x1552,x1551)),x1553),f1(x1553,f1(x1554,x1554))))), % 11.36/11.58 inference(scs_inference,[],[74,12,3])). % 11.36/11.58 cnf(183,plain, % 11.36/11.58 (P1(f1(f1(f1(x1831,x1831),f1(f1(x1832,x1833),f1(x1833,x1832))),f1(x1834,x1834)))), % 11.36/11.58 inference(scs_inference,[],[92,155,3])). % 11.36/11.58 cnf(202,plain, % 11.36/11.58 (~P1(f1(a2,f1(a4,f1(a4,a2))))), % 11.36/11.58 inference(scs_inference,[],[115,28,3])). % 11.36/11.58 cnf(221,plain, % 11.36/11.58 (P1(f1(f1(f1(x2211,x2211),f1(f1(x2212,x2212),f1(x2213,x2213))),f1(x2214,x2214)))), % 11.36/11.58 inference(scs_inference,[],[128,155,3])). % 11.36/11.58 cnf(476,plain, % 11.36/11.58 (P1(f1(f1(x4761,x4761),f1(f1(x4762,x4763),f1(f1(x4764,x4762),f1(x4763,x4764)))))), % 11.36/11.58 inference(scs_inference,[],[6,92,3])). % 11.36/11.58 cnf(480,plain, % 11.36/11.58 (P1(f1(f1(x4801,x4802),f1(f1(x4803,x4801),f1(x4802,x4803))))), % 11.36/11.58 inference(scs_inference,[],[24,476,3])). % 11.36/11.58 cnf(489,plain, % 11.36/11.58 (P1(f1(f1(x4891,f1(x4892,x4893)),f1(f1(f1(x4892,x4894),f1(x4894,x4893)),x4891)))), % 11.36/11.58 inference(scs_inference,[],[12,480,3])). % 11.36/11.58 cnf(508,plain, % 11.36/11.58 (P1(f1(f1(x5081,x5081),f1(f1(x5082,x5083),f1(f1(x5083,x5084),f1(x5084,x5082)))))), % 11.36/11.58 inference(scs_inference,[],[16,92,3])). % 11.36/11.58 cnf(512,plain, % 11.36/11.58 (P1(f1(f1(x5121,x5122),f1(f1(x5122,x5123),f1(x5123,x5121))))), % 11.36/11.58 inference(scs_inference,[],[183,508,3])). % 11.36/11.58 cnf(516,plain, % 11.36/11.58 (P1(f1(f1(x5161,f1(f1(x5162,x5163),f1(x5163,x5164))),f1(f1(x5164,x5162),x5161)))), % 11.36/11.58 inference(scs_inference,[],[512,4])). % 11.36/11.58 cnf(562,plain, % 11.36/11.58 (P1(f1(f1(x5621,x5621),f1(f1(f1(x5622,x5623),f1(x5623,x5624)),f1(x5622,x5624))))), % 11.36/11.58 inference(scs_inference,[],[489,22,3])). % 11.36/11.58 cnf(568,plain, % 11.36/11.58 (P1(f1(f1(f1(x5681,x5682),f1(x5682,x5683)),f1(x5681,x5683)))), % 11.36/11.58 inference(scs_inference,[],[221,562,4,3])). % 11.36/11.58 cnf(572,plain, % 11.36/11.59 (~P1(f1(f1(a2,x5721),f1(x5721,f1(a4,f1(a4,a2)))))), % 11.36/11.59 inference(scs_inference,[],[568,202,3])). % 11.36/11.59 cnf(575,plain, % 11.36/11.59 ($false), % 11.36/11.59 inference(scs_inference,[],[516,30,572,3]), % 11.36/11.59 ['proof']). % 11.36/11.59 % SZS output end Proof % 11.36/11.59 % Total time :11.079452s %------------------------------------------------------------------------------