%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL011-1 : TPTP v9.3.1. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n014.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:31 AM UTC 2026 % Result : Unsatisfiable 116.21s 116.39s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL011-1 : TPTP v9.3.1. Released v1.0.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.09/0.35 % Computer : n014.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Fri Sep 4 14:24:57 UTC 2026 % 0.09/0.36 % CPUTime : % 0.12/0.46 start to proof:theBenchmark % 116.21/116.38 %------------------------------------------- % 116.21/116.38 % File :CSE---1.7 % 116.21/116.38 % Problem :theBenchmark % 116.21/116.38 % Transform :cnf % 116.21/116.38 % Format :tptp:raw % 116.21/116.38 % Command :java -jar mcs_scs.jar %d %s % 116.21/116.38 % 116.21/116.38 % Result :Theorem 115.912294s % 116.21/116.38 % Output :CNFRefutation 115.912294s % 116.21/116.38 %------------------------------------------- % 116.21/116.38 %-------------------------------------------------------------------------- % 116.21/116.38 % File : LCL011-1 : TPTP v9.3.1. Released v1.0.0. % 116.21/116.38 % Domain : Logic Calculi (Equivalential) % 116.21/116.38 % Problem : YQF depends on YQJ % 116.21/116.38 % Version : [McC92] axioms. % 116.21/116.38 % English : Show that the single Lukasiewicz axiom YQF can be derived % 116.21/116.38 % from the single Lukasiewicz axiom YQJ. % 116.21/116.38 % 116.21/116.39 % Refs : [MW92] McCune & Wos (1992), Experiments in Automated Deductio % 116.21/116.39 % : [McC92] McCune (1992), Email to G. Sutcliffe % 116.21/116.39 % : [Wos95] Wos (1995), Searching for Circles of Pure Proofs % 116.21/116.39 % Source : [McC92] % 116.21/116.39 % Names : EC-74 [MW92] % 116.21/116.39 % 116.21/116.39 % Status : Unsatisfiable % 116.21/116.39 % Rating : 0.00 v6.1.0, 0.07 v6.0.0, 0.00 v5.4.0, 0.06 v5.3.0, 0.05 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.00 v2.2.1, 0.11 v2.1.0, 0.25 v2.0.0 % 116.21/116.39 % Syntax : Number of clauses : 3 ( 2 unt; 0 nHn; 2 RR) % 116.21/116.39 % Number of literals : 5 ( 0 equ; 3 neg) % 116.21/116.39 % Maximal clause size : 3 ( 1 avg) % 116.21/116.39 % Maximal term depth : 4 ( 2 avg) % 116.21/116.39 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty) % 116.21/116.39 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty) % 116.21/116.39 % Number of variables : 5 ( 0 sgn) % 116.21/116.39 % SPC : CNF_UNS_RFO_NEQ_HRN % 116.21/116.39 % 116.21/116.39 % Comments : % 116.21/116.39 %-------------------------------------------------------------------------- % 116.21/116.39 cnf(condensed_detachment,axiom, % 116.21/116.39 ( ~ is_a_theorem(equivalent(X,Y)) % 116.21/116.39 | ~ is_a_theorem(X) % 116.21/116.39 | is_a_theorem(Y) ) ). % 116.21/116.39 % 116.21/116.39 %----Axiom by Lukasiewicz % 116.21/116.39 cnf(yqj,axiom, % 116.21/116.39 is_a_theorem(equivalent(equivalent(X,Y),equivalent(equivalent(Z,X),equivalent(Y,Z)))) ). % 116.21/116.39 % 116.21/116.39 %----Axiom by Lukasiewicz % 116.21/116.39 cnf(prove_yqf,negated_conjecture, % 116.21/116.39 ~ is_a_theorem(equivalent(equivalent(a,b),equivalent(equivalent(a,c),equivalent(c,b)))) ). % 116.21/116.39 % 116.21/116.39 %-------------------------------------------------------------------------- % 116.21/116.39 %------------------------------------------- % 116.21/116.39 % Proof found % 116.21/116.39 % SZS status Theorem for theBenchmark % 116.21/116.39 % SZS output start Proof % 116.21/116.39 %ClaNum:3(EqnAxiom:0) % 116.21/116.39 %VarNum:10(SingletonVarNum:5) % 116.21/116.39 %MaxLitNum:3 % 116.21/116.39 %MaxfuncDepth:3 % 116.21/116.39 %SharedTerms:9 % 116.21/116.39 %goalClause: 2 % 116.21/116.39 %singleGoalClaCount:1 % 116.21/116.39 [2]~P1(f1(f1(a2,a3),f1(f1(a2,a4),f1(a4,a3)))) % 116.21/116.39 [1]P1(f1(f1(x11,x12),f1(f1(x13,x11),f1(x12,x13)))) % 116.21/116.39 [3]P1(x31)+~P1(x32)+~P1(f1(x32,x31)) % 116.21/116.39 %EqnAxiom % 116.21/116.39 % 116.21/116.39 %------------------------------------------- % 116.21/116.40 cnf(4,plain, % 116.21/116.40 (P1(f1(f1(x41,x42),f1(x43,x41)))+~P1(f1(x42,x43))), % 116.21/116.40 inference(scs_inference,[],[1,3])). % 116.21/116.40 cnf(6,plain, % 116.21/116.40 (P1(f1(f1(x61,f1(x62,x63)),f1(f1(f1(x64,x62),f1(x63,x64)),x61)))), % 116.21/116.40 inference(scs_inference,[],[1,4])). % 116.21/116.40 cnf(8,plain, % 116.21/116.40 (P1(f1(f1(f1(x81,x82),f1(x83,x81)),x84))+~P1(f1(x84,f1(x82,x83)))), % 116.21/116.40 inference(scs_inference,[],[1,4,3])). % 116.21/116.40 cnf(9,plain, % 116.21/116.40 (~P1(f1(x91,x92))+P1(x92)+~P1(x91)), % 116.21/116.40 inference(rename_variables,[],[3])). % 116.21/116.40 cnf(10,plain, % 116.21/116.40 (~P1(f1(x101,x101))+P1(f1(f1(f1(x101,x101),f1(x101,x101)),f1(x101,x101)))), % 116.21/116.40 inference(scs_inference,[],[1,4,3,9])). % 116.21/116.40 cnf(13,plain, % 116.21/116.40 (P1(f1(f1(f1(x131,f1(f1(x132,x133),f1(x134,x132))),f1(x135,x131)),f1(x135,f1(x133,x134))))), % 116.21/116.40 inference(scs_inference,[],[1,8,4])). % 116.21/116.40 cnf(14,plain, % 116.21/116.40 (P1(f1(f1(f1(x141,f1(x142,x143)),f1(f1(x144,x142),x141)),f1(x143,x144)))), % 116.21/116.40 inference(scs_inference,[],[1,8])). % 116.21/116.40 cnf(16,plain, % 116.21/116.40 (P1(f1(f1(x161,f1(f1(x162,f1(f1(x163,x164),f1(x165,x163))),f1(x166,x162))),f1(f1(x166,f1(x164,x165)),x161)))), % 116.21/116.40 inference(scs_inference,[],[1,13,8,4])). % 116.21/116.40 cnf(18,plain, % 116.21/116.40 (~P1(f1(f1(x181,f1(f1(x182,f1(a2,a4)),f1(f1(a4,a3),x182))),f1(f1(a2,a3),x181)))), % 116.21/116.40 inference(scs_inference,[],[1,2,13,8,4,3])). % 116.21/116.40 cnf(20,plain, % 116.21/116.40 (~P1(f1(x201,x202))+P1(x202)+~P1(x201)), % 116.21/116.40 inference(rename_variables,[],[3])). % 116.21/116.40 cnf(21,plain, % 116.21/116.40 (~P1(f1(f1(f1(x211,f1(a2,a4)),f1(f1(a4,a3),x211)),f1(a2,a3)))), % 116.21/116.40 inference(scs_inference,[],[1,2,13,8,4,3,20])). % 116.21/116.40 cnf(24,plain, % 116.21/116.40 (~P1(f1(x241,x241))+P1(f1(f1(x242,f1(f1(x241,x241),f1(x241,x241))),f1(f1(x241,x241),x242)))), % 116.21/116.40 inference(scs_inference,[],[10,4])). % 116.21/116.40 cnf(25,plain, % 116.21/116.40 (~P1(f1(f1(f1(a2,a3),f1(f1(f1(a4,a3),x251),x252)),f1(x252,f1(x251,f1(a2,a4)))))), % 116.21/116.40 inference(scs_inference,[],[18,8])). % 116.21/116.40 cnf(28,plain, % 116.21/116.40 (P1(f1(f1(x281,f1(f1(x282,f1(x283,x284)),f1(f1(x285,x283),x282))),f1(f1(x284,x285),x281)))), % 116.21/116.40 inference(scs_inference,[],[14,18,8,4])). % 116.21/116.40 cnf(34,plain, % 116.21/116.40 (P1(f1(f1(x341,f1(x342,f1(x343,x344))),f1(f1(f1(f1(x345,x343),f1(x344,x345)),x342),x341)))), % 116.21/116.40 inference(scs_inference,[],[6,25,8,4])). % 116.21/116.40 cnf(36,plain, % 116.21/116.40 (~P1(f1(f1(a2,a3),f1(f1(f1(a4,a3),f1(a4,x361)),f1(x361,a2))))), % 116.21/116.40 inference(scs_inference,[],[21,6,25,8,4,3])). % 116.21/116.40 cnf(40,plain, % 116.21/116.40 (P1(f1(f1(f1(x401,f1(x402,x403)),f1(x404,x401)),f1(x404,f1(f1(x405,f1(x406,x402)),f1(f1(x403,x406),x405)))))), % 116.21/116.40 inference(scs_inference,[],[28,8])). % 116.21/116.40 cnf(42,plain, % 116.21/116.40 (~P1(f1(f1(f1(f1(a4,a3),f1(a4,x421)),f1(x421,a2)),f1(f1(x422,f1(x423,a2)),f1(f1(a3,x423),x422))))), % 116.21/116.40 inference(scs_inference,[],[36,28,8,3])). % 116.21/116.40 cnf(45,plain, % 116.21/116.40 (~P1(f1(f1(f1(x451,f1(x452,a2)),f1(f1(a3,x452),x451)),f1(f1(a4,a2),f1(a3,a4))))), % 116.21/116.40 inference(scs_inference,[],[42,34,3])). % 0.38/116.40 cnf(49,plain, % 0.38/116.40 (P1(f1(f1(f1(x491,f1(x492,f1(x493,x494))),f1(x495,x491)),f1(x495,f1(f1(x496,f1(f1(x497,x493),f1(x494,x497))),f1(x492,x496)))))), % 0.38/116.40 inference(scs_inference,[],[42,16,34,3,8])). % 0.38/116.40 cnf(52,plain, % 0.38/116.40 (~P1(f1(f1(f1(a4,a2),f1(a3,a4)),f1(f1(x521,a2),f1(a3,x521))))), % 0.38/116.40 inference(scs_inference,[],[45,8])). % 0.38/116.40 cnf(54,plain, % 0.38/116.40 (~P1(f1(f1(x541,f1(a2,a3)),f1(f1(f1(f1(a4,a3),f1(a4,x542)),f1(x542,a2)),x541)))), % 0.38/116.40 inference(scs_inference,[],[45,40,42,8,3])). % 0.38/116.40 cnf(57,plain, % 0.38/116.40 (P1(f1(f1(f1(x571,x572),f1(x573,x571)),f1(f1(x574,f1(x575,x572)),f1(f1(x573,x575),x574))))), % 0.38/116.40 inference(scs_inference,[],[14,8])). % 0.38/116.40 cnf(59,plain, % 0.38/116.40 (~P1(f1(f1(f1(x591,a2),f1(a3,x591)),f1(a2,a3)))), % 0.38/116.40 inference(scs_inference,[],[52,14,6,8,3])). % 0.38/116.40 cnf(62,plain, % 0.38/116.40 (~P1(f1(x621,x621))+P1(f1(f1(f1(x622,x621),f1(x621,x622)),f1(f1(x621,x621),f1(x621,x621))))), % 0.38/116.40 inference(scs_inference,[],[8,10])). % 0.38/116.40 cnf(63,plain, % 0.38/116.40 (~P1(f1(f1(a2,a3),f1(a2,a3)))), % 0.38/116.40 inference(scs_inference,[],[59,8])). % 0.38/116.40 cnf(65,plain, % 0.38/116.40 (P1(f1(f1(x651,f1(x652,x653)),f1(f1(f1(x654,f1(x653,x654)),x652),x651)))), % 0.38/116.40 inference(scs_inference,[],[1,59,57,8,3])). % 0.38/116.40 cnf(69,plain, % 0.38/116.40 (~P1(f1(x691,x691))+P1(f1(f1(x692,f1(f1(x693,x691),f1(x691,x693))),f1(f1(f1(x691,x691),f1(x691,x691)),x692)))), % 0.38/116.40 inference(scs_inference,[],[62,4])). % 0.38/116.40 cnf(70,plain, % 0.38/116.40 (P1(f1(f1(f1(x701,f1(f1(x702,f1(x703,x702)),x704)),f1(x705,x701)),f1(x705,f1(x704,x703))))), % 0.38/116.40 inference(scs_inference,[],[65,8])). % 0.38/116.40 cnf(72,plain, % 0.38/116.40 (~P1(f1(f1(f1(f1(f1(a4,a3),f1(a4,x721)),f1(x721,a2)),f1(x722,f1(x723,x722))),f1(f1(a2,a3),x723)))), % 0.38/116.40 inference(scs_inference,[],[54,65,8,3])). % 0.38/116.40 cnf(76,plain, % 0.38/116.40 (~P1(f1(x761,x761))+P1(f1(f1(f1(x762,f1(f1(x761,x761),f1(x761,x761))),f1(x763,x762)),f1(x763,f1(f1(x764,x761),f1(x761,x764)))))), % 0.38/116.40 inference(scs_inference,[],[69,8])). % 0.38/116.40 cnf(77,plain, % 0.38/116.40 (~P1(f1(f1(f1(a2,a3),f1(a4,a3)),f1(f1(x771,a2),f1(a4,x771))))), % 0.38/116.40 inference(scs_inference,[],[72,8])). % 0.38/116.40 cnf(88,plain, % 0.38/116.40 (~P1(f1(f1(x881,f1(f1(x882,f1(a3,x882)),a2)),f1(f1(a2,a3),x881)))), % 0.38/116.40 inference(scs_inference,[],[63,70,54,8,3])). % 0.38/116.40 cnf(98,plain, % 0.38/116.40 (~P1(f1(f1(f1(a2,a3),f1(a2,x981)),f1(x981,f1(x982,f1(a3,x982)))))), % 0.38/116.40 inference(scs_inference,[],[88,8])). % 0.38/116.40 cnf(101,plain, % 0.38/116.40 (~P1(f1(f1(x1011,f1(f1(x1012,f1(f1(a4,x1013),x1012)),f1(x1013,a2))),f1(f1(f1(a2,a3),f1(a4,a3)),x1011)))), % 0.38/116.40 inference(scs_inference,[],[77,88,70,8,3])). % 0.38/116.40 cnf(104,plain, % 0.38/116.40 (P1(f1(f1(f1(x1041,f1(f1(f1(x1042,x1043),f1(x1044,x1042)),x1045)),f1(x1046,x1041)),f1(x1046,f1(x1045,f1(x1043,x1044)))))), % 0.38/116.40 inference(scs_inference,[],[34,8])). % 0.38/116.40 cnf(110,plain, % 0.38/116.40 (~P1(f1(f1(x1101,f1(a3,x1101)),a3))), % 0.38/116.40 inference(scs_inference,[],[98,8,4])). % 0.38/116.40 cnf(111,plain, % 0.38/116.40 (~P1(f1(a3,f1(f1(x1111,f1(f1(x1112,a3),f1(x1113,x1112))),f1(x1113,x1111))))), % 0.38/116.40 inference(scs_inference,[],[110,16,3])). % 0.38/116.40 cnf(114,plain, % 0.38/116.40 (P1(f1(f1(f1(x1141,x1142),f1(f1(x1143,x1144),x1141)),f1(f1(x1145,f1(f1(x1146,x1143),f1(x1144,x1146))),f1(x1142,x1145))))), % 0.38/116.40 inference(scs_inference,[],[110,16,13,3,8])). % 0.38/116.40 cnf(120,plain, % 0.38/116.40 (~P1(f1(f1(f1(f1(f1(a4,x1201),a2),x1201),f1(f1(a4,a3),x1202)),f1(x1202,f1(a2,a3))))), % 0.38/116.40 inference(scs_inference,[],[114,101,3,8])). % 0.38/116.40 cnf(123,plain, % 0.38/116.40 (P1(f1(f1(f1(x1231,x1232),f1(f1(x1233,x1234),x1231)),f1(f1(x1235,f1(f1(x1236,f1(x1234,x1236)),x1233)),f1(x1232,x1235))))), % 0.38/116.40 inference(scs_inference,[],[70,8])). % 0.38/116.40 cnf(125,plain, % 0.38/116.40 (~P1(f1(f1(f1(f1(a4,x1251),a2),f1(a2,a3)),f1(x1251,f1(a4,a3))))), % 0.38/116.40 inference(scs_inference,[],[6,120,70,8,3])). % 0.38/116.40 cnf(130,plain, % 0.38/116.40 (~P1(f1(f1(x1301,f1(f1(f1(x1302,a4),f1(a3,x1302)),x1303)),f1(f1(f1(f1(a4,x1303),a2),f1(a2,a3)),x1301)))), % 0.38/116.40 inference(scs_inference,[],[125,104,3])). % 0.38/116.40 cnf(137,plain, % 0.38/116.40 (~P1(f1(f1(x1371,f1(x1372,f1(a3,x1372))),f1(a3,x1371)))), % 0.38/116.40 inference(scs_inference,[],[111,49,130,8,3])). % 0.38/116.40 cnf(142,plain, % 0.38/116.40 (~P1(f1(f1(a3,f1(f1(a3,x1421),x1422)),f1(x1422,x1421)))), % 0.38/116.40 inference(scs_inference,[],[6,137,3])). % 0.38/116.40 cnf(150,plain, % 0.38/116.40 (~P1(f1(f1(x1501,f1(x1502,a3)),f1(f1(a3,x1502),x1501)))), % 0.38/116.40 inference(scs_inference,[],[142,14,24,3])). % 0.38/116.40 cnf(154,plain, % 0.38/116.40 (P1(f1(f1(f1(x1541,x1542),f1(f1(x1543,f1(x1544,x1543)),x1542)),f1(x1544,x1541)))), % 0.38/116.40 inference(scs_inference,[],[13,150,123,8,3])). % 0.38/116.40 cnf(158,plain, % 0.38/116.40 (~P1(f1(x1581,x1581))), % 0.38/116.40 inference(scs_inference,[],[13,150,123,8,3,76])). % 0.38/116.40 cnf(164,plain, % 0.38/116.40 (P1(f1(f1(f1(x1641,x1642),f1(f1(x1643,x1642),f1(x1644,x1643))),f1(x1644,x1641)))), % 0.38/116.40 inference(scs_inference,[],[13,154,114,4,8,3])). % 0.38/116.40 cnf(170,plain, % 0.38/116.40 ($false), % 0.38/116.40 inference(scs_inference,[],[158,164,4,8]), % 0.38/116.40 ['proof']). % 0.38/116.40 % SZS output end Proof % 0.38/116.40 % Total time :115.912294s %------------------------------------------------------------------------------