%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : ALG171+1 : TPTP v9.3.1. Released v2.7.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 : n018.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:11:45 AM UTC 2026
% Result : Theorem 31.00s 31.58s
% Output : Proof 31.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 4
% Syntax : Number of formulae : 20 ( 9 unt; 0 def)
% Number of atoms : 237 ( 204 equ)
% Maximal formula atoms : 80 ( 11 avg)
% Number of connectives : 354 ( 137 ~; 41 |; 176 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 53 ( 9 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 6 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 3 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax5,axiom,
( e3 != e4
& e2 != e4
& e2 != e3
& e1 != e4
& e1 != e3
& e1 != e2
& e0 != e4
& e0 != e3
& e0 != e2
& e0 != e1 ),
file('theBenchmark.p',ax5) ).
fof(ax6,axiom,
( e3 = op(op(e4,op(e4,e4)),op(e4,op(e4,e4)))
& e2 = op(op(e4,op(e4,e4)),op(e4,e4))
& e1 = op(e4,e4)
& e0 = op(e4,op(e4,e4)) ),
file('theBenchmark.p',ax6) ).
fof(co1,conjecture,
~ ( op(e4,op(e4,e4)) = e4
& op(e4,op(e4,e3)) = e3
& op(e4,op(e4,e2)) = e2
& op(e4,op(e4,e1)) = e1
& op(e4,op(e4,e0)) = e0
& op(e3,op(e3,e4)) = e4
& op(e3,op(e3,e3)) = e3
& op(e3,op(e3,e2)) = e2
& op(e3,op(e3,e1)) = e1
& op(e3,op(e3,e0)) = e0
& op(e2,op(e2,e4)) = e4
& op(e2,op(e2,e3)) = e3
& op(e2,op(e2,e2)) = e2
& op(e2,op(e2,e1)) = e1
& op(e2,op(e2,e0)) = e0
& op(e1,op(e1,e4)) = e4
& op(e1,op(e1,e3)) = e3
& op(e1,op(e1,e2)) = e2
& op(e1,op(e1,e1)) = e1
& op(e1,op(e1,e0)) = e0
& op(e0,op(e0,e4)) = e4
& op(e0,op(e0,e3)) = e3
& op(e0,op(e0,e2)) = e2
& op(e0,op(e0,e1)) = e1
& op(e0,op(e0,e0)) = e0
& ( ( op(e4,e4) != e4
& op(e3,e4) != e3
& op(e2,e4) != e2
& op(e1,e4) != e1
& op(e0,e4) != e0 )
| ( op(e4,e3) != e4
& op(e3,e3) != e3
& op(e2,e3) != e2
& op(e1,e3) != e1
& op(e0,e3) != e0 )
| ( op(e4,e2) != e4
& op(e3,e2) != e3
& op(e2,e2) != e2
& op(e1,e2) != e1
& op(e0,e2) != e0 )
| ( op(e4,e1) != e4
& op(e3,e1) != e3
& op(e2,e1) != e2
& op(e1,e1) != e1
& op(e0,e1) != e0 )
| ( op(e4,e0) != e4
& op(e3,e0) != e3
& op(e2,e0) != e2
& op(e1,e0) != e1
& op(e0,e0) != e0 ) ) ),
file('theBenchmark.p',co1) ).
fof(f_5_1,plain,
( e3 != e4
& e2 != e4
& e2 != e3
& e1 != e4
& e1 != e3
& e1 != e2
& e0 != e4
& e0 != e3
& e0 != e2
& e0 != e1 ),
inference(fof_nnf,[status(thm)],[ax5]) ).
fof(f_5_2,plain,
( e3 != e4
& e2 != e4
& e2 != e3
& e1 != e4
& e1 != e3
& e1 != e2
& e0 != e4
& e0 != e3
& e0 != e2
& e0 != e1 ),
inference(definitional_conversion,[status(esa)],[f_5_1]) ).
cnf(f_5_6,plain,
e0 != e4,
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
( e3 = op(op(e4,op(e4,e4)),op(e4,op(e4,e4)))
& e2 = op(op(e4,op(e4,e4)),op(e4,e4))
& e1 = op(e4,e4)
& e0 = op(e4,op(e4,e4)) ),
inference(fof_nnf,[status(thm)],[ax6]) ).
fof(f_6_2,plain,
( e3 = op(op(e4,op(e4,e4)),op(e4,op(e4,e4)))
& e2 = op(op(e4,op(e4,e4)),op(e4,e4))
& e1 = op(e4,e4)
& e0 = op(e4,op(e4,e4)) ),
inference(definitional_conversion,[status(esa)],[f_6_1]) ).
cnf(f_6_3,plain,
e0 = op(e4,op(e4,e4)),
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_7_1,negated_conjecture,
( op(e4,op(e4,e4)) = e4
& op(e4,op(e4,e3)) = e3
& op(e4,op(e4,e2)) = e2
& op(e4,op(e4,e1)) = e1
& op(e4,op(e4,e0)) = e0
& op(e3,op(e3,e4)) = e4
& op(e3,op(e3,e3)) = e3
& op(e3,op(e3,e2)) = e2
& op(e3,op(e3,e1)) = e1
& op(e3,op(e3,e0)) = e0
& op(e2,op(e2,e4)) = e4
& op(e2,op(e2,e3)) = e3
& op(e2,op(e2,e2)) = e2
& op(e2,op(e2,e1)) = e1
& op(e2,op(e2,e0)) = e0
& op(e1,op(e1,e4)) = e4
& op(e1,op(e1,e3)) = e3
& op(e1,op(e1,e2)) = e2
& op(e1,op(e1,e1)) = e1
& op(e1,op(e1,e0)) = e0
& op(e0,op(e0,e4)) = e4
& op(e0,op(e0,e3)) = e3
& op(e0,op(e0,e2)) = e2
& op(e0,op(e0,e1)) = e1
& op(e0,op(e0,e0)) = e0
& ( ( op(e4,e4) != e4
& op(e3,e4) != e3
& op(e2,e4) != e2
& op(e1,e4) != e1
& op(e0,e4) != e0 )
| ( op(e4,e3) != e4
& op(e3,e3) != e3
& op(e2,e3) != e2
& op(e1,e3) != e1
& op(e0,e3) != e0 )
| ( op(e4,e2) != e4
& op(e3,e2) != e3
& op(e2,e2) != e2
& op(e1,e2) != e1
& op(e0,e2) != e0 )
| ( op(e4,e1) != e4
& op(e3,e1) != e3
& op(e2,e1) != e2
& op(e1,e1) != e1
& op(e0,e1) != e0 )
| ( op(e4,e0) != e4
& op(e3,e0) != e3
& op(e2,e0) != e2
& op(e1,e0) != e1
& op(e0,e0) != e0 ) ) ),
inference(negate,[status(cth)],[co1]) ).
fof(f_7_2,negated_conjecture,
( ( op(e4,e4) != e4
| ~ sP4 )
& ( op(e3,e4) != e3
| ~ sP4 )
& ( op(e2,e4) != e2
| ~ sP4 )
& ( op(e1,e4) != e1
| ~ sP4 )
& ( op(e0,e4) != e0
| ~ sP4 )
& ( op(e4,e3) != e4
| ~ sP3 )
& ( op(e3,e3) != e3
| ~ sP3 )
& ( op(e2,e3) != e2
| ~ sP3 )
& ( op(e1,e3) != e1
| ~ sP3 )
& ( op(e0,e3) != e0
| ~ sP3 )
& ( op(e4,e2) != e4
| ~ sP2 )
& ( op(e3,e2) != e3
| ~ sP2 )
& ( op(e2,e2) != e2
| ~ sP2 )
& ( op(e1,e2) != e1
| ~ sP2 )
& ( op(e0,e2) != e0
| ~ sP2 )
& ( op(e4,e1) != e4
| ~ sP1 )
& ( op(e3,e1) != e3
| ~ sP1 )
& ( op(e2,e1) != e2
| ~ sP1 )
& ( op(e1,e1) != e1
| ~ sP1 )
& ( op(e0,e1) != e0
| ~ sP1 )
& ( op(e4,e0) != e4
| ~ sP0 )
& ( op(e3,e0) != e3
| ~ sP0 )
& ( op(e2,e0) != e2
| ~ sP0 )
& ( op(e1,e0) != e1
| ~ sP0 )
& ( op(e0,e0) != e0
| ~ sP0 )
& op(e4,op(e4,e4)) = e4
& op(e4,op(e4,e3)) = e3
& op(e4,op(e4,e2)) = e2
& op(e4,op(e4,e1)) = e1
& op(e4,op(e4,e0)) = e0
& op(e3,op(e3,e4)) = e4
& op(e3,op(e3,e3)) = e3
& op(e3,op(e3,e2)) = e2
& op(e3,op(e3,e1)) = e1
& op(e3,op(e3,e0)) = e0
& op(e2,op(e2,e4)) = e4
& op(e2,op(e2,e3)) = e3
& op(e2,op(e2,e2)) = e2
& op(e2,op(e2,e1)) = e1
& op(e2,op(e2,e0)) = e0
& op(e1,op(e1,e4)) = e4
& op(e1,op(e1,e3)) = e3
& op(e1,op(e1,e2)) = e2
& op(e1,op(e1,e1)) = e1
& op(e1,op(e1,e0)) = e0
& op(e0,op(e0,e4)) = e4
& op(e0,op(e0,e3)) = e3
& op(e0,op(e0,e2)) = e2
& op(e0,op(e0,e1)) = e1
& op(e0,op(e0,e0)) = e0
& ( sP4
| sP3
| sP2
| sP1
| sP0 ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1,sP2,sP3,sP4])],[f_7_1]) ).
cnf(f_7_28,negated_conjecture,
op(e4,op(e4,e4)) = e4,
inference(clausify,[status(thm)],[f_7_2]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(t1,plain,
op(e4,op(e4,e4)) = e4,
inference(start,[status(thm),parent(0:0)],[f_7_28]) ).
cnf(t2,plain,
( e0 = e4
| e0 != op(e4,op(e4,e4))
| op(e4,op(e4,e4)) != e4 ),
inference(extension,[status(thm),parent(t1:1)],[equality_3]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
e0 = op(e4,op(e4,e4)),
inference(extension,[status(thm),parent(t2:2)],[f_6_3]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
e0 != e4,
inference(extension,[status(thm),parent(t2:3)],[f_5_6]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t2:3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG171+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 This is a FOF_THM_EPR_PEQ problem
% 0.00/0.06 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.66 % Computer : n018.cluster.edu
% 0.15/0.66 % Model : x86_64 x86_64
% 0.15/0.66 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.66 % Memory : 8046.5625MB
% 0.15/0.66 % OS : Linux 6.8.0-71-generic
% 0.15/0.66 % CPULimit : 300
% 0.15/0.66 % WCLimit : 300
% 0.15/0.66 % DateTime : Sun Sep 20 09:31:58 UTC 2026
% 0.15/0.67 % CPUTime :
% 31.00/31.58 % SZS status Theorem for theBenchmark
% 31.00/31.58 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------