%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : ALG138+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:47:39 AM UTC 2026
% Result : Unsatisfiable 17.46s 2.59s
% Output : CNFRefutation 17.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 6
% Syntax : Number of formulae : 115 ( 41 unt; 0 def)
% Number of atoms : 444 ( 443 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 440 ( 111 ~; 241 |; 88 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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 ) ) ).
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) ) ).
fof(ax4,axiom,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ) ).
fof(ax5,axiom,
( op(e3,e3) = e3
& op(e2,e2) = e2
& op(e1,e1) = e1
& op(e0,e0) = e0 ) ).
fof(ax15,axiom,
~ ( e2 = op(op(e3,e0),e0)
& e1 = op(e3,e0) ) ).
fof(ax17,axiom,
~ ( e3 = op(op(e2,e0),e0)
& e1 = op(e2,e0) ) ).
cnf(c18,plain,
( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 ),
inference(clausification,[status(esa)],[ax2]) ).
cnf(c19,plain,
( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 ),
inference(clausification,[status(esa)],[ax2]) ).
cnf(c20,plain,
( op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 ),
inference(clausification,[status(esa)],[ax2]) ).
cnf(c21,plain,
( op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 ),
inference(clausification,[status(esa)],[ax2]) ).
cnf(c22,plain,
( op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 ),
inference(clausification,[status(esa)],[ax2]) ).
cnf(c23,plain,
( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 ),
inference(clausification,[status(esa)],[ax2]) ).
cnf(c30,plain,
( op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 ),
inference(clausification,[status(esa)],[ax2]) ).
cnf(c43,plain,
( op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 ),
inference(clausification,[status(esa)],[ax2]) ).
cnf(c47,plain,
( op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 ),
inference(clausification,[status(esa)],[ax2]) ).
cnf(c54,plain,
op(e0,e1) != op(e1,e1),
inference(clausification,[status(esa)],[ax3]) ).
cnf(c60,plain,
op(e0,e2) != op(e1,e2),
inference(clausification,[status(esa)],[ax3]) ).
cnf(c61,plain,
op(e0,e2) != op(e2,e2),
inference(clausification,[status(esa)],[ax3]) ).
cnf(c68,plain,
op(e0,e3) != op(e3,e3),
inference(clausification,[status(esa)],[ax3]) ).
cnf(c70,plain,
op(e1,e3) != op(e3,e3),
inference(clausification,[status(esa)],[ax3]) ).
cnf(c71,plain,
op(e2,e3) != op(e3,e3),
inference(clausification,[status(esa)],[ax3]) ).
cnf(c77,plain,
op(e0,e2) != op(e0,e3),
inference(clausification,[status(esa)],[ax3]) ).
cnf(c78,plain,
op(e1,e0) != op(e1,e1),
inference(clausification,[status(esa)],[ax3]) ).
cnf(c82,plain,
op(e1,e1) != op(e1,e3),
inference(clausification,[status(esa)],[ax3]) ).
cnf(c85,plain,
op(e2,e0) != op(e2,e2),
inference(clausification,[status(esa)],[ax3]) ).
cnf(c86,plain,
op(e2,e0) != op(e2,e3),
inference(clausification,[status(esa)],[ax3]) ).
cnf(c92,plain,
op(e3,e0) != op(e3,e3),
inference(clausification,[status(esa)],[ax3]) ).
cnf(c96,plain,
e0 != e1,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c97,plain,
e0 != e2,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c98,plain,
e0 != e3,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c99,plain,
e1 != e2,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c100,plain,
e1 != e3,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c101,plain,
e2 != e3,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c102,plain,
op(e0,e0) = e0,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c103,plain,
op(e1,e1) = e1,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c104,plain,
op(e2,e2) = e2,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c105,plain,
op(e3,e3) = e3,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c115,plain,
( e2 != op(op(e3,e0),e0)
| e1 != op(e3,e0) ),
inference(clausification,[status(esa)],[ax15]) ).
cnf(c117,plain,
( e3 != op(op(e2,e0),e0)
| e1 != op(e2,e0) ),
inference(clausification,[status(esa)],[ax17]) ).
cnf(d0,plain,
( op(e1,e3) = e3
| e1 = e3
| op(e1,e2) = e3
| op(e1,e0) = e3 ),
inference(demodulation,[status(thm)],[c30,c103]) ).
cnf(d1,plain,
( op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e0) = e3 ),
inference(resolution,[status(thm)],[c100,d0]) ).
cnf(d2,plain,
op(e1,e3) != e3,
inference(demodulation,[status(thm)],[c70,c105]) ).
cnf(d3,plain,
( op(e1,e2) = e3
| op(e1,e0) = e3 ),
inference(resolution,[status(thm)],[d2,d1]) ).
cnf(d4,plain,
( op(e1,e0) = e3
| op(e0,e2) != e3 ),
inference(superposition,[status(thm)],[d3,c60]) ).
cnf(d5,plain,
( op(e0,e3) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| e0 = e3 ),
inference(demodulation,[status(thm)],[c22,c102]) ).
cnf(d6,plain,
( op(e0,e3) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3 ),
inference(resolution,[status(thm)],[c98,d5]) ).
cnf(d7,plain,
op(e0,e3) != e3,
inference(demodulation,[status(thm)],[c68,c105]) ).
cnf(d8,plain,
( op(e0,e1) = e3
| op(e0,e2) = e3 ),
inference(resolution,[status(thm)],[d7,d6]) ).
cnf(d9,plain,
( op(e0,e3) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| e0 = e2 ),
inference(demodulation,[status(thm)],[c20,c102]) ).
cnf(d10,plain,
( op(e0,e3) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2 ),
inference(resolution,[status(thm)],[c97,d9]) ).
cnf(d11,plain,
( op(e0,e3) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| e0 = e1 ),
inference(demodulation,[status(thm)],[c18,c102]) ).
cnf(d12,plain,
( op(e0,e3) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1 ),
inference(resolution,[status(thm)],[c96,d11]) ).
cnf(d13,plain,
op(e0,e1) != e1,
inference(demodulation,[status(thm)],[c54,c103]) ).
cnf(d14,plain,
( op(e0,e3) = e1
| op(e0,e2) = e1 ),
inference(resolution,[status(thm)],[d13,d12]) ).
cnf(d15,plain,
( op(e0,e2) = e1
| op(e0,e1) = e2
| op(e0,e2) = e2
| e1 = e2 ),
inference(superposition,[status(thm)],[d14,d10]) ).
cnf(d16,plain,
( op(e0,e1) = e2
| op(e0,e2) = e1
| op(e0,e2) = e2 ),
inference(resolution,[status(thm)],[c99,d15]) ).
cnf(d17,plain,
op(e0,e2) != e2,
inference(demodulation,[status(thm)],[c61,c104]) ).
cnf(d18,plain,
( op(e0,e1) = e2
| op(e0,e2) = e1 ),
inference(resolution,[status(thm)],[d17,d16]) ).
cnf(d19,plain,
( op(e0,e2) = e1
| op(e0,e2) = e3
| e2 = e3 ),
inference(superposition,[status(thm)],[d18,d8]) ).
cnf(d20,plain,
( op(e0,e2) = e3
| op(e0,e2) = e1 ),
inference(resolution,[status(thm)],[c101,d19]) ).
cnf(d21,plain,
( op(e0,e2) = e1
| op(e1,e0) = e3
| e3 != e3 ),
inference(superposition,[status(thm)],[d20,d4]) ).
cnf(d22,plain,
( e3 = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e0,e3) = e3 ),
inference(demodulation,[status(thm)],[c47,c105]) ).
cnf(d23,plain,
( e3 = e3
| op(e1,e3) = e3
| op(e2,e3) = e3 ),
inference(resolution,[status(thm)],[d7,d22]) ).
cnf(d24,plain,
( e3 = e3
| op(e2,e3) = e3 ),
inference(resolution,[status(thm)],[d2,d23]) ).
cnf(d25,plain,
op(e2,e3) != e3,
inference(demodulation,[status(thm)],[c71,c105]) ).
cnf(d26,plain,
e3 = e3,
inference(resolution,[status(thm)],[d25,d24]) ).
cnf(d27,plain,
( op(e1,e0) = e3
| op(e0,e2) = e1 ),
inference(resolution,[status(thm)],[d26,d21]) ).
cnf(d28,plain,
e1 != op(e1,e3),
inference(demodulation,[status(thm)],[c82,c103]) ).
cnf(d29,plain,
( e3 = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e0,e3) = e1 ),
inference(demodulation,[status(thm)],[c43,c105]) ).
cnf(d30,plain,
( e3 = e1
| op(e2,e3) = e1
| op(e0,e3) = e1
| e1 != e1 ),
inference(superposition,[status(thm)],[d29,d28]) ).
cnf(d31,plain,
( e3 = e1
| op(e2,e3) = e1
| op(e0,e3) = e1 ),
inference(equality_resolution,[status(thm)],[d30]) ).
cnf(d32,plain,
( e3 = e1
| op(e0,e3) = e1
| op(e2,e0) != e1 ),
inference(superposition,[status(thm)],[d31,c86]) ).
cnf(d33,plain,
( op(e3,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| e0 = e1 ),
inference(demodulation,[status(thm)],[c19,c102]) ).
cnf(d34,plain,
( op(e3,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1 ),
inference(resolution,[status(thm)],[c96,d33]) ).
cnf(d35,plain,
op(e1,e0) != e1,
inference(demodulation,[status(thm)],[c78,c103]) ).
cnf(d36,plain,
( op(e3,e0) = e1
| op(e2,e0) = e1 ),
inference(resolution,[status(thm)],[d35,d34]) ).
cnf(d37,plain,
( op(e2,e0) = e1
| e1 != op(e3,e0)
| e2 != op(e1,e0) ),
inference(superposition,[status(thm)],[d36,c115]) ).
cnf(d38,plain,
( op(e2,e0) = e1
| e2 != op(e1,e0)
| op(e2,e0) = e1
| e1 != e1 ),
inference(superposition,[status(thm)],[d36,d37]) ).
cnf(d39,plain,
( op(e3,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| e0 = e2 ),
inference(demodulation,[status(thm)],[c21,c102]) ).
cnf(d40,plain,
( op(e3,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2 ),
inference(resolution,[status(thm)],[c97,d39]) ).
cnf(d41,plain,
( op(e1,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e2
| op(e2,e0) = e2
| e1 = e2 ),
inference(superposition,[status(thm)],[d34,d40]) ).
cnf(d42,plain,
( op(e1,e0) = e1
| op(e1,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e2 ),
inference(resolution,[status(thm)],[c99,d41]) ).
cnf(d43,plain,
( op(e1,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e2 ),
inference(resolution,[status(thm)],[d35,d42]) ).
cnf(d44,plain,
op(e2,e0) != e2,
inference(demodulation,[status(thm)],[c85,c104]) ).
cnf(d45,plain,
( op(e1,e0) = e2
| op(e2,e0) = e1 ),
inference(resolution,[status(thm)],[d44,d43]) ).
cnf(d46,plain,
( op(e2,e0) = e1
| e1 != e1
| op(e2,e0) = e1
| e2 != e2 ),
inference(superposition,[status(thm)],[d45,d38]) ).
cnf(d47,plain,
( e2 != e2
| op(e2,e0) = e1 ),
inference(equality_resolution,[status(thm)],[d46]) ).
cnf(d48,plain,
op(e2,e0) = e1,
inference(equality_resolution,[status(thm)],[d47]) ).
cnf(d49,plain,
( e3 = e1
| op(e0,e3) = e1 ),
inference(resolution,[status(thm)],[d48,d32]) ).
cnf(d50,plain,
( op(e3,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| e0 = e3 ),
inference(demodulation,[status(thm)],[c23,c102]) ).
cnf(d51,plain,
( op(e3,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3 ),
inference(resolution,[status(thm)],[c98,d50]) ).
cnf(d52,plain,
op(e3,e0) != e3,
inference(demodulation,[status(thm)],[c92,c105]) ).
cnf(d53,plain,
( op(e1,e0) = e3
| op(e2,e0) = e3 ),
inference(resolution,[status(thm)],[d52,d51]) ).
cnf(d54,plain,
( op(e2,e0) = e3
| e3 != e1 ),
inference(superposition,[status(thm)],[d53,d35]) ).
cnf(d55,plain,
( e3 != e1
| e1 = e3 ),
inference(demodulation,[status(thm)],[d54,d48]) ).
cnf(d56,plain,
e3 != e1,
inference(resolution,[status(thm)],[c100,d55]) ).
cnf(d57,plain,
op(e0,e3) = e1,
inference(resolution,[status(thm)],[d56,d49]) ).
cnf(d58,plain,
op(e0,e2) != e1,
inference(demodulation,[status(thm)],[c77,d57]) ).
cnf(d59,plain,
op(e1,e0) = e3,
inference(resolution,[status(thm)],[d58,d27]) ).
cnf(d60,plain,
( e3 != op(op(e2,e0),e0)
| e1 != e1 ),
inference(demodulation,[status(thm)],[c117,d48]) ).
cnf(d61,plain,
( e3 != op(e1,e0)
| e1 != e1 ),
inference(demodulation,[status(thm)],[d60,d48]) ).
cnf(d62,plain,
( e3 != e3
| e1 != e1 ),
inference(demodulation,[status(thm)],[d61,d59]) ).
cnf(d63,plain,
e1 != e1,
inference(resolution,[status(thm)],[d26,d62]) ).
cnf(d64,plain,
( op(e1,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e1
| op(e2,e0) = e1
| e2 = e1 ),
inference(superposition,[status(thm)],[d40,d34]) ).
cnf(d65,plain,
( e2 = e1
| op(e1,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e2 ),
inference(resolution,[status(thm)],[d35,d64]) ).
cnf(d66,plain,
( e2 = e1
| op(e1,e0) = e2
| op(e2,e0) = e1 ),
inference(resolution,[status(thm)],[d44,d65]) ).
cnf(d67,plain,
( e2 = e1
| op(e2,e0) = e1
| op(e2,e0) = e3
| e2 = e3 ),
inference(superposition,[status(thm)],[d66,d53]) ).
cnf(d68,plain,
( e2 = e3
| e2 = e1
| op(e2,e0) = e3
| e1 = e1 ),
inference(demodulation,[status(thm)],[d67,d48]) ).
cnf(d69,plain,
( e2 = e3
| e2 = e1
| e1 = e3
| e1 = e1 ),
inference(demodulation,[status(thm)],[d68,d48]) ).
cnf(d70,plain,
( e2 = e3
| e2 = e1
| e1 = e1 ),
inference(resolution,[status(thm)],[c100,d69]) ).
cnf(d71,plain,
( e2 = e1
| e1 = e1 ),
inference(resolution,[status(thm)],[c101,d70]) ).
cnf(d72,plain,
( op(e0,e2) = e1
| e2 != e1 ),
inference(superposition,[status(thm)],[d18,d13]) ).
cnf(d73,plain,
e2 != e1,
inference(resolution,[status(thm)],[d58,d72]) ).
cnf(d74,plain,
e1 = e1,
inference(resolution,[status(thm)],[d73,d71]) ).
cnf(d75,plain,
$false,
inference(resolution,[status(thm)],[d74,d63]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG138+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n015.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sat Sep 26 21:18:44 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.46/2.59 % SZS status Unsatisfiable for theBenchmark.p
% 17.46/2.59 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------