%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL182-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 : n029.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:45 AM UTC 2026
% Result : Unsatisfiable 110.78s 110.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL182-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.08/0.35 % Computer : n029.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 5 06:23:55 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.46 start to proof:theBenchmark
% 110.78/110.98 %-------------------------------------------
% 110.78/110.98 % File :CSE---1.7
% 110.78/110.98 % Problem :theBenchmark
% 110.78/110.98 % Transform :cnf
% 110.78/110.98 % Format :tptp:raw
% 110.78/110.98 % Command :java -jar mcs_scs.jar %d %s
% 110.78/110.98
% 110.78/110.98 % Result :Theorem 110.469859s
% 110.78/110.98 % Output :CNFRefutation 110.469859s
% 110.78/110.98 %-------------------------------------------
% 110.78/110.98 %--------------------------------------------------------------------------
% 110.78/110.98 % File : LCL182-3 : TPTP v9.3.1. Released v2.3.0.
% 110.78/110.98 % Domain : Logic Calculi (Propositional)
% 110.78/110.98 % Problem : Principia Mathematica 2.16
% 110.78/110.98 % Version : [WR27] axioms.
% 110.78/110.98 % English :
% 110.78/110.98
% 110.78/110.98 % Refs : [WR27] Whitehead & Russell (1927), Principia Mathematica
% 110.78/110.98 % Source : [WR27]
% 110.78/110.98 % Names : Problem 2.16 [WR27]
% 110.78/110.98
% 110.78/110.98 % Status : Unsatisfiable
% 110.78/110.98 % 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.22 v7.5.0, 0.20 v7.4.0, 0.33 v7.2.0, 0.38 v7.1.0, 0.43 v6.3.0, 0.33 v6.2.0, 0.00 v6.0.0, 0.33 v5.5.0, 0.56 v5.4.0, 0.47 v5.3.0, 0.42 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.7.0, 0.33 v3.5.0, 0.00 v3.4.0, 0.17 v3.3.0, 0.29 v3.2.0, 0.14 v3.1.0, 0.44 v2.7.0, 0.17 v2.6.0, 0.57 v2.5.0, 0.20 v2.4.0, 0.00 v2.3.0
% 110.78/110.98 % Syntax : Number of clauses : 9 ( 7 unt; 0 nHn; 3 RR)
% 110.78/110.98 % Number of literals : 12 ( 1 equ; 4 neg)
% 110.78/110.98 % Maximal clause size : 3 ( 1 avg)
% 110.78/110.98 % Maximal term depth : 4 ( 2 avg)
% 110.78/110.98 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 110.78/110.98 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 110.78/110.98 % Number of variables : 16 ( 1 sgn)
% 110.78/110.98 % SPC : CNF_UNS_RFO_SEQ_HRN
% 110.78/110.99
% 110.78/110.99 % Comments :
% 110.78/110.99 %--------------------------------------------------------------------------
% 110.78/110.99 %----Include axioms of propositional logic
% 110.78/110.99 include('Axioms/LCL004-0.ax').
% 110.78/110.99 %--------------------------------------------------------------------------
% 110.78/110.99 cnf(prove_this,negated_conjecture,
% 110.78/110.99 ~ theorem(implies(implies(p,q),implies(not(q),not(p)))) ).
% 110.78/110.99
% 110.78/110.99 %--------------------------------------------------------------------------
% 110.78/110.99 %-------------------------------------------
% 110.78/110.99 % Proof found
% 110.78/110.99 % SZS status Theorem for theBenchmark
% 110.78/110.99 % SZS output start Proof
% 110.78/110.99 %ClaNum:8(EqnAxiom:0)
% 110.78/110.99 %VarNum:28(SingletonVarNum:14)
% 110.78/110.99 %MaxLitNum:3
% 110.78/110.99 %MaxfuncDepth:3
% 110.78/110.99 %SharedTerms:10
% 110.78/110.99 %goalClause: 6
% 110.78/110.99 %singleGoalClaCount:1
% 110.78/110.99 [6]~P2(f2(f1(f2(f1(a3),a4)),f2(f1(f1(a4)),f1(a3))))
% 110.78/110.99 [2]P1(f2(f1(f2(x21,x21)),x21))
% 110.78/110.99 [1]P1(f2(f1(x11),f2(x12,x11)))
% 110.78/110.99 [3]P1(f2(f1(f2(x31,x32)),f2(x32,x31)))
% 110.78/110.99 [4]P1(f2(f1(f2(x41,f2(x42,x43))),f2(x42,f2(x41,x43))))
% 110.78/110.99 [5]P1(f2(f1(f2(f1(x51),x52)),f2(f1(f2(x53,x51)),f2(x53,x52))))
% 110.78/110.99 [7]~P1(x71)+P2(x71)
% 110.78/110.99 [8]P2(x81)+~P2(x82)+~P2(f2(f1(x82),x81))
% 110.78/110.99 %EqnAxiom
% 110.78/110.99
% 110.78/110.99 %-------------------------------------------
% 111.21/111.31 cnf(317557,plain,
% 111.21/111.31 (P2(f2(f1(x3175571),f2(x3175572,x3175571)))),
% 111.21/111.31 inference(scs_inference,[],[1,7])).
% 111.21/111.31 cnf(317561,plain,
% 111.21/111.31 (P2(f2(f1(f2(x3175611,x3175612)),f2(x3175612,x3175611)))),
% 111.21/111.31 inference(scs_inference,[],[3,7])).
% 111.21/111.32 cnf(317563,plain,
% 111.21/111.32 (P2(f2(f1(f2(x3175631,x3175631)),x3175631))),
% 111.21/111.32 inference(scs_inference,[],[2,7])).
% 111.21/111.32 cnf(317565,plain,
% 111.21/111.32 (P2(f2(f1(f2(x3175651,f2(x3175652,x3175653))),f2(x3175652,f2(x3175651,x3175653))))),
% 111.21/111.32 inference(scs_inference,[],[4,7])).
% 111.21/111.32 cnf(317567,plain,
% 111.21/111.32 (P2(f2(f1(f2(f1(x3175671),x3175672)),f2(f1(f2(x3175673,x3175671)),f2(x3175673,x3175672))))),
% 111.21/111.32 inference(scs_inference,[],[5,7])).
% 111.21/111.32 cnf(321772,plain,
% 111.21/111.32 (P2(f2(f1(f2(x3217721,f2(x3217722,f2(x3217723,x3217724)))),f2(x3217721,f2(x3217723,f2(x3217722,x3217724)))))),
% 111.21/111.32 inference(scs_inference,[],[317565,317567,8])).
% 111.21/111.32 cnf(321783,plain,
% 111.21/111.32 (P2(f2(f2(x3217831,f2(x3217832,f2(x3217833,x3217834))),f1(f2(x3217831,f2(x3217833,f2(x3217832,x3217834))))))),
% 111.21/111.32 inference(scs_inference,[],[321772,317561,8])).
% 111.21/111.32 cnf(321848,plain,
% 111.21/111.32 (P2(f2(f2(x3218481,x3218482),f1(f2(x3218482,x3218481))))),
% 111.21/111.32 inference(scs_inference,[],[3,317561,7,8])).
% 111.21/111.32 cnf(321849,plain,
% 111.21/111.32 (P2(f2(f1(f2(f2(x3218491,x3218492),x3218493)),f2(x3218491,f2(x3218493,x3218492))))),
% 111.21/111.32 inference(scs_inference,[],[317561,321772,8])).
% 111.21/111.32 cnf(321859,plain,
% 111.21/111.32 (P2(f2(x3218591,f2(f1(x3218592),x3218592)))),
% 111.21/111.32 inference(scs_inference,[],[1,317565,7,8])).
% 111.21/111.32 cnf(321860,plain,
% 111.21/111.32 (P2(f2(f1(x3218601),x3218601))),
% 111.21/111.32 inference(scs_inference,[],[317565,321859,8])).
% 111.21/111.32 cnf(321874,plain,
% 111.21/111.32 (P2(f2(x3218741,f2(f1(f2(x3218742,x3218741)),x3218742)))),
% 111.21/111.32 inference(scs_inference,[],[321848,321849,8])).
% 111.21/111.32 cnf(321921,plain,
% 111.21/111.32 (P2(f2(f2(x3219211,f2(x3219212,x3219213)),f1(f2(f2(x3219211,x3219213),x3219212))))),
% 111.21/111.32 inference(scs_inference,[],[3,321849,7,8])).
% 111.21/111.32 cnf(321922,plain,
% 111.21/111.32 (P2(f2(x3219221,f2(f1(f2(f2(x3219221,x3219222),x3219223)),f2(x3219223,x3219222))))),
% 111.21/111.32 inference(scs_inference,[],[321849,321921,8])).
% 111.21/111.32 cnf(321934,plain,
% 111.21/111.32 (P2(f2(x3219341,f2(f2(f1(f2(f2(f2(x3219341,x3219342),x3219343),x3219344)),f2(x3219344,x3219343)),x3219342)))),
% 111.21/111.32 inference(scs_inference,[],[321922,321849,8])).
% 111.21/111.32 cnf(321944,plain,
% 111.21/111.32 (P2(f2(x3219441,f1(x3219441)))),
% 111.21/111.32 inference(scs_inference,[],[321860,317561,8])).
% 111.21/111.32 cnf(322015,plain,
% 111.21/111.32 (P2(f2(f2(f2(f1(f2(f2(f2(x3220151,x3220152),x3220153),x3220154)),f2(x3220154,x3220153)),x3220152),x3220151))),
% 111.21/111.32 inference(scs_inference,[],[321934,317561,8])).
% 111.21/111.32 cnf(322026,plain,
% 111.21/111.32 (P2(f2(f2(f1(f2(f2(f2(x3220261,x3220262),x3220263),x3220264)),f2(x3220264,x3220263)),f2(x3220261,x3220262)))),
% 111.21/111.32 inference(scs_inference,[],[322015,321849,8])).
% 111.21/111.32 cnf(322089,plain,
% 111.21/111.32 (P2(f2(x3220891,f2(f1(f2(x3220891,f2(x3220892,f2(x3220893,x3220894)))),f2(x3220893,f2(x3220892,x3220894)))))),
% 111.21/111.32 inference(scs_inference,[],[321783,321849,8])).
% 111.21/111.32 cnf(322096,plain,
% 111.21/111.32 (~P2(f2(f2(f1(f2(f1(a3),a4)),f1(a3)),f1(f1(a4))))),
% 111.21/111.32 inference(scs_inference,[],[321849,6,8])).
% 111.21/111.32 cnf(322100,plain,
% 111.21/111.32 (P2(f2(x3221001,f2(x3221002,f2(f1(f2(x3221001,f2(x3221003,f2(x3221002,x3221004)))),f2(x3221003,x3221004)))))),
% 111.21/111.32 inference(scs_inference,[],[322089,321772,8])).
% 111.21/111.32 cnf(322121,plain,
% 111.21/111.32 (P2(f2(x3221211,f2(f1(f2(f1(f2(x3221212,f1(x3221212))),f2(x3221213,f2(x3221211,x3221214)))),f2(x3221213,x3221214))))),
% 111.21/111.32 inference(scs_inference,[],[322100,321944,8])).
% 111.21/111.32 cnf(322154,plain,
% 111.21/111.32 (P2(f2(f2(f1(f2(f1(f2(x3221541,f1(x3221541))),f2(x3221542,f2(x3221543,x3221544)))),f2(x3221542,x3221544)),x3221543))),
% 111.21/111.32 inference(scs_inference,[],[322121,317561,8])).
% 111.21/111.32 cnf(322218,plain,
% 111.21/111.32 (P2(f2(f1(f2(f1(f2(x3222181,f1(x3222181))),f2(x3222182,f2(x3222183,x3222184)))),f2(x3222183,f2(x3222182,x3222184))))),
% 111.21/111.32 inference(scs_inference,[],[322154,321849,8])).
% 111.21/111.32 cnf(322361,plain,
% 111.21/111.32 (P2(f2(x3223611,f2(f2(f1(f2(f2(f2(x3223612,x3223613),x3223614),x3223615)),f2(x3223615,x3223614)),f2(x3223612,x3223613))))),
% 111.21/111.32 inference(scs_inference,[],[317557,322026,8])).
% 111.21/111.32 cnf(322378,plain,
% 111.21/111.32 (P2(f2(f2(f2(f1(f2(f2(f2(x3223781,x3223782),x3223783),x3223784)),f2(x3223784,x3223783)),f2(x3223781,x3223782)),x3223785))),
% 111.21/111.32 inference(scs_inference,[],[317561,322361,8])).
% 111.21/111.32 cnf(322419,plain,
% 111.21/111.32 (P2(f2(f1(f2(x3224191,f2(x3224192,x3224192))),f2(x3224191,x3224192)))),
% 111.21/111.32 inference(scs_inference,[],[5,317563,7,8])).
% 111.21/111.32 cnf(322511,plain,
% 111.21/111.32 (P2(f2(f2(f1(f2(f2(f2(x3225111,x3225112),x3225113),x3225114)),f2(x3225114,x3225113)),f2(x3225115,f2(x3225111,x3225112))))),
% 111.21/111.32 inference(scs_inference,[],[321849,322378,8])).
% 111.21/111.32 cnf(322523,plain,
% 111.21/111.32 (P2(f2(f1(f2(f2(f2(x3225231,x3225232),x3225233),x3225234)),f2(f2(x3225235,f2(x3225231,x3225232)),f2(x3225234,x3225233))))),
% 111.21/111.32 inference(scs_inference,[],[321849,322511,8])).
% 111.21/111.32 cnf(322760,plain,
% 111.21/111.32 (P2(f2(f1(f2(f2(f2(x3227601,x3227602),x3227602),x3227601)),f2(x3227601,x3227602)))),
% 111.21/111.32 inference(scs_inference,[],[2,322511,7,8])).
% 111.21/111.32 cnf(322799,plain,
% 111.21/111.32 (~P2(f2(f2(f1(f2(f1(a3),a4)),f1(a3)),f2(f1(f1(a4)),f1(f1(a4)))))),
% 111.21/111.32 inference(scs_inference,[],[322096,322419,8])).
% 111.21/111.32 cnf(322815,plain,
% 111.21/111.32 (P2(f2(x3228151,f2(f1(f2(f1(f2(f1(x3228152),f2(x3228153,x3228152))),f2(x3228154,f2(x3228151,x3228155)))),f2(x3228154,x3228155))))),
% 111.21/111.32 inference(scs_inference,[],[322100,317557,8])).
% 111.21/111.32 cnf(322993,plain,
% 111.21/111.32 (P2(f2(f2(f1(f2(f2(f2(x3229931,x3229931),x3229932),x3229933)),f2(x3229933,x3229932)),x3229931))),
% 111.21/111.32 inference(scs_inference,[],[322419,322026,8])).
% 111.21/111.32 cnf(323005,plain,
% 111.21/111.32 (P2(f2(f2(f1(f2(f2(f2(f2(x3230051,x3230051),f2(x3230051,x3230051)),x3230052),x3230053)),f2(x3230053,x3230052)),x3230051))),
% 111.21/111.32 inference(scs_inference,[],[322419,322993,8])).
% 111.21/111.32 cnf(323043,plain,
% 111.21/111.32 (P2(f2(f1(f2(f2(f2(f2(x3230431,x3230431),f2(x3230431,x3230431)),x3230432),x3230433)),f2(x3230431,f2(x3230433,x3230432))))),
% 111.21/111.32 inference(scs_inference,[],[323005,321849,8])).
% 111.21/111.32 cnf(323171,plain,
% 111.21/111.32 (P2(f2(f1(f2(f1(f2(f1(x3231711),f2(x3231712,x3231711))),f2(x3231713,f2(x3231714,x3231715)))),f2(x3231714,f2(x3231713,x3231715))))),
% 111.21/111.32 inference(scs_inference,[],[322815,317565,8])).
% 111.21/111.32 cnf(323333,plain,
% 111.21/111.32 (P2(f2(f1(f2(f2(f2(x3233331,f2(x3233332,x3233333)),f2(x3233332,x3233333)),x3233331)),f2(x3233332,f2(x3233331,x3233333))))),
% 111.21/111.32 inference(scs_inference,[],[322760,321772,8])).
% 111.21/111.32 cnf(323625,plain,
% 111.21/111.32 (P2(f2(x3236251,f2(x3236252,f1(x3236252))))),
% 111.21/111.32 inference(scs_inference,[],[323171,322218,8])).
% 111.21/111.32 cnf(323638,plain,
% 111.21/111.32 (P2(f2(x3236381,f2(f2(x3236382,f1(x3236382)),x3236383)))),
% 111.21/111.32 inference(scs_inference,[],[323625,323333,8])).
% 111.21/111.32 cnf(323646,plain,
% 111.21/111.32 (P2(f2(f2(x3236461,f1(x3236461)),x3236462))),
% 111.21/111.32 inference(scs_inference,[],[323638,323625,8])).
% 111.21/111.32 cnf(323655,plain,
% 111.21/111.32 (P2(f2(x3236551,f2(f2(f2(x3236552,f1(x3236552)),x3236553),x3236554)))),
% 111.21/111.32 inference(scs_inference,[],[323638,323333,8])).
% 111.21/111.32 cnf(323664,plain,
% 111.21/111.32 (P2(f2(f2(f2(x3236641,f1(x3236641)),x3236642),x3236643))),
% 111.21/111.32 inference(scs_inference,[],[323646,323655,8])).
% 111.21/111.32 cnf(323763,plain,
% 111.21/111.32 (P2(f2(f2(x3237631,f2(x3237632,f1(x3237632))),f2(x3237633,x3237634)))),
% 111.21/111.32 inference(scs_inference,[],[323664,322523,8])).
% 111.21/111.32 cnf(323771,plain,
% 111.21/111.32 (P2(f2(x3237711,f2(f2(x3237712,x3237713),f2(x3237714,f1(x3237714)))))),
% 111.21/111.32 inference(scs_inference,[],[323763,323043,8])).
% 111.21/111.32 cnf(323782,plain,
% 111.21/111.32 (P2(f2(x3237821,f2(f2(x3237822,x3237823),f1(x3237821))))),
% 111.21/111.32 inference(scs_inference,[],[323771,323171,8])).
% 111.21/111.32 cnf(323792,plain,
% 111.21/111.32 (P2(f2(f2(x3237921,x3237922),f1(f1(f2(f2(x3237923,f2(x3237924,f1(x3237924))),f2(x3237925,x3237926))))))),
% 111.21/111.32 inference(scs_inference,[],[323782,323763,8])).
% 111.21/111.32 cnf(323878,plain,
% 111.21/111.32 (P2(f2(x3238781,f2(f2(x3238782,f2(x3238783,f1(x3238783))),x3238784)))),
% 111.21/111.32 inference(scs_inference,[],[4,323763,7,8])).
% 111.21/111.32 cnf(323888,plain,
% 111.21/111.32 (P2(f2(f2(x3238881,f2(x3238882,f1(x3238882))),x3238883))),
% 111.21/111.32 inference(scs_inference,[],[323878,323792,8])).
% 111.21/111.32 cnf(323900,plain,
% 111.21/111.32 (P2(f2(x3239001,f2(x3239002,f2(x3239003,f1(x3239003)))))),
% 111.21/111.32 inference(scs_inference,[],[323888,323043,8])).
% 111.21/111.32 cnf(323913,plain,
% 111.21/111.32 (P2(f2(x3239131,f2(x3239132,f1(x3239131))))),
% 111.21/111.32 inference(scs_inference,[],[323900,323171,8])).
% 111.21/111.32 cnf(323926,plain,
% 111.21/111.32 (P2(f2(f1(f2(x3239261,x3239262)),f2(x3239261,f2(x3239263,f1(f1(x3239262))))))),
% 111.21/111.32 inference(scs_inference,[],[323913,317567,8])).
% 111.21/111.32 cnf(323979,plain,
% 111.21/111.32 (~P2(f2(f2(f1(f2(f1(a3),a4)),f1(a3)),a4))),
% 111.21/111.32 inference(scs_inference,[],[322799,323926,8])).
% 111.21/111.32 cnf(323998,plain,
% 111.21/111.32 ($false),
% 111.21/111.32 inference(scs_inference,[],[323979,321874,317561,8]),
% 111.21/111.32 ['proof']).
% 111.32/111.43 % SZS output end Proof
% 111.32/111.43 % Total time :110.469859s
%------------------------------------------------------------------------------