%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL274-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 : n017.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 183.08s 183.19s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL274-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 : n017.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 22:15:22 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.24/0.51 start to proof:theBenchmark
% 183.08/183.19 %-------------------------------------------
% 183.08/183.19 % File :CSE---1.7
% 183.08/183.19 % Problem :theBenchmark
% 183.08/183.19 % Transform :cnf
% 183.08/183.19 % Format :tptp:raw
% 183.08/183.19 % Command :java -jar mcs_scs.jar %d %s
% 183.08/183.19
% 183.08/183.19 % Result :Theorem 182.629293s
% 183.08/183.19 % Output :CNFRefutation 182.629293s
% 183.08/183.19 %-------------------------------------------
% 183.08/183.19 %--------------------------------------------------------------------------
% 183.08/183.19 % File : LCL274-3 : TPTP v9.3.1. Released v2.3.0.
% 183.08/183.19 % Domain : Logic Calculi (Propositional)
% 183.08/183.19 % Problem : Principia Mathematica 4.31
% 183.08/183.19 % Version : [WR27] axioms.
% 183.08/183.19 % English :
% 183.08/183.19
% 183.08/183.19 % Refs : [WR27] Whitehead & Russell (1927), Principia Mathematica
% 183.08/183.19 % Source : [WR27]
% 183.08/183.19 % Names : Problem 4.31 [WR27]
% 183.08/183.19
% 183.08/183.19 % Status : Unsatisfiable
% 183.08/183.19 % Rating : 0.00 v9.3.0, 0.17 v9.1.0, 0.00 v9.0.0, 0.12 v8.2.0, 0.17 v8.1.0, 0.11 v7.5.0, 0.20 v7.4.0, 0.11 v7.2.0, 0.12 v7.1.0, 0.14 v7.0.0, 0.29 v6.3.0, 0.33 v6.2.0, 0.00 v6.1.0, 0.20 v6.0.0, 0.67 v5.5.0, 0.75 v5.4.0, 0.73 v5.3.0, 0.75 v5.2.0, 0.62 v5.1.0, 0.57 v4.1.0, 0.56 v4.0.1, 0.50 v4.0.0, 0.67 v3.5.0, 0.50 v3.3.0, 0.57 v3.2.0, 0.43 v3.1.0, 0.56 v2.7.0, 0.33 v2.6.0, 0.43 v2.5.0, 0.20 v2.4.0, 0.33 v2.3.0
% 183.08/183.19 % Syntax : Number of clauses : 11 ( 9 unt; 0 nHn; 3 RR)
% 183.08/183.19 % Number of literals : 14 ( 3 equ; 4 neg)
% 183.08/183.19 % Maximal clause size : 3 ( 1 avg)
% 183.08/183.19 % Maximal term depth : 4 ( 2 avg)
% 183.08/183.19 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 183.08/183.19 % Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% 183.08/183.19 % Number of variables : 20 ( 1 sgn)
% 183.08/183.19 % SPC : CNF_UNS_RFO_SEQ_HRN
% 183.08/183.19
% 183.08/183.19 % Comments :
% 183.08/183.19 %--------------------------------------------------------------------------
% 183.08/183.19 %----Include axioms of propositional logic
% 183.08/183.19 include('Axioms/LCL004-0.ax').
% 183.08/183.19 include('Axioms/LCL004-1.ax').
% 183.08/183.19 include('Axioms/LCL004-2.ax').
% 183.08/183.19 %--------------------------------------------------------------------------
% 183.08/183.19 cnf(prove_this,negated_conjecture,
% 183.08/183.19 ~ theorem(equivalent(or(p,q),or(q,p))) ).
% 183.08/183.19
% 183.08/183.19 %--------------------------------------------------------------------------
% 183.08/183.19 %-------------------------------------------
% 183.08/183.19 % Proof found
% 183.08/183.19 % SZS status Theorem for theBenchmark
% 183.08/183.19 % SZS output start Proof
% 183.08/183.19 %ClaNum:8(EqnAxiom:0)
% 183.08/183.19 %VarNum:28(SingletonVarNum:14)
% 183.08/183.19 %MaxLitNum:3
% 183.08/183.19 %MaxfuncDepth:5
% 183.08/183.19 %SharedTerms:13
% 183.08/183.19 %goalClause: 6
% 183.08/183.19 %singleGoalClaCount:1
% 183.08/183.19 [6]~P2(f1(f2(f1(f2(f1(f2(a3,a4)),f2(a4,a3))),f1(f2(f1(f2(a4,a3)),f2(a3,a4))))))
% 183.08/183.19 [2]P1(f2(f1(f2(x21,x21)),x21))
% 183.08/183.19 [1]P1(f2(f1(x11),f2(x12,x11)))
% 183.08/183.19 [3]P1(f2(f1(f2(x31,x32)),f2(x32,x31)))
% 183.08/183.19 [4]P1(f2(f1(f2(x41,f2(x42,x43))),f2(x42,f2(x41,x43))))
% 183.08/183.19 [5]P1(f2(f1(f2(f1(x51),x52)),f2(f1(f2(x53,x51)),f2(x53,x52))))
% 183.08/183.19 [7]~P1(x71)+P2(x71)
% 183.08/183.19 [8]P2(x81)+~P2(x82)+~P2(f2(f1(x82),x81))
% 183.08/183.19 %EqnAxiom
% 183.08/183.19
% 183.08/183.19 %-------------------------------------------
% 183.34/183.49 cnf(288519,plain,
% 183.34/183.49 (P2(f2(f1(x2885191),f2(x2885192,x2885191)))),
% 183.34/183.49 inference(scs_inference,[],[1,7])).
% 183.34/183.49 cnf(288523,plain,
% 183.34/183.49 (P2(f2(f1(f2(x2885231,x2885232)),f2(x2885232,x2885231)))),
% 183.34/183.49 inference(scs_inference,[],[3,7])).
% 183.34/183.49 cnf(288527,plain,
% 183.34/183.49 (P2(f2(f1(f2(x2885271,f2(x2885272,x2885273))),f2(x2885272,f2(x2885271,x2885273))))),
% 183.34/183.49 inference(scs_inference,[],[4,7])).
% 183.34/183.49 cnf(288529,plain,
% 183.34/183.49 (P2(f2(f1(f2(f1(x2885291),x2885292)),f2(f1(f2(x2885293,x2885291)),f2(x2885293,x2885292))))),
% 183.34/183.49 inference(scs_inference,[],[5,7])).
% 183.34/183.49 cnf(288532,plain,
% 183.34/183.49 (~P2(f2(f1(f2(f1(f2(x2885321,x2885322)),f2(x2885322,x2885321))),f1(f2(f1(f2(f1(f2(a3,a4)),f2(a4,a3))),f1(f2(f1(f2(a4,a3)),f2(a3,a4)))))))),
% 183.34/183.49 inference(scs_inference,[],[3,6,7,8])).
% 183.34/183.49 cnf(288535,plain,
% 183.34/183.49 (P2(f2(x2885351,f2(f1(x2885352),f2(x2885353,x2885352))))),
% 183.34/183.49 inference(scs_inference,[],[1,288519,7,8])).
% 183.34/183.49 cnf(288536,plain,
% 183.34/183.49 (P2(f2(x2885361,f2(f1(f2(x2885362,x2885363)),f2(x2885363,x2885362))))),
% 183.34/183.49 inference(scs_inference,[],[1,288523,7,8])).
% 183.34/183.49 cnf(290563,plain,
% 183.34/183.49 (P2(f2(f1(f2(x2905631,x2905632)),f2(x2905631,f2(f1(f2(x2905633,x2905634)),f2(x2905634,x2905633)))))),
% 183.34/183.49 inference(scs_inference,[],[288536,288529,8])).
% 183.34/183.49 cnf(290568,plain,
% 183.34/183.49 (P2(f2(x2905681,f2(f1(f2(x2905682,x2905683)),f2(x2905682,f2(f1(f2(x2905684,x2905685)),f2(x2905685,x2905684))))))),
% 183.34/183.49 inference(scs_inference,[],[290563,288519,8])).
% 183.34/183.49 cnf(290577,plain,
% 183.34/183.49 (P2(f2(f2(x2905771,f2(f1(f2(x2905772,x2905773)),f2(x2905773,x2905772))),f1(f2(x2905771,x2905774))))),
% 183.34/183.49 inference(scs_inference,[],[290563,288523,8])).
% 183.34/183.49 cnf(290605,plain,
% 183.34/183.49 (P2(f2(f1(f2(x2906051,x2906052)),f2(x2906053,f2(x2906051,f2(f1(f2(x2906054,x2906055)),f2(x2906055,x2906054))))))),
% 183.34/183.49 inference(scs_inference,[],[290568,288527,8])).
% 183.34/183.49 cnf(290614,plain,
% 183.34/183.49 (P2(f2(x2906141,f2(x2906142,f2(f1(f2(x2906143,x2906144)),f2(x2906144,x2906143)))))),
% 183.34/183.49 inference(scs_inference,[],[290568,290605,8])).
% 183.34/183.49 cnf(290671,plain,
% 183.34/183.49 (P2(f2(x2906711,f2(f1(f2(x2906712,x2906711)),x2906712)))),
% 183.34/183.49 inference(scs_inference,[],[288523,288527,8])).
% 183.34/183.49 cnf(290685,plain,
% 183.34/183.49 (P2(f2(f1(f2(x2906851,f2(x2906852,f2(x2906853,x2906854)))),f2(x2906851,f2(x2906853,f2(x2906852,x2906854)))))),
% 183.34/183.49 inference(scs_inference,[],[288527,288529,8])).
% 183.34/183.49 cnf(290694,plain,
% 183.34/183.49 (P2(f2(f1(f2(x2906941,f1(f2(x2906942,f2(f1(x2906943),f2(x2906944,x2906943)))))),x2906941))),
% 183.34/183.49 inference(scs_inference,[],[288535,290671,8])).
% 183.34/183.49 cnf(290698,plain,
% 183.34/183.49 (P2(f2(x2906981,f2(x2906982,f2(f1(x2906983),x2906983))))),
% 183.34/183.49 inference(scs_inference,[],[288535,290685,8])).
% 183.34/183.49 cnf(290707,plain,
% 183.34/183.49 (P2(f2(x2907071,f2(f1(x2907072),x2907072)))),
% 183.34/183.49 inference(scs_inference,[],[290577,290698,6,7,8])).
% 183.34/183.49 cnf(290711,plain,
% 183.34/183.49 (P2(f2(f1(x2907111),x2907111))),
% 183.34/183.49 inference(scs_inference,[],[290577,290707,8])).
% 183.34/183.49 cnf(290718,plain,
% 183.34/183.49 (P2(f2(x2907181,f2(f1(f2(x2907182,x2907183)),f2(x2907184,f2(x2907183,x2907182)))))),
% 183.34/183.49 inference(scs_inference,[],[290614,290685,8])).
% 183.34/183.49 cnf(290732,plain,
% 183.34/183.49 (P2(f2(f1(f2(x2907321,x2907322)),f2(x2907323,f2(x2907322,x2907321))))),
% 183.34/183.49 inference(scs_inference,[],[290671,290718,6,7,8])).
% 183.34/183.49 cnf(290743,plain,
% 183.34/183.49 (P2(f1(f1(f2(x2907431,f2(f1(x2907432),f2(x2907433,x2907432))))))),
% 183.34/183.49 inference(scs_inference,[],[290694,290711,8])).
% 183.34/183.49 cnf(290748,plain,
% 183.34/183.49 (P2(f2(f1(f2(f2(x2907481,f2(x2907482,x2907483)),f1(f2(x2907484,f2(f1(x2907485),f2(x2907486,x2907485)))))),f2(x2907482,f2(x2907481,x2907483))))),
% 183.34/183.49 inference(scs_inference,[],[290694,290685,8])).
% 183.34/183.49 cnf(290758,plain,
% 183.34/183.49 (P2(f2(x2907581,f2(x2907582,f1(x2907582))))),
% 183.34/183.49 inference(scs_inference,[],[290711,290732,8])).
% 183.34/183.49 cnf(290770,plain,
% 183.34/183.49 (P2(f2(x2907701,f1(x2907701)))),
% 183.34/183.49 inference(scs_inference,[],[290748,290758,8])).
% 183.34/183.49 cnf(290928,plain,
% 183.34/183.49 (P2(f2(x2909281,f2(f2(f1(x2909282),x2909282),x2909283)))),
% 183.34/183.49 inference(scs_inference,[],[290707,290732,8])).
% 183.34/183.49 cnf(290940,plain,
% 183.34/183.49 (P2(f2(f2(f1(x2909401),x2909401),x2909402))),
% 183.34/183.49 inference(scs_inference,[],[290743,290928,8])).
% 183.34/183.49 cnf(290944,plain,
% 183.34/183.49 (P2(f2(x2909441,f2(f1(f2(x2909441,x2909442)),x2909442)))),
% 183.34/183.49 inference(scs_inference,[],[290940,290748,8])).
% 183.34/183.49 cnf(291223,plain,
% 183.34/183.49 (P2(f2(x2912231,f2(x2912232,f1(f2(x2912232,x2912232)))))),
% 183.34/183.49 inference(scs_inference,[],[2,290732,7,8])).
% 183.34/183.50 cnf(291224,plain,
% 183.34/183.50 (P2(f2(x2912241,f2(f2(x2912242,f1(f2(x2912242,x2912242))),x2912243)))),
% 183.34/183.50 inference(scs_inference,[],[290732,291223,8])).
% 183.34/183.50 cnf(291232,plain,
% 183.34/183.50 (P2(f2(f2(x2912321,f1(f2(x2912321,x2912321))),x2912322))),
% 183.34/183.50 inference(scs_inference,[],[290748,291224,8])).
% 183.34/183.50 cnf(291254,plain,
% 183.34/183.50 (P2(f1(f1(f2(f2(x2912541,f1(f2(x2912541,x2912541))),x2912542))))),
% 183.34/183.50 inference(scs_inference,[],[290770,291232,8])).
% 183.34/183.50 cnf(291407,plain,
% 183.34/183.50 (P2(f2(x2914071,f2(x2914072,f2(f1(f2(x2914072,x2914073)),x2914073))))),
% 183.34/183.50 inference(scs_inference,[],[1,290944,7,8])).
% 183.34/183.50 cnf(291412,plain,
% 183.34/183.50 (P2(f2(x2914121,f2(x2914122,f2(f1(f2(x2914121,x2914123)),x2914123))))),
% 183.34/183.50 inference(scs_inference,[],[4,291407,7,8])).
% 183.34/183.50 cnf(291905,plain,
% 183.34/183.50 (P2(f2(x2919051,f2(f1(f2(f1(f2(f1(f2(x2919052,x2919053)),f2(x2919053,x2919052))),x2919054)),x2919054)))),
% 183.34/183.50 inference(scs_inference,[],[3,291412,7,8])).
% 183.34/183.50 cnf(291927,plain,
% 183.34/183.50 (P2(f2(f1(f2(f1(f2(f1(f2(x2919271,x2919272)),f2(x2919272,x2919271))),x2919273)),x2919273))),
% 183.34/183.50 inference(scs_inference,[],[291254,291905,8])).
% 183.34/183.50 cnf(294032,plain,
% 183.34/183.50 ($false),
% 183.34/183.50 inference(scs_inference,[],[288523,288532,291927,8]),
% 183.34/183.50 ['proof']).
% 183.46/183.59 % SZS output end Proof
% 183.46/183.59 % Total time :182.629293s
%------------------------------------------------------------------------------