%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG014+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 : Sun Sep 27 06:49:07 AM UTC 2026
% Result : Theorem 0.40s 0.72s
% Output : CNFRefutation 0.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 5
% Syntax : Number of formulae : 55 ( 17 unt; 0 def)
% Number of atoms : 235 ( 234 equ)
% Maximal formula atoms : 32 ( 4 avg)
% Number of connectives : 218 ( 38 ~; 116 |; 64 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax4,axiom,
( ( inv(e3) = e3
| inv(e3) = e2
| inv(e3) = e1
| inv(e3) = e0 )
& ( inv(e2) = e3
| inv(e2) = e2
| inv(e2) = e1
| inv(e2) = e0 )
& ( inv(e1) = e3
| inv(e1) = e2
| inv(e1) = e1
| inv(e1) = e0 )
& ( inv(e0) = e3
| inv(e0) = e2
| inv(e0) = e1
| inv(e0) = e0 )
& op(inv(e3),e3) = unit
& op(e3,inv(e3)) = unit
& op(inv(e2),e2) = unit
& op(e2,inv(e2)) = unit
& op(inv(e1),e1) = unit
& op(e1,inv(e1)) = unit
& op(inv(e0),e0) = unit
& op(e0,inv(e0)) = unit ),
file('theBenchmark.p',ax4) ).
fof(ax11,axiom,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
file('theBenchmark.p',ax11) ).
fof(co1,conjecture,
( ~ ( ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) )
| ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ( ~ ( ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) )
| ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_101,plain,
op(inv(e0),e0) = unit,
inference(clausify,[status(thm)],[ax4]) ).
fof(ax5,axiom,
unit = e0,
file('theBenchmark.p',ax5) ).
cnf(c_112,plain,
unit = e0,
inference(clausify,[status(thm)],[ax5]) ).
fof(ax6,axiom,
inv(unit) = unit,
file('theBenchmark.p',ax6) ).
cnf(c_113,plain,
inv(unit) = unit,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_512,plain,
inv(e0) = unit,
inference(paramod,[status(thm)],[c_112,c_113]) ).
cnf(c_114,plain,
inv(e0) = e0,
inference(paramod,[status(thm)],[c_112,c_512]) ).
cnf(c_194,plain,
e1 != e0,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_195,plain,
e2 != e0,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_196,plain,
e3 != e0,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_200,negated_conjecture,
( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0
| op(e0,e0) != e0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_326,negated_conjecture,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_389,negated_conjecture,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_393,negated_conjecture,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_513,plain,
op(e0,e0) = unit,
inference(paramod,[status(thm)],[c_114,c_101]) ).
cnf(c_462,plain,
op(e0,e0) = e0,
inference(paramod,[status(thm)],[c_112,c_513]) ).
cnf(c_514,negated_conjecture,
( op(e0,e0) = e3
| op(e0,e0) = e2
| e0 = e1
| op(e3,e3) = e0 ),
inference(paramod,[status(thm)],[c_462,c_393]) ).
cnf(c_515,negated_conjecture,
( op(e0,e0) = e3
| e0 = e2
| e0 = e1
| op(e3,e3) = e0 ),
inference(paramod,[status(thm)],[c_462,c_514]) ).
cnf(c_516,negated_conjecture,
( e0 = e3
| e0 = e2
| e0 = e1
| op(e3,e3) = e0 ),
inference(paramod,[status(thm)],[c_462,c_515]) ).
cnf(c_517,negated_conjecture,
( e0 = e3
| e0 = e2
| e1 = e0
| op(e3,e3) = e0 ),
inference(copy,[status(thm)],[c_516]) ).
cnf(c_518,negated_conjecture,
( e0 = e3
| e2 = e0
| e1 = e0
| op(e3,e3) = e0 ),
inference(copy,[status(thm)],[c_517]) ).
cnf(c_519,negated_conjecture,
( e3 = e0
| e2 = e0
| e1 = e0
| op(e3,e3) = e0 ),
inference(copy,[status(thm)],[c_518]) ).
cnf(c_520,negated_conjecture,
( e3 = e0
| e2 = e0
| op(e3,e3) = e0 ),
inference(resolve,[status(thm)],[c_194,c_519]) ).
cnf(c_521,negated_conjecture,
( e3 = e0
| op(e3,e3) = e0 ),
inference(resolve,[status(thm)],[c_195,c_520]) ).
cnf(c_508,negated_conjecture,
op(e3,e3) = e0,
inference(resolve,[status(thm)],[c_196,c_521]) ).
cnf(c_522,negated_conjecture,
( op(e0,e0) = e3
| op(e3,e3) = e2
| e0 = e1
| op(e2,e2) = e0 ),
inference(paramod,[status(thm)],[c_508,c_389]) ).
cnf(c_523,negated_conjecture,
( op(e0,e0) = e3
| e0 = e2
| e0 = e1
| op(e2,e2) = e0 ),
inference(paramod,[status(thm)],[c_508,c_522]) ).
cnf(c_524,negated_conjecture,
( e0 = e3
| e0 = e2
| e0 = e1
| op(e2,e2) = e0 ),
inference(paramod,[status(thm)],[c_462,c_523]) ).
cnf(c_525,negated_conjecture,
( e0 = e3
| e0 = e2
| e1 = e0
| op(e2,e2) = e0 ),
inference(copy,[status(thm)],[c_524]) ).
cnf(c_526,negated_conjecture,
( e0 = e3
| e2 = e0
| e1 = e0
| op(e2,e2) = e0 ),
inference(copy,[status(thm)],[c_525]) ).
cnf(c_527,negated_conjecture,
( e3 = e0
| e2 = e0
| e1 = e0
| op(e2,e2) = e0 ),
inference(copy,[status(thm)],[c_526]) ).
cnf(c_528,negated_conjecture,
( e3 = e0
| e2 = e0
| op(e2,e2) = e0 ),
inference(resolve,[status(thm)],[c_194,c_527]) ).
cnf(c_529,negated_conjecture,
( e3 = e0
| op(e2,e2) = e0 ),
inference(resolve,[status(thm)],[c_195,c_528]) ).
cnf(c_509,negated_conjecture,
op(e2,e2) = e0,
inference(resolve,[status(thm)],[c_196,c_529]) ).
cnf(c_530,negated_conjecture,
( op(e0,e0) = e3
| op(e3,e3) = e2
| e0 = e1
| op(e1,e1) = e0 ),
inference(paramod,[status(thm)],[c_508,c_326]) ).
cnf(c_531,negated_conjecture,
( op(e0,e0) = e3
| e0 = e2
| e0 = e1
| op(e1,e1) = e0 ),
inference(paramod,[status(thm)],[c_508,c_530]) ).
cnf(c_532,negated_conjecture,
( e0 = e3
| e0 = e2
| e0 = e1
| op(e1,e1) = e0 ),
inference(paramod,[status(thm)],[c_462,c_531]) ).
cnf(c_533,negated_conjecture,
( e0 = e3
| e0 = e2
| e1 = e0
| op(e1,e1) = e0 ),
inference(copy,[status(thm)],[c_532]) ).
cnf(c_534,negated_conjecture,
( e0 = e3
| e2 = e0
| e1 = e0
| op(e1,e1) = e0 ),
inference(copy,[status(thm)],[c_533]) ).
cnf(c_535,negated_conjecture,
( e3 = e0
| e2 = e0
| e1 = e0
| op(e1,e1) = e0 ),
inference(copy,[status(thm)],[c_534]) ).
cnf(c_536,negated_conjecture,
( e3 = e0
| e2 = e0
| op(e1,e1) = e0 ),
inference(resolve,[status(thm)],[c_194,c_535]) ).
cnf(c_537,negated_conjecture,
( e3 = e0
| op(e1,e1) = e0 ),
inference(resolve,[status(thm)],[c_195,c_536]) ).
cnf(c_510,negated_conjecture,
op(e1,e1) = e0,
inference(resolve,[status(thm)],[c_196,c_537]) ).
cnf(c_538,negated_conjecture,
( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0
| e0 != e0 ),
inference(paramod,[status(thm)],[c_462,c_200]) ).
cnf(c_539,negated_conjecture,
( op(e3,e3) != e0
| op(e2,e2) != e0
| e0 != e0
| e0 != e0 ),
inference(paramod,[status(thm)],[c_510,c_538]) ).
cnf(c_540,negated_conjecture,
( op(e3,e3) != e0
| e0 != e0
| e0 != e0
| e0 != e0 ),
inference(paramod,[status(thm)],[c_509,c_539]) ).
cnf(c_541,negated_conjecture,
( e0 != e0
| e0 != e0
| e0 != e0
| e0 != e0 ),
inference(paramod,[status(thm)],[c_508,c_540]) ).
cnf(c_542,negated_conjecture,
( e0 != e0
| e0 != e0
| e0 != e0 ),
inference(copy,[status(thm)],[c_541]) ).
cnf(c_543,negated_conjecture,
( e0 != e0
| e0 != e0 ),
inference(copy,[status(thm)],[c_542]) ).
cnf(c_544,negated_conjecture,
e0 != e0,
inference(copy,[status(thm)],[c_543]) ).
cnf(c_511,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_544]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG014+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n026.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Sat Sep 26 21:01:27 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.46 % Process 1942985 was started by sandbox on n026,
% 0.18/0.46 % Sat Sep 26 21:01:27 2026
% 0.18/0.46 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.36/0.62
% 0.36/0.62 % From the command line: assign(max_seconds, 300).
% 0.40/0.72
% 0.40/0.72 % SZS status Theorem for theBenchmark
% 0.40/0.72
% 0.40/0.72 % Proof 1 at 0.07 (+ 0.02) seconds.
% 0.40/0.72 % Length of proof is 19.
% 0.40/0.72 % Level of proof is 5.
% 0.40/0.72 % Maximum clause weight is 20.000.
% 0.40/0.72 % Given clauses 0.
% 0.40/0.72
% 0.40/0.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------