%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : ALG138+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 : n005.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:43 AM UTC 2026
% Result : Unsatisfiable 160.86s 171.29s
% Output : Proof 161.24s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(ax1,axiom,
( ( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ) ),
file('theBenchmark.p',ax1) ).
fof(ax2,axiom,
( ( op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 )
& ( op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 )
& ( op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 )
& ( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 )
& ( op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 )
& ( op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 )
& ( op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 )
& ( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 )
& ( op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 )
& ( op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 )
& ( op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 )
& ( op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 )
& ( op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 )
& ( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 )
& ( op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 )
& ( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 )
& ( op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 )
& ( op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 )
& ( op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 )
& ( op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 )
& ( op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 )
& ( op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 )
& ( op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 )
& ( op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 )
& ( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 )
& ( op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 )
& ( op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 )
& ( op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 )
& ( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 )
& ( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 )
& ( op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 )
& ( op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ) ),
file('theBenchmark.p',ax2) ).
fof(ax3,axiom,
( op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
file('theBenchmark.p',ax3) ).
fof(ax4,axiom,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
file('theBenchmark.p',ax4) ).
fof(ax5,axiom,
( op(e3,e3) = e3
& op(e2,e2) = e2
& op(e1,e1) = e1
& op(e0,e0) = e0 ),
file('theBenchmark.p',ax5) ).
fof(ax6,axiom,
~ ( e1 = op(op(e2,e3),e3)
& e0 = op(e2,e3) ),
file('theBenchmark.p',ax6) ).
fof(ax7,axiom,
~ ( e1 = op(op(e3,e2),e2)
& e0 = op(e3,e2) ),
file('theBenchmark.p',ax7) ).
fof(ax8,axiom,
~ ( e2 = op(op(e1,e3),e3)
& e0 = op(e1,e3) ),
file('theBenchmark.p',ax8) ).
fof(ax9,axiom,
~ ( e2 = op(op(e3,e1),e1)
& e0 = op(e3,e1) ),
file('theBenchmark.p',ax9) ).
fof(ax10,axiom,
~ ( e3 = op(op(e1,e2),e2)
& e0 = op(e1,e2) ),
file('theBenchmark.p',ax10) ).
fof(ax11,axiom,
~ ( e3 = op(op(e2,e1),e1)
& e0 = op(e2,e1) ),
file('theBenchmark.p',ax11) ).
fof(ax12,axiom,
~ ( e0 = op(op(e2,e3),e3)
& e1 = op(e2,e3) ),
file('theBenchmark.p',ax12) ).
fof(ax13,axiom,
~ ( e0 = op(op(e3,e2),e2)
& e1 = op(e3,e2) ),
file('theBenchmark.p',ax13) ).
fof(ax14,axiom,
~ ( e2 = op(op(e0,e3),e3)
& e1 = op(e0,e3) ),
file('theBenchmark.p',ax14) ).
fof(ax15,axiom,
~ ( e2 = op(op(e3,e0),e0)
& e1 = op(e3,e0) ),
file('theBenchmark.p',ax15) ).
fof(ax16,axiom,
~ ( e3 = op(op(e0,e2),e2)
& e1 = op(e0,e2) ),
file('theBenchmark.p',ax16) ).
fof(ax17,axiom,
~ ( e3 = op(op(e2,e0),e0)
& e1 = op(e2,e0) ),
file('theBenchmark.p',ax17) ).
fof(ax18,axiom,
~ ( e0 = op(op(e1,e3),e3)
& e2 = op(e1,e3) ),
file('theBenchmark.p',ax18) ).
fof(ax19,axiom,
~ ( e0 = op(op(e3,e1),e1)
& e2 = op(e3,e1) ),
file('theBenchmark.p',ax19) ).
fof(ax20,axiom,
~ ( e1 = op(op(e0,e3),e3)
& e2 = op(e0,e3) ),
file('theBenchmark.p',ax20) ).
fof(ax21,axiom,
~ ( e1 = op(op(e3,e0),e0)
& e2 = op(e3,e0) ),
file('theBenchmark.p',ax21) ).
fof(ax22,axiom,
~ ( e3 = op(op(e0,e1),e1)
& e2 = op(e0,e1) ),
file('theBenchmark.p',ax22) ).
fof(ax23,axiom,
~ ( e3 = op(op(e1,e0),e0)
& e2 = op(e1,e0) ),
file('theBenchmark.p',ax23) ).
fof(ax24,axiom,
~ ( e0 = op(op(e1,e2),e2)
& e3 = op(e1,e2) ),
file('theBenchmark.p',ax24) ).
fof(ax25,axiom,
~ ( e0 = op(op(e2,e1),e1)
& e3 = op(e2,e1) ),
file('theBenchmark.p',ax25) ).
fof(ax26,axiom,
~ ( e1 = op(op(e0,e2),e2)
& e3 = op(e0,e2) ),
file('theBenchmark.p',ax26) ).
fof(ax27,axiom,
~ ( e1 = op(op(e2,e0),e0)
& e3 = op(e2,e0) ),
file('theBenchmark.p',ax27) ).
fof(ax28,axiom,
~ ( e2 = op(op(e0,e1),e1)
& e3 = op(e0,e1) ),
file('theBenchmark.p',ax28) ).
fof(ax29,axiom,
~ ( e2 = op(op(e1,e0),e0)
& e3 = op(e1,e0) ),
file('theBenchmark.p',ax29) ).
fof(f_1_1,plain,
( ( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ) ),
inference(fof_nnf,[status(thm)],[ax1]) ).
fof(f_1_2,plain,
( ( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ) ),
inference(definitional_conversion,[status(esa)],[f_1_1]) ).
cnf(f_1_3,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_4,plain,
( op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_5,plain,
( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_6,plain,
( op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_7,plain,
( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_8,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_9,plain,
( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_10,plain,
( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_11,plain,
( op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_12,plain,
( op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_13,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_14,plain,
( op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_15,plain,
( op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_16,plain,
( op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_17,plain,
( op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_18,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(clausify,[status(thm)],[f_1_2]) ).
fof(f_2_1,plain,
( ( op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 )
& ( op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 )
& ( op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 )
& ( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 )
& ( op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 )
& ( op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 )
& ( op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 )
& ( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 )
& ( op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 )
& ( op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 )
& ( op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 )
& ( op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 )
& ( op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 )
& ( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 )
& ( op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 )
& ( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 )
& ( op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 )
& ( op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 )
& ( op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 )
& ( op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 )
& ( op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 )
& ( op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 )
& ( op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 )
& ( op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 )
& ( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 )
& ( op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 )
& ( op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 )
& ( op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 )
& ( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 )
& ( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 )
& ( op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 )
& ( op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ) ),
inference(fof_nnf,[status(thm)],[ax2]) ).
fof(f_2_2,plain,
( ( op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 )
& ( op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 )
& ( op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 )
& ( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 )
& ( op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 )
& ( op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 )
& ( op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 )
& ( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 )
& ( op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 )
& ( op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 )
& ( op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 )
& ( op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 )
& ( op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 )
& ( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 )
& ( op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 )
& ( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 )
& ( op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 )
& ( op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 )
& ( op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 )
& ( op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 )
& ( op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 )
& ( op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 )
& ( op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 )
& ( op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 )
& ( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 )
& ( op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 )
& ( op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 )
& ( op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 )
& ( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 )
& ( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 )
& ( op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 )
& ( op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ) ),
inference(definitional_conversion,[status(esa)],[f_2_1]) ).
cnf(f_2_3,plain,
( op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_4,plain,
( op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_5,plain,
( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_6,plain,
( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_7,plain,
( op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_8,plain,
( op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_9,plain,
( op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_10,plain,
( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_11,plain,
( op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_12,plain,
( op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_13,plain,
( op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_14,plain,
( op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_15,plain,
( op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_16,plain,
( op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_17,plain,
( op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_18,plain,
( op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_19,plain,
( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_20,plain,
( op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_21,plain,
( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_22,plain,
( op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_23,plain,
( op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_24,plain,
( op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_25,plain,
( op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_26,plain,
( op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_27,plain,
( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_28,plain,
( op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_29,plain,
( op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_30,plain,
( op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_31,plain,
( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_32,plain,
( op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_33,plain,
( op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 ),
inference(clausify,[status(thm)],[f_2_2]) ).
cnf(f_2_34,plain,
( op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 ),
inference(clausify,[status(thm)],[f_2_2]) ).
fof(f_3_1,plain,
( op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
inference(fof_nnf,[status(thm)],[ax3]) ).
fof(f_3_2,plain,
( op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
inference(definitional_conversion,[status(esa)],[f_3_1]) ).
cnf(f_3_3,plain,
op(e0,e0) != op(e1,e0),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_4,plain,
op(e0,e0) != op(e2,e0),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_5,plain,
op(e0,e0) != op(e3,e0),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_6,plain,
op(e1,e0) != op(e2,e0),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_7,plain,
op(e1,e0) != op(e3,e0),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_8,plain,
op(e2,e0) != op(e3,e0),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_9,plain,
op(e0,e1) != op(e1,e1),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_10,plain,
op(e0,e1) != op(e2,e1),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_11,plain,
op(e0,e1) != op(e3,e1),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_12,plain,
op(e1,e1) != op(e2,e1),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_13,plain,
op(e1,e1) != op(e3,e1),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_14,plain,
op(e2,e1) != op(e3,e1),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_15,plain,
op(e0,e2) != op(e1,e2),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_16,plain,
op(e0,e2) != op(e2,e2),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_17,plain,
op(e0,e2) != op(e3,e2),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_18,plain,
op(e1,e2) != op(e2,e2),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_19,plain,
op(e1,e2) != op(e3,e2),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_20,plain,
op(e2,e2) != op(e3,e2),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_21,plain,
op(e0,e3) != op(e1,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_22,plain,
op(e0,e3) != op(e2,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_23,plain,
op(e0,e3) != op(e3,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_24,plain,
op(e1,e3) != op(e2,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_25,plain,
op(e1,e3) != op(e3,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_26,plain,
op(e2,e3) != op(e3,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_27,plain,
op(e0,e0) != op(e0,e1),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_28,plain,
op(e0,e0) != op(e0,e2),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_29,plain,
op(e0,e0) != op(e0,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_30,plain,
op(e0,e1) != op(e0,e2),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_31,plain,
op(e0,e1) != op(e0,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_32,plain,
op(e0,e2) != op(e0,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_33,plain,
op(e1,e0) != op(e1,e1),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_34,plain,
op(e1,e0) != op(e1,e2),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_35,plain,
op(e1,e0) != op(e1,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_36,plain,
op(e1,e1) != op(e1,e2),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_37,plain,
op(e1,e1) != op(e1,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_38,plain,
op(e1,e2) != op(e1,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_39,plain,
op(e2,e0) != op(e2,e1),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_40,plain,
op(e2,e0) != op(e2,e2),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_41,plain,
op(e2,e0) != op(e2,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_42,plain,
op(e2,e1) != op(e2,e2),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_43,plain,
op(e2,e1) != op(e2,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_44,plain,
op(e2,e2) != op(e2,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_45,plain,
op(e3,e0) != op(e3,e1),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_46,plain,
op(e3,e0) != op(e3,e2),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_47,plain,
op(e3,e0) != op(e3,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_48,plain,
op(e3,e1) != op(e3,e2),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_49,plain,
op(e3,e1) != op(e3,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
cnf(f_3_50,plain,
op(e3,e2) != op(e3,e3),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
inference(fof_nnf,[status(thm)],[ax4]) ).
fof(f_4_2,plain,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
inference(definitional_conversion,[status(esa)],[f_4_1]) ).
cnf(f_4_3,plain,
e0 != e1,
inference(clausify,[status(thm)],[f_4_2]) ).
cnf(f_4_4,plain,
e0 != e2,
inference(clausify,[status(thm)],[f_4_2]) ).
cnf(f_4_5,plain,
e0 != e3,
inference(clausify,[status(thm)],[f_4_2]) ).
cnf(f_4_6,plain,
e1 != e2,
inference(clausify,[status(thm)],[f_4_2]) ).
cnf(f_4_7,plain,
e1 != e3,
inference(clausify,[status(thm)],[f_4_2]) ).
cnf(f_4_8,plain,
e2 != e3,
inference(clausify,[status(thm)],[f_4_2]) ).
fof(f_5_1,plain,
( op(e3,e3) = e3
& op(e2,e2) = e2
& op(e1,e1) = e1
& op(e0,e0) = e0 ),
inference(fof_nnf,[status(thm)],[ax5]) ).
fof(f_5_2,plain,
( op(e3,e3) = e3
& op(e2,e2) = e2
& op(e1,e1) = e1
& op(e0,e0) = e0 ),
inference(definitional_conversion,[status(esa)],[f_5_1]) ).
cnf(f_5_3,plain,
op(e0,e0) = e0,
inference(clausify,[status(thm)],[f_5_2]) ).
cnf(f_5_4,plain,
op(e1,e1) = e1,
inference(clausify,[status(thm)],[f_5_2]) ).
cnf(f_5_5,plain,
op(e2,e2) = e2,
inference(clausify,[status(thm)],[f_5_2]) ).
cnf(f_5_6,plain,
op(e3,e3) = e3,
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
( e1 != op(op(e2,e3),e3)
| e0 != op(e2,e3) ),
inference(fof_nnf,[status(thm)],[ax6]) ).
fof(f_6_2,plain,
( e1 != op(op(e2,e3),e3)
| e0 != op(e2,e3) ),
inference(definitional_conversion,[status(esa)],[f_6_1]) ).
cnf(f_6_3,plain,
( e1 != op(op(e2,e3),e3)
| e0 != op(e2,e3) ),
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_7_1,plain,
( e1 != op(op(e3,e2),e2)
| e0 != op(e3,e2) ),
inference(fof_nnf,[status(thm)],[ax7]) ).
fof(f_7_2,plain,
( e1 != op(op(e3,e2),e2)
| e0 != op(e3,e2) ),
inference(definitional_conversion,[status(esa)],[f_7_1]) ).
cnf(f_7_3,plain,
( e1 != op(op(e3,e2),e2)
| e0 != op(e3,e2) ),
inference(clausify,[status(thm)],[f_7_2]) ).
fof(f_8_1,plain,
( e2 != op(op(e1,e3),e3)
| e0 != op(e1,e3) ),
inference(fof_nnf,[status(thm)],[ax8]) ).
fof(f_8_2,plain,
( e2 != op(op(e1,e3),e3)
| e0 != op(e1,e3) ),
inference(definitional_conversion,[status(esa)],[f_8_1]) ).
cnf(f_8_3,plain,
( e2 != op(op(e1,e3),e3)
| e0 != op(e1,e3) ),
inference(clausify,[status(thm)],[f_8_2]) ).
fof(f_9_1,plain,
( e2 != op(op(e3,e1),e1)
| e0 != op(e3,e1) ),
inference(fof_nnf,[status(thm)],[ax9]) ).
fof(f_9_2,plain,
( e2 != op(op(e3,e1),e1)
| e0 != op(e3,e1) ),
inference(definitional_conversion,[status(esa)],[f_9_1]) ).
cnf(f_9_3,plain,
( e2 != op(op(e3,e1),e1)
| e0 != op(e3,e1) ),
inference(clausify,[status(thm)],[f_9_2]) ).
fof(f_10_1,plain,
( e3 != op(op(e1,e2),e2)
| e0 != op(e1,e2) ),
inference(fof_nnf,[status(thm)],[ax10]) ).
fof(f_10_2,plain,
( e3 != op(op(e1,e2),e2)
| e0 != op(e1,e2) ),
inference(definitional_conversion,[status(esa)],[f_10_1]) ).
cnf(f_10_3,plain,
( e3 != op(op(e1,e2),e2)
| e0 != op(e1,e2) ),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
( e3 != op(op(e2,e1),e1)
| e0 != op(e2,e1) ),
inference(fof_nnf,[status(thm)],[ax11]) ).
fof(f_11_2,plain,
( e3 != op(op(e2,e1),e1)
| e0 != op(e2,e1) ),
inference(definitional_conversion,[status(esa)],[f_11_1]) ).
cnf(f_11_3,plain,
( e3 != op(op(e2,e1),e1)
| e0 != op(e2,e1) ),
inference(clausify,[status(thm)],[f_11_2]) ).
fof(f_12_1,plain,
( e0 != op(op(e2,e3),e3)
| e1 != op(e2,e3) ),
inference(fof_nnf,[status(thm)],[ax12]) ).
fof(f_12_2,plain,
( e0 != op(op(e2,e3),e3)
| e1 != op(e2,e3) ),
inference(definitional_conversion,[status(esa)],[f_12_1]) ).
cnf(f_12_3,plain,
( e0 != op(op(e2,e3),e3)
| e1 != op(e2,e3) ),
inference(clausify,[status(thm)],[f_12_2]) ).
fof(f_13_1,plain,
( e0 != op(op(e3,e2),e2)
| e1 != op(e3,e2) ),
inference(fof_nnf,[status(thm)],[ax13]) ).
fof(f_13_2,plain,
( e0 != op(op(e3,e2),e2)
| e1 != op(e3,e2) ),
inference(definitional_conversion,[status(esa)],[f_13_1]) ).
cnf(f_13_3,plain,
( e0 != op(op(e3,e2),e2)
| e1 != op(e3,e2) ),
inference(clausify,[status(thm)],[f_13_2]) ).
fof(f_14_1,plain,
( e2 != op(op(e0,e3),e3)
| e1 != op(e0,e3) ),
inference(fof_nnf,[status(thm)],[ax14]) ).
fof(f_14_2,plain,
( e2 != op(op(e0,e3),e3)
| e1 != op(e0,e3) ),
inference(definitional_conversion,[status(esa)],[f_14_1]) ).
cnf(f_14_3,plain,
( e2 != op(op(e0,e3),e3)
| e1 != op(e0,e3) ),
inference(clausify,[status(thm)],[f_14_2]) ).
fof(f_15_1,plain,
( e2 != op(op(e3,e0),e0)
| e1 != op(e3,e0) ),
inference(fof_nnf,[status(thm)],[ax15]) ).
fof(f_15_2,plain,
( e2 != op(op(e3,e0),e0)
| e1 != op(e3,e0) ),
inference(definitional_conversion,[status(esa)],[f_15_1]) ).
cnf(f_15_3,plain,
( e2 != op(op(e3,e0),e0)
| e1 != op(e3,e0) ),
inference(clausify,[status(thm)],[f_15_2]) ).
fof(f_16_1,plain,
( e3 != op(op(e0,e2),e2)
| e1 != op(e0,e2) ),
inference(fof_nnf,[status(thm)],[ax16]) ).
fof(f_16_2,plain,
( e3 != op(op(e0,e2),e2)
| e1 != op(e0,e2) ),
inference(definitional_conversion,[status(esa)],[f_16_1]) ).
cnf(f_16_3,plain,
( e3 != op(op(e0,e2),e2)
| e1 != op(e0,e2) ),
inference(clausify,[status(thm)],[f_16_2]) ).
fof(f_17_1,plain,
( e3 != op(op(e2,e0),e0)
| e1 != op(e2,e0) ),
inference(fof_nnf,[status(thm)],[ax17]) ).
fof(f_17_2,plain,
( e3 != op(op(e2,e0),e0)
| e1 != op(e2,e0) ),
inference(definitional_conversion,[status(esa)],[f_17_1]) ).
cnf(f_17_3,plain,
( e3 != op(op(e2,e0),e0)
| e1 != op(e2,e0) ),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,plain,
( e0 != op(op(e1,e3),e3)
| e2 != op(e1,e3) ),
inference(fof_nnf,[status(thm)],[ax18]) ).
fof(f_18_2,plain,
( e0 != op(op(e1,e3),e3)
| e2 != op(e1,e3) ),
inference(definitional_conversion,[status(esa)],[f_18_1]) ).
cnf(f_18_3,plain,
( e0 != op(op(e1,e3),e3)
| e2 != op(e1,e3) ),
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_19_1,plain,
( e0 != op(op(e3,e1),e1)
| e2 != op(e3,e1) ),
inference(fof_nnf,[status(thm)],[ax19]) ).
fof(f_19_2,plain,
( e0 != op(op(e3,e1),e1)
| e2 != op(e3,e1) ),
inference(definitional_conversion,[status(esa)],[f_19_1]) ).
cnf(f_19_3,plain,
( e0 != op(op(e3,e1),e1)
| e2 != op(e3,e1) ),
inference(clausify,[status(thm)],[f_19_2]) ).
fof(f_20_1,plain,
( e1 != op(op(e0,e3),e3)
| e2 != op(e0,e3) ),
inference(fof_nnf,[status(thm)],[ax20]) ).
fof(f_20_2,plain,
( e1 != op(op(e0,e3),e3)
| e2 != op(e0,e3) ),
inference(definitional_conversion,[status(esa)],[f_20_1]) ).
cnf(f_20_3,plain,
( e1 != op(op(e0,e3),e3)
| e2 != op(e0,e3) ),
inference(clausify,[status(thm)],[f_20_2]) ).
fof(f_21_1,plain,
( e1 != op(op(e3,e0),e0)
| e2 != op(e3,e0) ),
inference(fof_nnf,[status(thm)],[ax21]) ).
fof(f_21_2,plain,
( e1 != op(op(e3,e0),e0)
| e2 != op(e3,e0) ),
inference(definitional_conversion,[status(esa)],[f_21_1]) ).
cnf(f_21_3,plain,
( e1 != op(op(e3,e0),e0)
| e2 != op(e3,e0) ),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,plain,
( e3 != op(op(e0,e1),e1)
| e2 != op(e0,e1) ),
inference(fof_nnf,[status(thm)],[ax22]) ).
fof(f_22_2,plain,
( e3 != op(op(e0,e1),e1)
| e2 != op(e0,e1) ),
inference(definitional_conversion,[status(esa)],[f_22_1]) ).
cnf(f_22_3,plain,
( e3 != op(op(e0,e1),e1)
| e2 != op(e0,e1) ),
inference(clausify,[status(thm)],[f_22_2]) ).
fof(f_23_1,plain,
( e3 != op(op(e1,e0),e0)
| e2 != op(e1,e0) ),
inference(fof_nnf,[status(thm)],[ax23]) ).
fof(f_23_2,plain,
( e3 != op(op(e1,e0),e0)
| e2 != op(e1,e0) ),
inference(definitional_conversion,[status(esa)],[f_23_1]) ).
cnf(f_23_3,plain,
( e3 != op(op(e1,e0),e0)
| e2 != op(e1,e0) ),
inference(clausify,[status(thm)],[f_23_2]) ).
fof(f_24_1,plain,
( e0 != op(op(e1,e2),e2)
| e3 != op(e1,e2) ),
inference(fof_nnf,[status(thm)],[ax24]) ).
fof(f_24_2,plain,
( e0 != op(op(e1,e2),e2)
| e3 != op(e1,e2) ),
inference(definitional_conversion,[status(esa)],[f_24_1]) ).
cnf(f_24_3,plain,
( e0 != op(op(e1,e2),e2)
| e3 != op(e1,e2) ),
inference(clausify,[status(thm)],[f_24_2]) ).
fof(f_25_1,plain,
( e0 != op(op(e2,e1),e1)
| e3 != op(e2,e1) ),
inference(fof_nnf,[status(thm)],[ax25]) ).
fof(f_25_2,plain,
( e0 != op(op(e2,e1),e1)
| e3 != op(e2,e1) ),
inference(definitional_conversion,[status(esa)],[f_25_1]) ).
cnf(f_25_3,plain,
( e0 != op(op(e2,e1),e1)
| e3 != op(e2,e1) ),
inference(clausify,[status(thm)],[f_25_2]) ).
fof(f_26_1,plain,
( e1 != op(op(e0,e2),e2)
| e3 != op(e0,e2) ),
inference(fof_nnf,[status(thm)],[ax26]) ).
fof(f_26_2,plain,
( e1 != op(op(e0,e2),e2)
| e3 != op(e0,e2) ),
inference(definitional_conversion,[status(esa)],[f_26_1]) ).
cnf(f_26_3,plain,
( e1 != op(op(e0,e2),e2)
| e3 != op(e0,e2) ),
inference(clausify,[status(thm)],[f_26_2]) ).
fof(f_27_1,plain,
( e1 != op(op(e2,e0),e0)
| e3 != op(e2,e0) ),
inference(fof_nnf,[status(thm)],[ax27]) ).
fof(f_27_2,plain,
( e1 != op(op(e2,e0),e0)
| e3 != op(e2,e0) ),
inference(definitional_conversion,[status(esa)],[f_27_1]) ).
cnf(f_27_3,plain,
( e1 != op(op(e2,e0),e0)
| e3 != op(e2,e0) ),
inference(clausify,[status(thm)],[f_27_2]) ).
fof(f_28_1,plain,
( e2 != op(op(e0,e1),e1)
| e3 != op(e0,e1) ),
inference(fof_nnf,[status(thm)],[ax28]) ).
fof(f_28_2,plain,
( e2 != op(op(e0,e1),e1)
| e3 != op(e0,e1) ),
inference(definitional_conversion,[status(esa)],[f_28_1]) ).
cnf(f_28_3,plain,
( e2 != op(op(e0,e1),e1)
| e3 != op(e0,e1) ),
inference(clausify,[status(thm)],[f_28_2]) ).
fof(f_29_1,plain,
( e2 != op(op(e1,e0),e0)
| e3 != op(e1,e0) ),
inference(fof_nnf,[status(thm)],[ax29]) ).
fof(f_29_2,plain,
( e2 != op(op(e1,e0),e0)
| e3 != op(e1,e0) ),
inference(definitional_conversion,[status(esa)],[f_29_1]) ).
cnf(f_29_3,plain,
( e2 != op(op(e1,e0),e0)
| e3 != op(e1,e0) ),
inference(clausify,[status(thm)],[f_29_2]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
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(equality_4,axiom,
( op(Eq_x_0,Eq_x_1) = op(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG138+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 This is a FOF_UNS_EPR_PEQ 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.11/5.38 % Computer : n005.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Sun Sep 20 09:19:26 UTC 2026
% 0.11/5.38 % CPUTime :
% 160.86/171.29 % SZS status Unsatisfiable for theBenchmark
% 160.86/171.29 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------