%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : LCL525+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 : Thu Sep 24 08:49:27 AM UTC 2026
% Result : Theorem 0.96s 1.20s
% Output : Proof 0.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 9
% Syntax : Number of formulae : 65 ( 33 unt; 0 def)
% Number of atoms : 163 ( 7 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 161 ( 63 ~; 63 |; 29 &)
% ( 3 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 5 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 49 ( 0 sgn 30 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(modus_ponens,axiom,
( modus_ponens
<=> ! [X,Y] :
( ( is_a_theorem(implies(X,Y))
& is_a_theorem(X) )
=> is_a_theorem(Y) ) ),
file('LCL006+0.ax',modus_ponens) ).
fof(hilbert_modus_ponens,axiom,
modus_ponens,
file('LCL006+2.ax',hilbert_modus_ponens) ).
fof(modus_ponens_strict_implies,axiom,
( modus_ponens_strict_implies
<=> ! [X,Y] :
( ( is_a_theorem(strict_implies(X,Y))
& is_a_theorem(X) )
=> is_a_theorem(Y) ) ),
file('LCL007+0.ax',modus_ponens_strict_implies) ).
fof(axiom_M,axiom,
( axiom_M
<=> ! [X] : is_a_theorem(implies(necessarily(X),X)) ),
file('LCL007+0.ax',axiom_M) ).
fof(op_strict_implies,axiom,
( op_strict_implies
=> ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y)) ),
file('LCL007+1.ax',op_strict_implies) ).
fof(km5_axiom_M,axiom,
axiom_M,
file('LCL007+2.ax',km5_axiom_M) ).
fof(s1_0_op_strict_implies,axiom,
op_strict_implies,
file('theBenchmark.p',s1_0_op_strict_implies) ).
fof(s1_0_modus_ponens_strict_implies,conjecture,
modus_ponens_strict_implies,
file('theBenchmark.p',s1_0_modus_ponens_strict_implies) ).
fof(f_1_1,plain,
( ( modus_ponens
| ? [X,Y] :
( ~ is_a_theorem(Y)
& is_a_theorem(implies(X,Y))
& is_a_theorem(X) ) )
& ( ! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) )
| ~ modus_ponens ) ),
inference(fof_nnf,[status(thm)],[modus_ponens]) ).
fof(f_1_2,plain,
( ( modus_ponens
| ? [U_3,U_2] :
( ~ is_a_theorem(U_2)
& is_a_theorem(implies(U_3,U_2))
& is_a_theorem(U_3) ) )
& ( ! [U_1,U_0] :
( is_a_theorem(U_0)
| ~ is_a_theorem(implies(U_1,U_0))
| ~ is_a_theorem(U_1) )
| ~ modus_ponens ) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
( ( modus_ponens
| ? [U_2] :
( ~ is_a_theorem(U_2)
& is_a_theorem(implies(sK1,U_2))
& is_a_theorem(sK1) ) )
& ( ! [U_1,U_0] :
( is_a_theorem(U_0)
| ~ is_a_theorem(implies(U_1,U_0))
| ~ is_a_theorem(U_1) )
| ~ modus_ponens ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_3,sK1)],[f_1_2]) ).
fof(f_1_4,plain,
( ( modus_ponens
| ( ~ is_a_theorem(sK2)
& is_a_theorem(implies(sK1,sK2))
& is_a_theorem(sK1) ) )
& ( ! [U_1,U_0] :
( is_a_theorem(U_0)
| ~ is_a_theorem(implies(U_1,U_0))
| ~ is_a_theorem(U_1) )
| ~ modus_ponens ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_2,sK2)],[f_1_3]) ).
cnf(f_1_5,plain,
( is_a_theorem(U_0)
| ~ is_a_theorem(implies(U_1,U_0))
| ~ is_a_theorem(U_1)
| ~ modus_ponens ),
inference(clausify,[status(thm)],[f_1_4]) ).
fof(f_35_1,plain,
modus_ponens,
inference(fof_nnf,[status(thm)],[hilbert_modus_ponens]) ).
cnf(f_35_2,plain,
modus_ponens,
inference(clausify,[status(thm)],[f_35_1]) ).
fof(f_51_1,plain,
( ( modus_ponens_strict_implies
| ? [X,Y] :
( ~ is_a_theorem(Y)
& is_a_theorem(strict_implies(X,Y))
& is_a_theorem(X) ) )
& ( ! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(strict_implies(X,Y))
| ~ is_a_theorem(X) )
| ~ modus_ponens_strict_implies ) ),
inference(fof_nnf,[status(thm)],[modus_ponens_strict_implies]) ).
fof(f_51_2,plain,
( ( modus_ponens_strict_implies
| ? [U_125,U_124] :
( ~ is_a_theorem(U_124)
& is_a_theorem(strict_implies(U_125,U_124))
& is_a_theorem(U_125) ) )
& ( ! [U_123,U_122] :
( is_a_theorem(U_122)
| ~ is_a_theorem(strict_implies(U_123,U_122))
| ~ is_a_theorem(U_123) )
| ~ modus_ponens_strict_implies ) ),
inference(variable_rename,[status(thm)],[f_51_1]) ).
fof(f_51_3,plain,
( ( modus_ponens_strict_implies
| ? [U_124] :
( ~ is_a_theorem(U_124)
& is_a_theorem(strict_implies(sK57,U_124))
& is_a_theorem(sK57) ) )
& ( ! [U_123,U_122] :
( is_a_theorem(U_122)
| ~ is_a_theorem(strict_implies(U_123,U_122))
| ~ is_a_theorem(U_123) )
| ~ modus_ponens_strict_implies ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57]),skolemize(U_125,sK57)],[f_51_2]) ).
fof(f_51_4,plain,
( ( modus_ponens_strict_implies
| ( ~ is_a_theorem(sK58)
& is_a_theorem(strict_implies(sK57,sK58))
& is_a_theorem(sK57) ) )
& ( ! [U_123,U_122] :
( is_a_theorem(U_122)
| ~ is_a_theorem(strict_implies(U_123,U_122))
| ~ is_a_theorem(U_123) )
| ~ modus_ponens_strict_implies ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58]),skolemize(U_124,sK58)],[f_51_3]) ).
cnf(f_51_6,plain,
( is_a_theorem(sK57)
| modus_ponens_strict_implies ),
inference(clausify,[status(thm)],[f_51_4]) ).
cnf(f_51_7,plain,
( is_a_theorem(strict_implies(sK57,sK58))
| modus_ponens_strict_implies ),
inference(clausify,[status(thm)],[f_51_4]) ).
cnf(f_51_8,plain,
( ~ is_a_theorem(sK58)
| modus_ponens_strict_implies ),
inference(clausify,[status(thm)],[f_51_4]) ).
fof(f_55_1,plain,
( ( axiom_M
| ? [X] : ~ is_a_theorem(implies(necessarily(X),X)) )
& ( ! [X] : is_a_theorem(implies(necessarily(X),X))
| ~ axiom_M ) ),
inference(fof_nnf,[status(thm)],[axiom_M]) ).
fof(f_55_2,plain,
( ( axiom_M
| ? [U_139] : ~ is_a_theorem(implies(necessarily(U_139),U_139)) )
& ( ! [U_138] : is_a_theorem(implies(necessarily(U_138),U_138))
| ~ axiom_M ) ),
inference(variable_rename,[status(thm)],[f_55_1]) ).
fof(f_55_3,plain,
( ( axiom_M
| ~ is_a_theorem(implies(necessarily(sK65),sK65)) )
& ( ! [U_138] : is_a_theorem(implies(necessarily(U_138),U_138))
| ~ axiom_M ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK65]),skolemize(U_139,sK65)],[f_55_2]) ).
cnf(f_55_4,plain,
( is_a_theorem(implies(necessarily(U_138),U_138))
| ~ axiom_M ),
inference(clausify,[status(thm)],[f_55_3]) ).
fof(f_75_1,plain,
( ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y))
| ~ op_strict_implies ),
inference(fof_nnf,[status(thm)],[op_strict_implies]) ).
fof(f_75_2,plain,
( ! [U_201,U_200] : strict_implies(U_201,U_200) = necessarily(implies(U_201,U_200))
| ~ op_strict_implies ),
inference(variable_rename,[status(thm)],[f_75_1]) ).
cnf(f_75_3,plain,
( strict_implies(U_201,U_200) = necessarily(implies(U_201,U_200))
| ~ op_strict_implies ),
inference(clausify,[status(thm)],[f_75_2]) ).
fof(f_80_1,plain,
axiom_M,
inference(fof_nnf,[status(thm)],[km5_axiom_M]) ).
cnf(f_80_2,plain,
axiom_M,
inference(clausify,[status(thm)],[f_80_1]) ).
fof(f_85_1,plain,
op_strict_implies,
inference(fof_nnf,[status(thm)],[s1_0_op_strict_implies]) ).
cnf(f_85_2,plain,
op_strict_implies,
inference(clausify,[status(thm)],[f_85_1]) ).
fof(f_88_1,negated_conjecture,
~ modus_ponens_strict_implies,
inference(negate,[status(cth)],[s1_0_modus_ponens_strict_implies]) ).
fof(f_88_2,negated_conjecture,
~ modus_ponens_strict_implies,
inference(definitional_conversion,[status(esa)],[f_88_1]) ).
cnf(f_88_3,negated_conjecture,
~ modus_ponens_strict_implies,
inference(clausify,[status(thm)],[f_88_2]) ).
cnf(equality_13,axiom,
( is_a_theorem(Eq_y_0)
| ~ is_a_theorem(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(t1,plain,
~ modus_ponens_strict_implies,
inference(start,[status(thm),parent(0:0)],[f_88_3]) ).
cnf(t2,plain,
( is_a_theorem(strict_implies(sK57,sK58))
| modus_ponens_strict_implies ),
inference(extension,[status(thm),parent(t1:1)],[f_51_7]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( is_a_theorem(necessarily(implies(sK57,sK58)))
| strict_implies(sK57,sK58) != necessarily(implies(sK57,sK58))
| ~ is_a_theorem(strict_implies(sK57,sK58)) ),
inference(extension,[status(thm),parent(t2:2)],[equality_13]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ op_strict_implies
| strict_implies(sK57,sK58) = necessarily(implies(sK57,sK58)) ),
inference(extension,[status(thm),parent(t4:2)],[f_75_3]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
op_strict_implies,
inference(extension,[status(thm),parent(t6:2)],[f_85_2]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
( is_a_theorem(implies(sK57,sK58))
| ~ is_a_theorem(implies(necessarily(implies(sK57,sK58)),implies(sK57,sK58)))
| ~ modus_ponens
| ~ is_a_theorem(necessarily(implies(sK57,sK58))) ),
inference(extension,[status(thm),parent(t4:3)],[f_1_5]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t4:3]) ).
cnf(t12,plain,
modus_ponens,
inference(extension,[status(thm),parent(t10:2)],[f_35_2]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
cnf(l6,lemma,
modus_ponens,
inference(lemma,[status(cth),parent(t10:2),below(t4:3)],[t10:2]) ).
cnf(t14,plain,
( ~ axiom_M
| is_a_theorem(implies(necessarily(implies(sK57,sK58)),implies(sK57,sK58))) ),
inference(extension,[status(thm),parent(t10:3)],[f_55_4]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t10:3]) ).
cnf(t16,plain,
axiom_M,
inference(extension,[status(thm),parent(t14:2)],[f_80_2]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
cnf(t18,plain,
( ~ is_a_theorem(sK57)
| is_a_theorem(sK58)
| ~ modus_ponens
| ~ is_a_theorem(implies(sK57,sK58)) ),
inference(extension,[status(thm),parent(t10:4)],[f_1_5]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t10:4]) ).
cnf(t20,plain,
modus_ponens,
inference(lemma_extension,[status(thm),parent(t18:2)],[l6:1]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t18:2]) ).
cnf(t22,plain,
( modus_ponens_strict_implies
| ~ is_a_theorem(sK58) ),
inference(extension,[status(thm),parent(t18:3)],[f_51_8]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t18:3]) ).
cnf(t24,plain,
$false,
inference(reduction,[status(thm),parent(t22:2)],[t22:2,t1:1]) ).
cnf(t25,plain,
( modus_ponens_strict_implies
| is_a_theorem(sK57) ),
inference(extension,[status(thm),parent(t18:4)],[f_51_6]) ).
cnf(t26,plain,
$false,
inference(connection,[status(thm),parent(t25:1)],[t25:1,t18:4]) ).
cnf(t27,plain,
$false,
inference(reduction,[status(thm),parent(t25:2)],[t25:2,t1:1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL525+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n011.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 19 15:11:39 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.96/1.20 % SZS status Theorem for theBenchmark
% 0.96/1.20 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------