%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL268-3 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n013.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:55 AM UTC 2026
% Result : Unsatisfiable 66.39s 66.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL268-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.06/0.34 % Computer : n013.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Sat Sep 5 00:20:35 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.30/0.49 start to proof:theBenchmark
% 66.39/66.61 %-------------------------------------------
% 66.39/66.61 % File :CSE---1.7
% 66.39/66.61 % Problem :theBenchmark
% 66.39/66.61 % Transform :cnf
% 66.39/66.61 % Format :tptp:raw
% 66.39/66.61 % Command :java -jar mcs_scs.jar %d %s
% 66.39/66.61
% 66.39/66.61 % Result :Theorem 66.043236s
% 66.39/66.61 % Output :CNFRefutation 66.043236s
% 66.39/66.61 %-------------------------------------------
% 66.39/66.61 %--------------------------------------------------------------------------
% 66.39/66.61 % File : LCL268-3 : TPTP v9.3.1. Released v2.3.0.
% 66.39/66.61 % Domain : Logic Calculi (Propositional)
% 66.39/66.61 % Problem : Principia Mathematica 4.2
% 66.39/66.61 % Version : [WR27] axioms.
% 66.39/66.61 % English :
% 66.39/66.61
% 66.39/66.61 % Refs : [WR27] Whitehead & Russell (1927), Principia Mathematica
% 66.39/66.61 % Source : [WR27]
% 66.39/66.61 % Names : Problem 4.2 [WR27]
% 66.39/66.61
% 66.39/66.61 % Status : Unsatisfiable
% 66.39/66.61 % Rating : 0.00 v9.3.0, 0.17 v9.1.0, 0.00 v7.0.0, 0.14 v6.3.0, 0.17 v6.2.0, 0.00 v6.0.0, 0.22 v5.5.0, 0.31 v5.4.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.14 v5.0.0, 0.29 v4.1.0, 0.22 v4.0.1, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.3.0
% 66.39/66.61 % Syntax : Number of clauses : 11 ( 9 unt; 0 nHn; 3 RR)
% 66.39/66.61 % Number of literals : 14 ( 3 equ; 4 neg)
% 66.39/66.61 % Maximal clause size : 3 ( 1 avg)
% 66.39/66.61 % Maximal term depth : 4 ( 2 avg)
% 66.39/66.61 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 66.39/66.61 % Number of functors : 6 ( 6 usr; 1 con; 0-2 aty)
% 66.39/66.61 % Number of variables : 20 ( 1 sgn)
% 66.39/66.61 % SPC : CNF_UNS_RFO_SEQ_HRN
% 66.39/66.61
% 66.39/66.61 % Comments :
% 66.39/66.61 %--------------------------------------------------------------------------
% 66.39/66.61 %----Include axioms of propositional logic
% 66.39/66.61 include('Axioms/LCL004-0.ax').
% 66.39/66.61 include('Axioms/LCL004-1.ax').
% 66.39/66.61 include('Axioms/LCL004-2.ax').
% 66.39/66.61 %--------------------------------------------------------------------------
% 66.39/66.61 cnf(prove_this,negated_conjecture,
% 66.39/66.61 ~ theorem(equivalent(p,p)) ).
% 66.39/66.61
% 66.39/66.61 %--------------------------------------------------------------------------
% 66.39/66.61 %-------------------------------------------
% 66.39/66.61 % Proof found
% 66.39/66.61 % SZS status Theorem for theBenchmark
% 66.39/66.61 % SZS output start Proof
% 66.39/66.61 %ClaNum:8(EqnAxiom:0)
% 66.39/66.61 %VarNum:28(SingletonVarNum:14)
% 66.39/66.61 %MaxLitNum:3
% 66.39/66.61 %MaxfuncDepth:5
% 66.39/66.61 %SharedTerms:7
% 66.39/66.61 %goalClause: 6
% 66.39/66.61 %singleGoalClaCount:1
% 66.39/66.61 [6]~P2(f1(f2(f1(f2(f1(a3),a3)),f1(f2(f1(a3),a3)))))
% 66.39/66.61 [2]P1(f2(f1(f2(x21,x21)),x21))
% 66.39/66.61 [1]P1(f2(f1(x11),f2(x12,x11)))
% 66.39/66.61 [3]P1(f2(f1(f2(x31,x32)),f2(x32,x31)))
% 66.39/66.61 [4]P1(f2(f1(f2(x41,f2(x42,x43))),f2(x42,f2(x41,x43))))
% 66.39/66.61 [5]P1(f2(f1(f2(f1(x51),x52)),f2(f1(f2(x53,x51)),f2(x53,x52))))
% 66.39/66.61 [7]~P1(x71)+P2(x71)
% 66.39/66.61 [8]P2(x81)+~P2(x82)+~P2(f2(f1(x82),x81))
% 66.39/66.61 %EqnAxiom
% 66.39/66.61
% 66.39/66.61 %-------------------------------------------
% 66.84/67.08 cnf(457543,plain,
% 66.84/67.08 (P2(f2(f1(x4575431),f2(x4575432,x4575431)))),
% 66.84/67.08 inference(scs_inference,[],[1,7])).
% 66.84/67.08 cnf(457547,plain,
% 66.84/67.08 (P2(f2(f1(f2(x4575471,x4575472)),f2(x4575472,x4575471)))),
% 66.84/67.08 inference(scs_inference,[],[3,7])).
% 66.84/67.08 cnf(457549,plain,
% 66.84/67.08 (P2(f2(f1(f2(x4575491,x4575491)),x4575491))),
% 66.84/67.08 inference(scs_inference,[],[2,7])).
% 66.84/67.08 cnf(457551,plain,
% 66.84/67.08 (P2(f2(f1(f2(x4575511,f2(x4575512,x4575513))),f2(x4575512,f2(x4575511,x4575513))))),
% 66.84/67.08 inference(scs_inference,[],[4,7])).
% 66.84/67.08 cnf(457553,plain,
% 66.84/67.08 (P2(f2(f1(f2(f1(x4575531),x4575532)),f2(f1(f2(x4575533,x4575531)),f2(x4575533,x4575532))))),
% 66.84/67.08 inference(scs_inference,[],[5,7])).
% 66.84/67.08 cnf(457555,plain,
% 66.84/67.08 (P2(f2(x4575551,f2(f1(x4575552),f2(x4575553,x4575552))))),
% 66.84/67.08 inference(scs_inference,[],[1,457543,7,8])).
% 66.84/67.08 cnf(461745,plain,
% 66.84/67.08 (P2(f2(f1(x4617451),f2(x4617452,f2(x4617453,x4617451))))),
% 66.84/67.08 inference(scs_inference,[],[457555,457551,8])).
% 66.84/67.08 cnf(461750,plain,
% 66.84/67.08 (P2(f2(x4617501,f2(x4617502,f2(f1(x4617503),f2(x4617504,x4617503)))))),
% 66.84/67.08 inference(scs_inference,[],[461745,457543,8])).
% 66.84/67.08 cnf(461757,plain,
% 66.84/67.08 (P2(f2(x4617571,f2(x4617572,f2(x4617573,f2(f1(x4617574),f2(x4617575,x4617574))))))),
% 66.84/67.08 inference(scs_inference,[],[457543,461750,8])).
% 66.84/67.08 cnf(461761,plain,
% 66.84/67.08 (P2(f2(x4617611,f2(x4617612,f2(x4617613,f2(x4617614,f2(f1(x4617615),f2(x4617616,x4617615)))))))),
% 66.84/67.08 inference(scs_inference,[],[457543,461757,8])).
% 66.84/67.08 cnf(461768,plain,
% 66.84/67.08 (P2(f2(x4617681,f2(f1(f2(x4617682,x4617681)),x4617682)))),
% 66.84/67.08 inference(scs_inference,[],[457551,457547,8])).
% 66.84/67.08 cnf(461780,plain,
% 66.84/67.08 (P2(f2(x4617801,f2(x4617802,f2(x4617803,f2(f1(f2(x4617804,x4617803)),x4617804)))))),
% 66.84/67.08 inference(scs_inference,[],[461745,461768,8])).
% 66.84/67.08 cnf(461791,plain,
% 66.84/67.08 (P2(f2(x4617911,f2(x4617912,f2(f1(f2(x4617913,x4617912)),x4617913))))),
% 66.84/67.08 inference(scs_inference,[],[461761,461780,8])).
% 66.84/67.08 cnf(461811,plain,
% 66.84/67.08 (P2(f2(x4618111,f2(f1(x4618112),f2(x4618113,f2(x4618114,x4618112)))))),
% 66.84/67.08 inference(scs_inference,[],[457543,461745,8])).
% 66.84/67.08 cnf(461815,plain,
% 66.84/67.08 (P2(f2(x4618151,f2(x4618152,f2(f1(x4618153),f2(x4618154,f2(x4618155,x4618153))))))),
% 66.84/67.08 inference(scs_inference,[],[457543,461811,8])).
% 66.84/67.08 cnf(461822,plain,
% 66.84/67.08 (P2(f2(x4618221,f2(x4618222,f2(f1(f2(x4618223,x4618221)),x4618223))))),
% 66.84/67.08 inference(scs_inference,[],[457551,461791,8])).
% 66.84/67.08 cnf(461827,plain,
% 66.84/67.08 (P2(f2(f1(f2(x4618271,f2(x4618272,f2(x4618273,x4618274)))),f2(x4618271,f2(x4618273,f2(x4618272,x4618274)))))),
% 66.84/67.08 inference(scs_inference,[],[457551,457553,8])).
% 66.84/67.08 cnf(461838,plain,
% 66.84/67.08 (P2(f2(f2(x4618381,f2(x4618382,x4618383)),f1(x4618383)))),
% 66.84/67.08 inference(scs_inference,[],[461745,457547,8])).
% 66.84/67.08 cnf(461865,plain,
% 66.84/67.08 (P2(f2(x4618651,f2(f1(f2(x4618652,x4618651)),f2(x4618653,x4618652))))),
% 66.84/67.08 inference(scs_inference,[],[461822,461827,8])).
% 66.84/67.08 cnf(461875,plain,
% 66.84/67.08 (P2(f2(f1(f2(x4618751,f1(f2(f2(x4618752,f2(x4618753,x4618754)),f1(x4618754))))),f2(x4618755,x4618751)))),
% 66.84/67.08 inference(scs_inference,[],[461838,461865,8])).
% 66.84/67.08 cnf(461879,plain,
% 66.84/67.08 (P2(f2(x4618791,f2(f1(x4618792),f2(x4618793,f2(x4618794,f2(x4618795,x4618792))))))),
% 66.84/67.08 inference(scs_inference,[],[461815,461827,8])).
% 66.84/67.08 cnf(461886,plain,
% 66.84/67.08 (P2(f2(f1(x4618861),f2(x4618862,f2(x4618863,f2(x4618864,x4618861)))))),
% 66.84/67.08 inference(scs_inference,[],[461879,461875,8])).
% 66.84/67.08 cnf(461890,plain,
% 66.84/67.08 (P2(f2(x4618901,f2(x4618902,f2(f1(x4618903),f2(x4618904,f2(x4618905,f2(x4618906,x4618903)))))))),
% 66.84/67.08 inference(scs_inference,[],[461886,461745,8])).
% 66.84/67.08 cnf(461897,plain,
% 66.84/67.08 (P2(f2(f1(f2(x4618971,f1(f2(f1(f2(x4618972,x4618972)),x4618972)))),f2(x4618973,x4618971)))),
% 66.84/67.08 inference(scs_inference,[],[457549,461865,8])).
% 66.84/67.08 cnf(461917,plain,
% 66.84/67.08 (P2(f2(x4619171,f2(f1(f2(x4619172,x4619173)),f2(x4619173,x4619172))))),
% 66.84/67.09 inference(scs_inference,[],[461791,461827,8])).
% 66.84/67.09 cnf(461937,plain,
% 66.84/67.09 (P2(f2(f1(x4619371),f2(x4619372,f2(x4619373,f2(x4619374,f2(x4619375,x4619371))))))),
% 66.84/67.09 inference(scs_inference,[],[461879,457551,8])).
% 66.84/67.09 cnf(461947,plain,
% 66.84/67.09 (P2(f2(f1(f2(x4619471,x4619472)),f2(x4619471,f2(f1(f2(x4619473,x4619474)),f2(x4619474,x4619473)))))),
% 66.84/67.09 inference(scs_inference,[],[461917,457553,8])).
% 66.84/67.09 cnf(461958,plain,
% 66.84/67.09 (P2(f2(f1(f2(x4619581,x4619582)),f2(f1(f2(x4619583,x4619584)),f2(x4619581,f2(x4619584,x4619583)))))),
% 66.84/67.09 inference(scs_inference,[],[461947,461827,8])).
% 66.84/67.09 cnf(461968,plain,
% 66.84/67.09 (P2(f2(f1(f2(x4619681,x4619682)),f2(f1(f2(x4619683,f2(x4619684,x4619685))),f2(x4619682,x4619681))))),
% 66.84/67.09 inference(scs_inference,[],[457551,461958,8])).
% 66.84/67.09 cnf(461972,plain,
% 66.84/67.09 (P2(f2(f1(f2(x4619721,f2(x4619722,x4619723))),f2(f2(x4619724,f2(x4619725,x4619726)),f1(f2(x4619725,f2(x4619724,x4619726))))))),
% 66.84/67.09 inference(scs_inference,[],[457551,461968,8])).
% 66.84/67.09 cnf(461990,plain,
% 66.84/67.09 (P2(f2(f2(x4619901,f2(x4619902,x4619903)),f1(f2(x4619902,f2(x4619901,x4619903)))))),
% 66.84/67.09 inference(scs_inference,[],[461761,461972,8])).
% 66.84/67.09 cnf(462000,plain,
% 66.84/67.09 (P2(f2(x4620001,f2(x4620002,f2(f1(f2(f2(x4620002,x4620003),f2(x4620002,x4620003))),x4620003))))),
% 66.84/67.09 inference(scs_inference,[],[461990,461897,8])).
% 66.84/67.09 cnf(462011,plain,
% 66.84/67.09 (P2(f2(x4620111,f2(f1(f2(f2(x4620111,x4620112),f2(x4620111,x4620112))),x4620112)))),
% 66.84/67.09 inference(scs_inference,[],[461937,462000,8])).
% 66.84/67.09 cnf(462022,plain,
% 66.84/67.09 (P2(f2(f1(f2(x4620221,f1(f2(x4620222,f2(f1(f2(x4620223,x4620224)),f2(x4620224,x4620223)))))),f2(x4620225,x4620221)))),
% 66.84/67.09 inference(scs_inference,[],[461865,461917,8])).
% 66.84/67.09 cnf(462026,plain,
% 66.84/67.09 (P2(f2(x4620261,f2(x4620262,f2(x4620263,f2(x4620264,f2(f1(f2(x4620265,x4620264)),f2(x4620266,x4620265)))))))),
% 66.84/67.09 inference(scs_inference,[],[461865,461886,8])).
% 66.84/67.09 cnf(462037,plain,
% 66.84/67.09 (P2(f2(x4620371,f2(x4620372,f2(x4620373,f2(f1(f2(x4620374,x4620373)),f2(x4620375,x4620374))))))),
% 66.84/67.09 inference(scs_inference,[],[461886,462026,8])).
% 66.84/67.09 cnf(462044,plain,
% 66.84/67.09 (P2(f2(x4620441,f2(x4620442,f2(f1(f2(x4620443,x4620442)),f2(x4620444,x4620443)))))),
% 66.84/67.09 inference(scs_inference,[],[462011,462037,8])).
% 66.84/67.09 cnf(462065,plain,
% 66.84/67.09 (P2(f2(x4620651,f2(f1(f2(x4620652,x4620653)),f2(x4620654,f2(x4620653,x4620652)))))),
% 66.84/67.09 inference(scs_inference,[],[461990,462022,8])).
% 66.84/67.09 cnf(462076,plain,
% 66.84/67.09 (P2(f2(f1(f2(x4620761,x4620762)),f2(x4620763,f2(x4620762,x4620761))))),
% 66.84/67.09 inference(scs_inference,[],[462037,462065,8])).
% 66.84/67.09 cnf(462108,plain,
% 66.84/67.09 (P2(f2(f1(f2(x4621081,f2(x4621082,x4621083))),f2(x4621081,f2(x4621084,f2(x4621083,x4621082)))))),
% 66.84/67.09 inference(scs_inference,[],[457553,462076,8])).
% 66.84/67.09 cnf(462140,plain,
% 66.84/67.09 (P2(f2(x4621401,f2(f1(x4621402),f2(x4621403,f2(x4621404,f2(x4621405,f2(x4621406,x4621402)))))))),
% 66.84/67.09 inference(scs_inference,[],[461827,461890,8])).
% 66.84/67.09 cnf(462174,plain,
% 66.84/67.09 (P2(f2(x4621741,f2(f2(f1(f2(x4621742,x4621743)),f2(x4621743,x4621742)),x4621744)))),
% 66.84/67.09 inference(scs_inference,[],[461917,462076,8])).
% 66.84/67.09 cnf(462188,plain,
% 66.84/67.09 (P2(f2(x4621881,f2(f1(f2(f2(x4621882,x4621883),f2(x4621882,x4621883))),f2(x4621882,x4621883))))),
% 66.84/67.09 inference(scs_inference,[],[462000,461827,8])).
% 66.84/67.09 cnf(462294,plain,
% 66.84/67.09 (P2(f2(f1(f2(x4622941,x4622942)),f2(x4622941,f2(f1(f2(f2(x4622943,x4622944),f2(x4622943,x4622944))),f2(x4622943,x4622944)))))),
% 66.84/67.09 inference(scs_inference,[],[457553,462188,8])).
% 66.84/67.09 cnf(462299,plain,
% 66.84/67.09 (P2(f2(f1(f2(x4622991,f2(x4622992,x4622993))),f2(x4622991,f2(x4622992,f2(f1(f2(f2(x4622994,x4622995),f2(x4622994,x4622995))),f2(x4622994,x4622995))))))),
% 66.84/67.09 inference(scs_inference,[],[457553,462294,8])).
% 66.84/67.09 cnf(462306,plain,
% 66.84/67.09 (P2(f2(x4623061,f2(x4623062,f2(f1(f2(f2(x4623063,x4623064),f2(x4623063,x4623064))),f2(x4623063,x4623064)))))),
% 66.84/67.09 inference(scs_inference,[],[461750,462299,8])).
% 66.84/67.09 cnf(462326,plain,
% 66.84/67.09 (P2(f2(x4623261,f2(f1(f2(f2(x4623262,x4623263),f2(x4623262,x4623263))),f2(x4623264,f2(x4623262,x4623263)))))),
% 66.84/67.09 inference(scs_inference,[],[461827,462306,8])).
% 66.84/67.09 cnf(462331,plain,
% 66.84/67.09 (P2(f2(f1(f2(f2(x4623311,x4623312),f2(x4623311,x4623312))),f2(x4623313,f2(x4623311,x4623312))))),
% 66.84/67.09 inference(scs_inference,[],[461827,462326,8])).
% 66.84/67.09 cnf(462349,plain,
% 66.84/67.09 (P2(f2(x4623491,f2(x4623492,f2(x4623493,f2(f1(f2(x4623494,x4623494)),x4623494)))))),
% 66.84/67.09 inference(scs_inference,[],[461897,461838,8])).
% 66.84/67.09 cnf(462354,plain,
% 66.84/67.09 (P2(f2(x4623541,f2(x4623542,f2(f1(f2(x4623543,x4623543)),x4623543))))),
% 66.84/67.09 inference(scs_inference,[],[461897,462349,8])).
% 66.84/67.09 cnf(462361,plain,
% 66.84/67.09 (P2(f2(x4623611,f2(f1(f2(x4623612,x4623612)),x4623612)))),
% 66.84/67.09 inference(scs_inference,[],[462331,462354,8])).
% 66.84/67.09 cnf(462384,plain,
% 66.84/67.09 (P2(f2(x4623841,f2(f2(f1(f2(f2(x4623842,x4623843),f2(x4623842,x4623843))),x4623843),x4623842)))),
% 66.84/67.09 inference(scs_inference,[],[462011,462076,8])).
% 66.84/67.09 cnf(462394,plain,
% 66.84/67.09 (P2(f2(f2(f1(f2(f2(x4623941,x4623942),f2(x4623941,x4623942))),x4623942),x4623941))),
% 66.84/67.09 inference(scs_inference,[],[462044,462384,8])).
% 66.84/67.09 cnf(462419,plain,
% 66.84/67.09 (P2(f2(x4624191,f2(x4624192,f2(f2(x4624193,f2(x4624194,f2(x4624195,f2(x4624196,x4624197)))),f1(x4624197)))))),
% 66.84/67.09 inference(scs_inference,[],[462140,462108,8])).
% 66.84/67.09 cnf(462426,plain,
% 66.84/67.09 (P2(f2(x4624261,f2(f2(x4624262,f2(x4624263,f2(x4624264,f2(x4624265,x4624266)))),f1(x4624266))))),
% 66.84/67.09 inference(scs_inference,[],[462174,462419,8])).
% 66.84/67.09 cnf(462484,plain,
% 66.84/67.09 (P2(f2(x4624841,f2(x4624842,f2(x4624843,f1(f2(x4624843,x4624843))))))),
% 66.84/67.09 inference(scs_inference,[],[462361,462108,8])).
% 66.84/67.09 cnf(462491,plain,
% 66.84/67.09 (P2(f2(x4624911,f2(x4624912,f1(f2(x4624912,x4624912)))))),
% 66.84/67.09 inference(scs_inference,[],[462384,462484,8])).
% 66.84/67.09 cnf(462495,plain,
% 66.84/67.09 (P2(f2(x4624951,f1(f2(x4624951,x4624951))))),
% 66.84/67.09 inference(scs_inference,[],[462394,462491,8])).
% 66.84/67.09 cnf(462502,plain,
% 66.84/67.09 (~P2(f2(f1(a3),a3))),
% 66.84/67.09 inference(scs_inference,[],[462495,6,8])).
% 66.84/67.09 cnf(462506,plain,
% 66.84/67.09 (~P2(f2(f1(f2(x4625061,f2(f2(x4625062,f2(x4625063,f2(x4625064,f2(x4625065,x4625066)))),f1(x4625066)))),f2(f1(a3),a3)))),
% 66.84/67.09 inference(scs_inference,[],[462426,462502,8])).
% 66.84/67.09 cnf(462616,plain,
% 66.84/67.09 ($false),
% 66.84/67.09 inference(scs_inference,[],[462506,457543,457551,8]),
% 66.84/67.09 ['proof']).
% 67.03/67.24 % SZS output end Proof
% 67.03/67.24 % Total time :66.043236s
%------------------------------------------------------------------------------