%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL238-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 : n019.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:52 AM UTC 2026
% Result : Unsatisfiable 66.04s 66.26s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL238-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.10/0.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 4 22:18:23 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.23/0.53 start to proof:theBenchmark
% 66.04/66.25 %-------------------------------------------
% 66.04/66.25 % File :CSE---1.7
% 66.04/66.25 % Problem :theBenchmark
% 66.04/66.25 % Transform :cnf
% 66.04/66.25 % Format :tptp:raw
% 66.04/66.25 % Command :java -jar mcs_scs.jar %d %s
% 66.04/66.25
% 66.04/66.25 % Result :Theorem 65.695344s
% 66.04/66.25 % Output :CNFRefutation 65.695344s
% 66.04/66.25 %-------------------------------------------
% 66.04/66.26 %--------------------------------------------------------------------------
% 66.04/66.26 % File : LCL238-3 : TPTP v9.3.1. Released v2.3.0.
% 66.04/66.26 % Domain : Logic Calculi (Propositional)
% 66.04/66.26 % Problem : Principia Mathematica 3.22
% 66.04/66.26 % Version : [WR27] axioms.
% 66.04/66.26 % English :
% 66.04/66.26
% 66.04/66.26 % Refs : [WR27] Whitehead & Russell (1927), Principia Mathematica
% 66.04/66.26 % Source : [WR27]
% 66.04/66.26 % Names : Problem 3.22 [WR27]
% 66.04/66.26
% 66.04/66.26 % Status : Unsatisfiable
% 66.04/66.26 % Rating : 0.00 v9.3.0, 0.17 v9.1.0, 0.08 v9.0.0, 0.12 v8.2.0, 0.17 v8.1.0, 0.11 v7.5.0, 0.20 v7.4.0, 0.22 v7.3.0, 0.33 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.50 v5.4.0, 0.53 v5.3.0, 0.50 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.29 v2.5.0, 0.20 v2.4.0, 0.00 v2.3.0
% 66.04/66.26 % Syntax : Number of clauses : 10 ( 8 unt; 0 nHn; 3 RR)
% 66.04/66.26 % Number of literals : 13 ( 2 equ; 4 neg)
% 66.04/66.26 % Maximal clause size : 3 ( 1 avg)
% 66.04/66.26 % Maximal term depth : 4 ( 2 avg)
% 66.04/66.26 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 66.04/66.26 % Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% 66.04/66.26 % Number of variables : 18 ( 1 sgn)
% 66.04/66.26 % SPC : CNF_UNS_RFO_SEQ_HRN
% 66.04/66.26
% 66.04/66.26 % Comments :
% 66.04/66.26 %--------------------------------------------------------------------------
% 66.04/66.26 %----Include axioms of propositional logic
% 66.04/66.26 include('Axioms/LCL004-0.ax').
% 66.04/66.26 include('Axioms/LCL004-1.ax').
% 66.04/66.26 %--------------------------------------------------------------------------
% 66.04/66.26 cnf(prove_this,negated_conjecture,
% 66.04/66.26 ~ theorem(implies(and(p,q),and(q,p))) ).
% 66.04/66.26
% 66.04/66.26 %--------------------------------------------------------------------------
% 66.04/66.26 %-------------------------------------------
% 66.04/66.26 % Proof found
% 66.04/66.26 % SZS status Theorem for theBenchmark
% 66.04/66.26 % SZS output start Proof
% 66.04/66.26 %ClaNum:8(EqnAxiom:0)
% 66.04/66.26 %VarNum:28(SingletonVarNum:14)
% 66.04/66.26 %MaxLitNum:3
% 66.04/66.26 %MaxfuncDepth:4
% 66.04/66.26 %SharedTerms:11
% 66.04/66.26 %goalClause: 6
% 66.04/66.26 %singleGoalClaCount:1
% 66.04/66.26 [6]~P2(f2(f1(f1(f2(f1(a3),f1(a4)))),f1(f2(f1(a4),f1(a3)))))
% 66.04/66.26 [2]P1(f2(f1(f2(x21,x21)),x21))
% 66.04/66.26 [1]P1(f2(f1(x11),f2(x12,x11)))
% 66.04/66.26 [3]P1(f2(f1(f2(x31,x32)),f2(x32,x31)))
% 66.04/66.26 [4]P1(f2(f1(f2(x41,f2(x42,x43))),f2(x42,f2(x41,x43))))
% 66.04/66.26 [5]P1(f2(f1(f2(f1(x51),x52)),f2(f1(f2(x53,x51)),f2(x53,x52))))
% 66.04/66.26 [7]~P1(x71)+P2(x71)
% 66.04/66.26 [8]P2(x81)+~P2(x82)+~P2(f2(f1(x82),x81))
% 66.04/66.26 %EqnAxiom
% 66.04/66.26
% 66.04/66.26 %-------------------------------------------
% 66.35/66.59 cnf(320923,plain,
% 66.35/66.59 (~P2(f2(f1(f2(f1(x3209231),f2(x3209232,x3209231))),f2(f1(f1(f2(f1(a3),f1(a4)))),f1(f2(f1(a4),f1(a3))))))),
% 66.35/66.59 inference(scs_inference,[],[6,1,7,8])).
% 66.35/66.59 cnf(320925,plain,
% 66.35/66.59 (P2(f2(f1(f2(x3209251,x3209252)),f2(x3209252,x3209251)))),
% 66.35/66.59 inference(scs_inference,[],[3,7])).
% 66.35/66.59 cnf(320927,plain,
% 66.35/66.59 (P2(f2(f1(f2(x3209271,x3209271)),x3209271))),
% 66.35/66.59 inference(scs_inference,[],[2,7])).
% 66.35/66.59 cnf(320931,plain,
% 66.35/66.59 (P2(f2(f1(f2(f1(x3209311),x3209312)),f2(f1(f2(x3209313,x3209311)),f2(x3209313,x3209312))))),
% 66.35/66.59 inference(scs_inference,[],[5,7])).
% 66.35/66.59 cnf(320940,plain,
% 66.35/66.59 (~P2(f2(f1(f2(x3209401,f1(f2(f1(a3),f1(a4))))),f1(f2(f1(a4),f1(a3)))))),
% 66.35/66.59 inference(scs_inference,[],[5,320923,7,8])).
% 66.35/66.59 cnf(320956,plain,
% 66.35/66.59 (P2(f2(x3209561,f1(f2(x3209561,x3209561))))),
% 66.35/66.59 inference(scs_inference,[],[3,320927,7,8])).
% 66.35/66.59 cnf(321007,plain,
% 66.35/66.59 (P2(f2(f1(f2(x3210071,f2(f1(x3210072),x3210073))),f2(x3210071,f2(f1(f2(x3210074,x3210072)),f2(x3210074,x3210073)))))),
% 66.35/66.59 inference(scs_inference,[],[5,320931,7,8])).
% 66.35/66.59 cnf(321011,plain,
% 66.35/66.59 (P2(f2(x3210111,f2(f1(f2(x3210112,x3210113)),f2(x3210113,x3210112))))),
% 66.35/66.59 inference(scs_inference,[],[1,320925,7,8])).
% 66.35/66.59 cnf(321016,plain,
% 66.35/66.59 (P2(f2(x3210161,f2(f1(f2(x3210161,f2(f1(x3210162),x3210163))),f2(f1(f2(x3210164,x3210162)),f2(x3210164,x3210163)))))),
% 66.35/66.59 inference(scs_inference,[],[4,321007,7,8])).
% 66.35/66.59 cnf(321067,plain,
% 66.35/66.59 (P2(f2(f1(f2(f1(f2(x3210671,f1(f2(x3210671,x3210671)))),f2(f1(x3210672),x3210673))),f2(f1(f2(x3210674,x3210672)),f2(x3210674,x3210673))))),
% 66.35/66.59 inference(scs_inference,[],[321016,320956,8])).
% 66.35/66.59 cnf(321073,plain,
% 66.35/66.59 (P2(f2(f1(f2(x3210731,f2(x3210732,x3210733))),f2(x3210731,f2(x3210733,x3210732))))),
% 66.35/66.59 inference(scs_inference,[],[321067,321011,8])).
% 66.35/66.59 cnf(321077,plain,
% 66.35/66.59 (P2(f2(f1(f2(f2(x3210771,x3210772),f2(x3210771,x3210772))),f2(x3210772,x3210771)))),
% 66.35/66.59 inference(scs_inference,[],[2,321073,7,8])).
% 66.35/66.59 cnf(321090,plain,
% 66.35/66.59 (P2(f2(f1(f2(x3210901,f2(f1(x3210902),x3210903))),f2(f1(f2(x3210904,x3210902)),f2(x3210904,f2(x3210901,x3210903)))))),
% 66.35/66.59 inference(scs_inference,[],[4,321007,7,8])).
% 66.35/66.59 cnf(321091,plain,
% 66.35/66.59 (P2(f2(f1(f2(x3210911,f2(f1(x3210912),x3210913))),f2(f1(f2(x3210914,f2(x3210915,x3210912))),f2(x3210914,f2(x3210915,f2(x3210911,x3210913))))))),
% 66.35/66.59 inference(scs_inference,[],[321007,321090,8])).
% 66.35/66.59 cnf(321116,plain,
% 66.35/66.59 (P2(f2(f1(f2(x3211161,f2(x3211162,x3211163))),f2(x3211161,f2(x3211162,f2(f1(f2(f1(x3211163),f2(x3211164,x3211165))),f2(x3211165,x3211164))))))),
% 66.35/66.59 inference(scs_inference,[],[321073,321091,8])).
% 66.35/66.59 cnf(321136,plain,
% 66.35/66.59 (P2(f2(f1(f2(f2(x3211361,x3211362),f2(x3211361,x3211362))),f2(x3211362,f2(f1(f2(f1(x3211361),f2(x3211363,x3211364))),f2(x3211364,x3211363)))))),
% 66.35/66.59 inference(scs_inference,[],[321077,321116,8])).
% 66.35/66.59 cnf(321142,plain,
% 66.35/66.59 (P2(f2(f2(x3211421,x3211422),f1(f2(x3211422,x3211421))))),
% 66.35/66.59 inference(scs_inference,[],[321077,321011,8])).
% 66.35/66.59 cnf(321151,plain,
% 66.35/66.59 (P2(f2(x3211511,f2(f2(x3211512,x3211513),f1(f2(x3211513,x3211512)))))),
% 66.35/66.59 inference(scs_inference,[],[1,321142,7,8])).
% 66.35/66.59 cnf(321160,plain,
% 66.35/66.59 (P2(f2(f1(f2(x3211601,x3211602)),f2(f1(f2(f1(f2(x3211602,x3211601)),f2(x3211603,x3211604))),f2(x3211604,x3211603))))),
% 66.35/66.59 inference(scs_inference,[],[321151,321136,8])).
% 66.35/66.59 cnf(321166,plain,
% 66.35/66.59 (P2(f2(f1(f2(f1(f2(f1(f2(x3211661,x3211662)),f2(x3211662,x3211661))),f2(x3211663,x3211664))),f2(x3211664,x3211663)))),
% 66.35/66.59 inference(scs_inference,[],[321160,321142,8])).
% 66.35/66.59 cnf(321354,plain,
% 66.35/66.59 (P2(f2(f1(f2(x3213541,x3213542)),f2(x3213541,f1(f2(f1(x3213542),f1(x3213542))))))),
% 66.35/66.59 inference(scs_inference,[],[5,320956,7,8])).
% 66.35/66.59 cnf(321578,plain,
% 66.35/66.59 ($false),
% 66.35/66.59 inference(scs_inference,[],[321354,321166,320940,8]),
% 66.35/66.59 ['proof']).
% 66.47/66.69 % SZS output end Proof
% 66.47/66.69 % Total time :65.695344s
%------------------------------------------------------------------------------