%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL202-3 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n027.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:47 AM UTC 2026
% Result : Unsatisfiable 285.51s 285.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL202-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.36 % Computer : n027.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sat Sep 5 22:00:58 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.24/0.53 start to proof:theBenchmark
% 285.51/285.53 %-------------------------------------------
% 285.51/285.53 % File :CSE---1.7
% 285.51/285.53 % Problem :theBenchmark
% 285.51/285.53 % Transform :cnf
% 285.51/285.53 % Format :tptp:raw
% 285.51/285.53 % Command :java -jar mcs_scs.jar %d %s
% 285.51/285.53
% 285.51/285.53 % Result :Theorem 284.956507s
% 285.51/285.53 % Output :CNFRefutation 284.956507s
% 285.51/285.53 %-------------------------------------------
% 285.51/285.54 %--------------------------------------------------------------------------
% 285.51/285.54 % File : LCL202-3 : TPTP v9.3.1. Released v2.3.0.
% 285.51/285.54 % Domain : Logic Calculi (Propositional)
% 285.51/285.54 % Problem : Principia Mathematica 2.48
% 285.51/285.54 % Version : [WR27] axioms.
% 285.51/285.54 % English :
% 285.51/285.54
% 285.51/285.54 % Refs : [WR27] Whitehead & Russell (1927), Principia Mathematica
% 285.51/285.54 % Source : [WR27]
% 285.51/285.54 % Names : Problem 2.48 [WR27]
% 285.51/285.54
% 285.51/285.54 % Status : Unsatisfiable
% 285.51/285.54 % Rating : 0.00 v9.3.0, 0.17 v9.1.0, 0.15 v9.0.0, 0.19 v8.2.0, 0.08 v8.1.0, 0.11 v7.5.0, 0.10 v7.4.0, 0.22 v7.2.0, 0.25 v7.1.0, 0.29 v6.3.0, 0.17 v6.2.0, 0.00 v6.0.0, 0.33 v5.5.0, 0.44 v5.4.0, 0.40 v5.3.0, 0.33 v5.2.0, 0.38 v5.1.0, 0.29 v4.1.0, 0.22 v4.0.1, 0.00 v4.0.0, 0.17 v3.5.0, 0.00 v3.4.0, 0.17 v3.3.0, 0.29 v3.2.0, 0.00 v3.1.0, 0.22 v2.7.0, 0.17 v2.6.0, 0.43 v2.5.0, 0.20 v2.4.0, 0.00 v2.3.0
% 285.51/285.54 % Syntax : Number of clauses : 9 ( 7 unt; 0 nHn; 3 RR)
% 285.51/285.54 % Number of literals : 12 ( 1 equ; 4 neg)
% 285.51/285.54 % Maximal clause size : 3 ( 1 avg)
% 285.51/285.54 % Maximal term depth : 4 ( 2 avg)
% 285.51/285.54 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 285.51/285.54 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 285.51/285.54 % Number of variables : 16 ( 1 sgn)
% 285.51/285.54 % SPC : CNF_UNS_RFO_SEQ_HRN
% 285.51/285.54
% 285.51/285.54 % Comments :
% 285.51/285.54 %--------------------------------------------------------------------------
% 285.51/285.54 %----Include axioms of propositional logic
% 285.51/285.54 include('Axioms/LCL004-0.ax').
% 285.51/285.54 %--------------------------------------------------------------------------
% 285.51/285.54 cnf(prove_this,negated_conjecture,
% 285.51/285.54 ~ theorem(implies(not(or(p,q)),or(p,not(q)))) ).
% 285.51/285.54
% 285.51/285.54 %--------------------------------------------------------------------------
% 285.51/285.54 %-------------------------------------------
% 285.51/285.54 % Proof found
% 285.51/285.54 % SZS status Theorem for theBenchmark
% 285.51/285.54 % SZS output start Proof
% 285.51/285.54 %ClaNum:8(EqnAxiom:0)
% 285.51/285.54 %VarNum:28(SingletonVarNum:14)
% 285.51/285.54 %MaxLitNum:3
% 285.51/285.54 %MaxfuncDepth:3
% 285.51/285.54 %SharedTerms:8
% 285.51/285.54 %goalClause: 6
% 285.51/285.54 %singleGoalClaCount:1
% 285.51/285.54 [6]~P2(f2(f1(f1(f2(a3,a4))),f2(a3,f1(a4))))
% 285.51/285.54 [2]P1(f2(f1(f2(x21,x21)),x21))
% 285.51/285.54 [1]P1(f2(f1(x11),f2(x12,x11)))
% 285.51/285.54 [3]P1(f2(f1(f2(x31,x32)),f2(x32,x31)))
% 285.51/285.54 [4]P1(f2(f1(f2(x41,f2(x42,x43))),f2(x42,f2(x41,x43))))
% 285.51/285.54 [5]P1(f2(f1(f2(f1(x51),x52)),f2(f1(f2(x53,x51)),f2(x53,x52))))
% 285.51/285.54 [7]~P1(x71)+P2(x71)
% 285.51/285.54 [8]P2(x81)+~P2(x82)+~P2(f2(f1(x82),x81))
% 285.51/285.54 %EqnAxiom
% 285.51/285.54
% 285.51/285.54 %-------------------------------------------
% 285.82/285.89 cnf(342979,plain,
% 285.82/285.89 (P2(f2(f1(x3429791),f2(x3429792,x3429791)))),
% 285.82/285.89 inference(scs_inference,[],[1,7])).
% 285.82/285.89 cnf(342983,plain,
% 285.82/285.89 (P2(f2(f1(f2(x3429831,x3429832)),f2(x3429832,x3429831)))),
% 285.82/285.89 inference(scs_inference,[],[3,7])).
% 285.82/285.89 cnf(342987,plain,
% 285.82/285.89 (P2(f2(f1(f2(x3429871,x3429871)),x3429871))),
% 285.82/285.89 inference(scs_inference,[],[2,7])).
% 285.82/285.89 cnf(342989,plain,
% 285.82/285.89 (P2(f2(f1(f2(x3429891,f2(x3429892,x3429893))),f2(x3429892,f2(x3429891,x3429893))))),
% 285.82/285.89 inference(scs_inference,[],[4,7])).
% 285.82/285.89 cnf(342991,plain,
% 285.82/285.89 (P2(f2(f1(f2(f1(x3429911),x3429912)),f2(f1(f2(x3429913,x3429911)),f2(x3429913,x3429912))))),
% 285.82/285.89 inference(scs_inference,[],[5,7])).
% 285.82/285.89 cnf(342999,plain,
% 285.82/285.89 (P2(f2(f2(x3429991,x3429992),f1(x3429992)))),
% 285.82/285.89 inference(scs_inference,[],[3,342979,7,8])).
% 285.82/285.89 cnf(343617,plain,
% 285.82/285.89 (P2(f2(x3436171,f2(f1(f2(x3436172,f2(x3436173,x3436174))),f2(x3436173,f2(x3436172,x3436174)))))),
% 285.82/285.89 inference(scs_inference,[],[1,342989,7,8])).
% 285.82/285.89 cnf(343620,plain,
% 285.82/285.89 (P2(f2(f1(f2(x3436201,f2(x3436202,x3436203))),f2(x3436204,f2(x3436202,f2(x3436201,x3436203)))))),
% 285.82/285.89 inference(scs_inference,[],[4,343617,7,8])).
% 285.82/285.89 cnf(344997,plain,
% 285.82/285.89 (P2(f2(f1(f2(x3449971,x3449972)),f2(f1(f2(f1(x3449972),x3449973)),f2(x3449971,x3449973))))),
% 285.82/285.89 inference(scs_inference,[],[4,342991,7,8])).
% 285.82/285.89 cnf(344999,plain,
% 285.82/285.89 (P2(f2(x3449991,f2(f1(f2(x3449992,x3449993)),f2(f1(f2(f1(x3449993),x3449994)),f2(x3449992,x3449994)))))),
% 285.82/285.89 inference(scs_inference,[],[1,344997,7,8])).
% 285.82/285.89 cnf(345003,plain,
% 285.82/285.89 (P2(f2(f1(f2(x3450031,x3450032)),f2(x3450031,f2(f1(f2(x3450033,x3450034)),f2(f1(f2(f1(x3450034),x3450035)),f2(x3450033,x3450035))))))),
% 285.82/285.89 inference(scs_inference,[],[5,344999,7,8])).
% 285.82/285.89 cnf(345178,plain,
% 285.82/285.89 (P2(f2(f1(f2(x3451781,x3451782)),f2(x3451783,f2(f1(f2(f1(x3451782),x3451784)),f2(x3451781,x3451784)))))),
% 285.82/285.89 inference(scs_inference,[],[4,344999,7,8])).
% 285.82/285.89 cnf(345650,plain,
% 285.82/285.89 (P2(f2(f1(f2(x3456501,f2(x3456502,x3456503))),f2(x3456501,f2(x3456504,f2(f1(f2(f1(x3456503),x3456505)),f2(x3456502,x3456505))))))),
% 285.82/285.89 inference(scs_inference,[],[5,345178,7,8])).
% 285.82/285.89 cnf(345660,plain,
% 285.82/285.89 (P2(f2(f2(x3456601,f2(f1(f2(f1(x3456602),x3456603)),f2(x3456604,x3456603))),f1(f2(x3456604,x3456602))))),
% 285.82/285.89 inference(scs_inference,[],[3,345178,7,8])).
% 285.82/285.89 cnf(346070,plain,
% 285.82/285.89 (P2(f2(x3460701,f2(f1(f2(f1(f1(x3460702)),x3460703)),f2(f2(x3460704,x3460702),x3460703))))),
% 285.82/285.89 inference(scs_inference,[],[345178,342999,8])).
% 285.82/285.89 cnf(346074,plain,
% 285.82/285.89 (P2(f2(f1(f2(f1(f1(x3460741)),x3460742)),f2(f2(x3460743,x3460741),x3460742)))),
% 285.82/285.89 inference(scs_inference,[],[345660,346070,8])).
% 285.82/285.89 cnf(346083,plain,
% 285.82/285.89 (P2(f2(f2(x3460831,x3460832),f2(x3460833,f1(x3460832))))),
% 285.82/285.89 inference(scs_inference,[],[346074,342979,8])).
% 285.82/285.89 cnf(346198,plain,
% 285.82/285.89 (P2(f2(x3461981,f2(f1(f2(f1(x3461982),x3461983)),f2(f1(f2(x3461984,x3461982)),f2(x3461984,x3461983)))))),
% 285.82/285.89 inference(scs_inference,[],[344997,343620,8])).
% 285.82/285.89 cnf(346229,plain,
% 285.82/285.89 (P2(f2(f1(f2(f1(x3462291),x3462292)),f2(x3462293,f2(f1(f2(x3462294,x3462291)),f2(x3462294,x3462292)))))),
% 285.82/285.89 inference(scs_inference,[],[346198,342989,8])).
% 285.82/285.89 cnf(346413,plain,
% 285.82/285.89 (P2(f2(x3464131,f2(f1(f2(x3464132,x3464133)),f2(x3464132,f2(x3464134,x3464133)))))),
% 285.82/285.89 inference(scs_inference,[],[346229,342979,8])).
% 285.82/285.89 cnf(346418,plain,
% 285.82/285.89 (P2(f2(f1(f2(x3464181,x3464182)),f2(x3464181,f2(x3464183,x3464182))))),
% 285.82/285.89 inference(scs_inference,[],[346229,346413,8])).
% 285.82/285.89 cnf(346727,plain,
% 285.82/285.89 (~P2(f2(f1(f1(f2(a3,a4))),f1(a4)))),
% 285.82/285.89 inference(scs_inference,[],[346418,6,8])).
% 285.82/285.89 cnf(346964,plain,
% 285.82/285.89 (~P2(f2(f1(a4),f1(f1(f2(a3,a4)))))),
% 285.82/285.89 inference(scs_inference,[],[346727,342983,8])).
% 285.82/285.89 cnf(347427,plain,
% 285.82/285.89 (P2(f2(x3474271,f2(f2(x3474272,x3474273),f2(x3474274,f1(x3474273)))))),
% 285.82/285.89 inference(scs_inference,[],[342979,346083,8])).
% 285.82/285.89 cnf(347431,plain,
% 285.82/285.89 (P2(f2(x3474311,f2(f1(f2(f1(f2(x3474312,x3474313)),x3474314)),f2(f1(x3474313),x3474314))))),
% 285.82/285.89 inference(scs_inference,[],[342979,345178,8])).
% 285.82/285.89 cnf(347442,plain,
% 285.82/285.89 (P2(f2(f1(f2(f1(f2(x3474421,x3474422)),x3474423)),f2(f1(x3474422),x3474423)))),
% 285.82/285.89 inference(scs_inference,[],[342979,347431,8])).
% 285.82/285.89 cnf(348346,plain,
% 285.82/285.89 (~P2(f2(f1(f2(x3483461,a4)),f1(f1(f2(a3,a4)))))),
% 285.82/285.89 inference(scs_inference,[],[346964,347442,8])).
% 285.82/285.89 cnf(348377,plain,
% 285.82/285.89 (P2(f2(x3483771,f2(f1(f2(f1(x3483772),x3483773)),f2(f1(f2(x3483772,x3483772)),x3483773))))),
% 285.82/285.89 inference(scs_inference,[],[6,342987,345178,7,8])).
% 285.82/285.89 cnf(348383,plain,
% 285.82/285.89 (P2(f2(f1(f2(f1(x3483831),x3483832)),f2(f1(f2(x3483831,x3483831)),x3483832)))),
% 285.82/285.89 inference(scs_inference,[],[6,342987,348377,7,8])).
% 285.82/285.89 cnf(348389,plain,
% 285.82/285.89 (P2(f2(f1(f2(f2(x3483891,x3483892),f2(x3483891,x3483892))),f2(x3483893,f2(f1(f2(f1(x3483892),x3483894)),f2(x3483891,x3483894)))))),
% 285.82/285.89 inference(scs_inference,[],[6,342987,345650,7,8])).
% 285.82/285.89 cnf(352920,plain,
% 285.82/285.89 (P2(f2(f2(f2(x3529201,x3529202),f2(x3529203,f1(x3529202))),x3529204))),
% 285.82/285.89 inference(scs_inference,[],[347427,342983,8])).
% 285.82/285.89 cnf(353047,plain,
% 285.82/285.89 (P2(f2(x3530471,f2(f1(f2(f1(f2(x3530472,f1(x3530473))),x3530474)),f2(f2(x3530475,x3530473),x3530474))))),
% 285.82/285.89 inference(scs_inference,[],[352920,348389,8])).
% 285.82/285.89 cnf(353052,plain,
% 285.82/285.89 (P2(f2(f1(f2(f1(f2(x3530521,f1(x3530522))),x3530523)),f2(f2(x3530524,x3530522),x3530523)))),
% 285.82/285.89 inference(scs_inference,[],[353047,345003,8])).
% 285.82/285.89 cnf(353793,plain,
% 285.82/285.89 (P2(f2(f2(x3537931,x3537932),f2(f1(x3537932),x3537933)))),
% 285.82/285.89 inference(scs_inference,[],[342983,353052,8])).
% 285.82/285.89 cnf(353816,plain,
% 285.82/285.89 (P2(f2(f1(f2(f2(x3538161,x3538162),f2(x3538161,x3538162))),f2(x3538162,x3538161)))),
% 285.82/285.89 inference(scs_inference,[],[342983,348383,8])).
% 285.82/285.89 cnf(353820,plain,
% 285.82/285.89 ($false),
% 285.82/285.89 inference(scs_inference,[],[353816,353793,348346,8]),
% 285.82/285.89 ['proof']).
% 285.93/286.00 % SZS output end Proof
% 285.93/286.00 % Total time :284.956507s
%------------------------------------------------------------------------------