%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL672+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n028.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:19:35 AM UTC 2026
% Result : Theorem 59.69s 59.89s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL672+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.07/0.35 % Computer : n028.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sat Sep 5 14:36:59 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.25/0.52 start to proof:theBenchmark
% 59.69/59.88 %-------------------------------------------
% 59.69/59.88 % File :CSE---1.7
% 59.69/59.88 % Problem :theBenchmark
% 59.69/59.88 % Transform :cnf
% 59.69/59.88 % Format :tptp:raw
% 59.69/59.88 % Command :java -jar mcs_scs.jar %d %s
% 59.69/59.88
% 59.69/59.88 % Result :Theorem 59.358894s
% 59.69/59.88 % Output :CNFRefutation 59.358894s
% 59.69/59.88 %-------------------------------------------
% 59.69/59.88 %------------------------------------------------------------------------------
% 59.69/59.88 % File : LCL672+1.001 : TPTP v9.3.1. Released v4.0.0.
% 59.69/59.88 % Domain : Logic Calculi (Modal Logic)
% 59.69/59.88 % Problem : In S4, A5{box p0/p0} & box A5{~p0/p0} -> A5, size 1
% 59.69/59.88 % Version : Especial.
% 59.69/59.88 % English :
% 59.69/59.88
% 59.69/59.88 % Refs : [BHS00] Balsiger et al. (2000), A Benchmark Method for the Pro
% 59.69/59.88 % : [Kam08] Kaminski (2008), Email to G. Sutcliffe
% 59.69/59.88 % Source : [Kam08]
% 59.69/59.88 % Names : s4_45_p [BHS00]
% 59.69/59.88
% 59.69/59.88 % Status : Theorem
% 59.69/59.88 % Rating : 0.00 v9.1.0, 0.07 v9.0.0, 0.00 v6.1.0, 0.12 v6.0.0, 0.25 v5.4.0, 0.26 v5.3.0, 0.30 v5.2.0, 0.14 v5.0.0, 0.15 v4.1.0, 0.17 v4.0.1, 0.21 v4.0.0
% 59.69/59.88 % Syntax : Number of formulae : 3 ( 1 unt; 0 def)
% 59.69/59.88 % Number of atoms : 53 ( 0 equ)
% 59.69/59.88 % Maximal formula atoms : 49 ( 17 avg)
% 59.69/59.88 % Number of connectives : 110 ( 60 ~; 37 |; 12 &)
% 59.69/59.88 % ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% 59.69/59.88 % Maximal formula depth : 24 ( 11 avg)
% 59.69/59.88 % Maximal term depth : 1 ( 1 avg)
% 59.69/59.88 % Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% 59.69/59.88 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 59.69/59.88 % Number of variables : 35 ( 34 !; 1 ?)
% 59.69/59.88 % SPC : FOF_THM_RFO_NEQ
% 59.69/59.88
% 59.69/59.88 % Comments : A naive relational encoding of the modal logic problem into
% 59.69/59.88 % first-order logic.
% 59.69/59.88 %------------------------------------------------------------------------------
% 59.69/59.88 fof(reflexivity,axiom,
% 59.69/59.88 ! [X] : r1(X,X) ).
% 59.69/59.88
% 59.69/59.88 fof(transitivity,axiom,
% 59.69/59.88 ! [X,Y,Z] :
% 59.69/59.88 ( ( r1(X,Y)
% 59.69/59.88 & r1(Y,Z) )
% 59.69/59.88 => r1(X,Z) ) ).
% 59.69/59.88
% 59.69/59.88 fof(main,conjecture,
% 59.69/59.88 ~ ? [X] :
% 59.69/59.88 ~ ( ( ~ ! [Y] :
% 59.69/59.88 ( ~ r1(X,Y)
% 59.69/59.88 | p2(Y) )
% 59.69/59.88 & ~ ! [Y] :
% 59.69/59.88 ( ~ r1(X,Y)
% 59.69/59.88 | ~ ( ~ ! [X] :
% 59.69/59.88 ( ~ r1(Y,X)
% 59.69/59.88 | ~ ! [Y] :
% 59.69/59.88 ( ~ r1(X,Y)
% 59.69/59.88 | ~ p1(Y) ) )
% 59.69/59.88 & p1(Y) ) )
% 59.69/59.88 & ~ ! [Y] :
% 59.69/59.88 ( ~ r1(X,Y)
% 59.69/59.88 | p1(Y) ) )
% 59.69/59.88 | ( ~ ! [Y] :
% 59.69/59.88 ( ~ r1(X,Y)
% 59.69/59.88 | p2(Y) )
% 59.69/59.88 & ~ ! [Y] :
% 59.69/59.88 ( ~ r1(X,Y)
% 59.69/59.88 | ! [X] :
% 59.69/59.88 ( ~ r1(Y,X)
% 59.69/59.89 | ~ ( ~ ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | ~ ! [X] :
% 59.69/59.89 ( ~ r1(Y,X)
% 59.69/59.89 | p1(X) ) )
% 59.69/59.89 & ~ ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | p1(Y) ) ) ) )
% 59.69/59.89 & ~ ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | p1(Y) ) )
% 59.69/59.89 | ( ~ ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | p2(Y) )
% 59.69/59.89 & ~ ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | ~ ( ~ ! [X] :
% 59.69/59.89 ( ~ r1(Y,X)
% 59.69/59.89 | ~ ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | ~ ! [X] :
% 59.69/59.89 ( ~ r1(Y,X)
% 59.69/59.89 | p1(X) ) ) )
% 59.69/59.89 & ~ ! [X] :
% 59.69/59.89 ( ~ r1(Y,X)
% 59.69/59.89 | ~ ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | p1(Y) ) ) ) )
% 59.69/59.89 & ~ ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | p1(Y) ) )
% 59.69/59.89 | ( ~ ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | p2(Y) )
% 59.69/59.89 & ~ ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | ~ ! [X] :
% 59.69/59.89 ( ~ r1(Y,X)
% 59.69/59.89 | $false ) )
% 59.69/59.89 & ~ ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | p1(Y) ) )
% 59.69/59.89 | ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | p2(Y) )
% 59.69/59.89 | ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | ! [X] :
% 59.69/59.89 ( ~ r1(Y,X)
% 59.69/59.89 | ~ ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | p1(Y) ) )
% 59.69/59.89 | ! [X] :
% 59.69/59.89 ( ~ r1(Y,X)
% 59.69/59.89 | p1(X) ) )
% 59.69/59.89 | ! [Y] :
% 59.69/59.89 ( ~ r1(X,Y)
% 59.69/59.89 | p1(Y) ) ) ).
% 59.69/59.89
% 59.69/59.89 %------------------------------------------------------------------------------
% 59.69/59.89 %-------------------------------------------
% 59.69/59.89 % Proof found
% 59.69/59.89 % SZS status Theorem for theBenchmark
% 59.69/59.89 % SZS output start Proof
% 59.69/59.89 %ClaNum:20(EqnAxiom:0)
% 59.69/59.89 %VarNum:129(SingletonVarNum:50)
% 59.69/59.89 %MaxLitNum:10
% 59.69/59.89 %MaxfuncDepth:1
% 59.69/59.89 %SharedTerms:14
% 59.69/59.89 %goalClause: 1 2 3 4 5 7 8 9 10 12 13 14 15 16 17 18 19 20
% 59.69/59.89 %singleGoalClaCount:8
% 59.69/59.89 [1]P1(a1,a4)
% 59.69/59.89 [2]P1(a1,a10)
% 59.69/59.89 [3]P1(a1,a2)
% 59.69/59.89 [4]P1(a10,a11)
% 59.69/59.89 [5]P1(a10,a3)
% 59.69/59.89 [7]~P2(a4)
% 59.69/59.89 [8]~P3(a3)
% 59.69/59.89 [9]~P3(a2)
% 59.69/59.89 [6]P1(x61,x61)
% 59.69/59.89 [10]P3(x101)+~P1(a11,x101)
% 59.69/59.89 [11]~P1(x111,x113)+P1(x111,x112)+~P1(x113,x112)
% 59.69/59.89 [12]P2(x121)+P3(x122)+~P1(a1,x122)+~P1(a1,x123)+~P1(a1,x121)+P1(x123,f5(x123))
% 59.69/59.89 [13]~P3(x133)+~P1(x133,x134)+P2(x131)+P3(x132)+~P1(a1,x132)+~P1(a1,x131)+~P1(a1,x133)+P3(f6(x133,x134))
% 59.69/59.89 [14]~P3(x144)+~P1(x144,x143)+P2(x141)+P3(x142)+~P1(a1,x142)+~P1(a1,x141)+~P1(a1,x144)+P1(x143,f6(x144,x143))
% 59.69/59.89 [15]~P1(x154,x153)+~P1(x154,x155)+P2(x151)+P3(x152)+~P1(a1,x152)+~P1(a1,x151)+~P1(a1,x154)+P1(x153,f7(x154,x153))+P1(x155,f9(x154,x155))
% 59.69/59.89 [16]~P1(x164,x163)+P2(x161)+P3(x162)+~P1(x164,x165)+~P1(a1,x162)+~P1(a1,x161)+~P1(a1,x164)+P1(x163,f7(x164,x163))+~P3(f9(x164,x165))
% 59.69/59.89 [17]~P1(x175,x174)+P2(x171)+P3(x172)+P3(x173)+~P1(x175,x176)+~P1(a1,x172)+~P1(a1,x171)+~P1(a1,x175)+~P1(f7(x175,x176),x173)+P1(x174,f9(x175,x174))
% 59.69/59.89 [18]P2(x181)+P3(x182)+~P1(x184,x185)+P3(x183)+~P1(x184,x186)+~P1(a1,x182)+~P1(a1,x181)+~P1(a1,x184)+~P1(f7(x184,x185),x183)+~P3(f9(x184,x186))
% 59.69/59.89 [19]~P1(x196,x193)+~P1(x196,x194)+~P1(x195,x196)+P2(x191)+P3(x192)+P3(x193)+~P1(a1,x192)+~P1(a1,x191)+~P1(a1,x195)+P1(x194,f8(x195,x196,x194))
% 59.69/59.89 [20]P2(x201)+P3(x202)+~P1(x204,x203)+~P1(x204,x205)+P3(x203)+~P1(x206,x204)+~P1(a1,x202)+~P1(a1,x201)+~P1(a1,x206)+~P3(f8(x206,x204,x205))
% 59.69/59.89 %EqnAxiom
% 59.69/59.89
% 59.69/59.89 %-------------------------------------------
% 59.80/59.99 cnf(21,plain,
% 59.80/59.99 (P3(a11)),
% 59.80/59.99 inference(scs_inference,[],[6,10])).
% 59.80/59.99 cnf(24,plain,
% 59.80/59.99 (P1(a1,a11)),
% 59.80/59.99 inference(scs_inference,[],[2,4,6,10,11])).
% 59.80/59.99 cnf(35,plain,
% 59.80/59.99 (P1(a1,a3)),
% 59.80/59.99 inference(scs_inference,[],[5,2,11])).
% 59.80/59.99 cnf(1249,plain,
% 59.80/59.99 (~P1(a11,a10)),
% 59.80/59.99 inference(scs_inference,[],[8,5,10,11])).
% 59.80/59.99 cnf(1250,plain,
% 59.80/59.99 (~P1(a11,a1)),
% 59.80/59.99 inference(scs_inference,[],[2,1249,11])).
% 59.80/59.99 cnf(110284,plain,
% 59.80/59.99 (~P1(a11,a3)),
% 59.80/59.99 inference(scs_inference,[],[8,10])).
% 59.80/59.99 cnf(110287,plain,
% 59.80/59.99 (~P1(a1,x1102871)+~P1(a1,x1102872)+P2(x1102871)+P3(x1102873)+P1(x1102872,f5(x1102872))+~P1(a1,x1102873)),
% 59.80/59.99 inference(rename_variables,[],[12])).
% 59.80/59.99 cnf(110290,plain,
% 59.80/59.99 (P1(a11,f6(a11,a11))),
% 59.80/59.99 inference(scs_inference,[],[2,21,7,6,1,35,8,24,10,12,110287,14])).
% 59.80/59.99 cnf(110291,plain,
% 59.80/59.99 (P1(x1102911,x1102911)),
% 59.80/59.99 inference(rename_variables,[],[6])).
% 59.80/59.99 cnf(110293,plain,
% 59.80/59.99 (P1(a3,f8(a10,a3,a3))),
% 59.80/59.99 inference(scs_inference,[],[2,21,7,6,110291,1,35,8,5,24,10,12,110287,14,19])).
% 59.80/59.99 cnf(110308,plain,
% 59.80/59.99 (~P3(f8(a1,a1,a1))),
% 59.80/59.99 inference(scs_inference,[],[2,110284,110290,7,6,1,35,8,9,10,11,12,20])).
% 59.80/59.99 cnf(110309,plain,
% 59.80/59.99 (P1(x1103091,x1103091)),
% 59.80/59.99 inference(rename_variables,[],[6])).
% 59.80/59.99 cnf(110311,plain,
% 59.80/59.99 (P1(a2,f8(a2,a2,a2))),
% 59.80/59.99 inference(scs_inference,[],[2,110284,110290,7,6,110309,3,1,35,8,9,10,11,12,20,19])).
% 59.80/59.99 cnf(110371,plain,
% 59.80/59.99 (P1(a1,f8(a2,a2,a2))),
% 59.80/59.99 inference(scs_inference,[],[110311,3,11])).
% 59.80/59.99 cnf(110424,plain,
% 59.80/59.99 (P1(a1,f8(a1,a1,a1))),
% 59.80/59.99 inference(scs_inference,[],[110293,9,7,6,3,1,5,11,19])).
% 59.80/59.99 cnf(110483,plain,
% 59.80/59.99 (P1(a11,f8(a1,a1,a11))),
% 59.80/59.99 inference(scs_inference,[],[110424,110308,7,6,1,24,19])).
% 59.80/59.99 cnf(110538,plain,
% 59.80/59.99 (~P3(f8(a10,a10,a3))),
% 59.80/59.99 inference(scs_inference,[],[5,110424,110483,110308,1250,7,6,35,1,8,24,2,11,12,20])).
% 59.80/59.99 cnf(110691,plain,
% 59.80/59.99 (~P3(f8(a2,a2,a2))),
% 59.80/59.99 inference(scs_inference,[],[6,9,7,3,1,20])).
% 59.80/59.99 cnf(110724,plain,
% 59.80/59.99 (P1(a3,f8(a10,a10,a3))),
% 59.80/59.99 inference(scs_inference,[],[6,110691,110371,7,1,5,8,2,19])).
% 59.80/59.99 cnf(110816,plain,
% 59.80/59.99 (P1(a1,f8(a10,a10,a3))),
% 59.80/59.99 inference(scs_inference,[],[110724,35,11])).
% 59.80/59.99 cnf(110832,plain,
% 59.80/59.99 ($false),
% 59.80/59.99 inference(scs_inference,[],[24,110816,110538,110483,7,6,1,20,10]),
% 59.80/59.99 ['proof']).
% 59.80/60.02 % SZS output end Proof
% 59.80/60.02 % Total time :59.358894s
%------------------------------------------------------------------------------