%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEV214^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n002.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 : Wed Sep 30 08:37:00 AM UTC 2026
% Result : Theorem 13.64s 3.36s
% Output : Refutation 12.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 7
% Syntax : Number of formulae : 48 ( 12 unt; 0 typ; 6 def)
% Number of atoms : 239 ( 238 equ; 14 cnn)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 498 ( 83 ~; 128 |; 36 &; 233 @)
% ( 0 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 7 ( 7 >; 0 *; 0 +; 0 <<)
% Number of symbols : 13 ( 10 usr; 9 con; 0-2 aty)
% Number of variables : 111 ( 16 ^; 54 !; 35 ?; 111 :)
% ( 0 !>; 0 ?*; 0 @-; 6 @+)
% Comments :
%------------------------------------------------------------------------------
thf(iS_type,type,
iS: $tType ).
thf(c0_decl,type,
c0: iS ).
thf(cP_decl,type,
cP: iS > iS > iS ).
thf(sk1_decl,type,
sk1: ( iS > $o ) > iS ).
thf(sk2_decl,type,
sk2: ( iS > $o ) > iS ).
thf(sk5_decl,type,
sk5: iS ).
thf(sk6_decl,type,
sk6: iS ).
thf(sk39_decl,type,
sk39: iS ).
thf(sk41_decl,type,
sk41: iS ).
thf(sk42_decl,type,
sk42: iS ).
thf(sk44_decl,type,
sk44: iS ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: iS > $o] :
@+[B: iS] :
~ ! [C: iS] :
( ( ( A @ B )
& ( A @ C ) )
=> ( A @ ( cP @ B @ C ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: iS > $o] :
@+[B: iS] :
~ ( ( ( A @ ( sk1 @ A ) )
& ( A @ B ) )
=> ( A @ ( cP @ ( sk1 @ A ) @ B ) ) ) ) ) ).
thf(sk39_def,definition,
( sk39
= ( @+[A: iS] :
( c0
= ( cP @ sk5 @ A ) ) ) ) ).
thf(sk41_def,definition,
( sk41
= ( @+[A: iS] :
( c0
= ( cP @ sk5 @ A ) ) ) ) ).
thf(sk42_def,definition,
( sk42
= ( @+[A: iS] :
( c0
= ( cP @ A @ sk6 ) ) ) ) ).
thf(sk44_def,definition,
( sk44
= ( @+[A: iS] :
( c0
= ( cP @ A @ sk6 ) ) ) ) ).
thf(1,conjecture,
( ( ! [A: iS,B: iS] :
( ( cP @ A @ B )
!= c0 )
& ! [A: iS,B: iS,C: iS,D: iS] :
( ( ( cP @ A @ C )
= ( cP @ B @ D ) )
=> ( ( A = B )
& ( C = D ) ) )
& ! [A: iS > $o] :
( ( ( A @ c0 )
& ! [B: iS,C: iS] :
( ( ( A @ B )
& ( A @ C ) )
=> ( A @ ( cP @ B @ C ) ) ) )
=> ! [B: iS] : ( A @ B ) ) )
=> ( ( ( ^ [A: iS] :
( ( A = c0 )
| ? [B: iS] :
( c0
= ( cP @ A @ B ) ) ) )
= ( (=) @ iS @ c0 ) )
& ( ( ^ [A: iS] :
( ( A = c0 )
| ? [B: iS] :
( c0
= ( cP @ B @ A ) ) ) )
= ( (=) @ iS @ c0 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cS_T_LR_LEM2_pme) ).
thf(2,negated_conjecture,
~ ( ( ! [A: iS,B: iS] :
( ( cP @ A @ B )
!= c0 )
& ! [A: iS,B: iS,C: iS,D: iS] :
( ( ( cP @ A @ C )
= ( cP @ B @ D ) )
=> ( ( A = B )
& ( C = D ) ) )
& ! [A: iS > $o] :
( ( ( A @ c0 )
& ! [B: iS,C: iS] :
( ( ( A @ B )
& ( A @ C ) )
=> ( A @ ( cP @ B @ C ) ) ) )
=> ! [B: iS] : ( A @ B ) ) )
=> ( ( ( ^ [A: iS] :
( ( A = c0 )
| ? [B: iS] :
( c0
= ( cP @ A @ B ) ) ) )
= ( (=) @ iS @ c0 ) )
& ( ( ^ [A: iS] :
( ( A = c0 )
| ? [B: iS] :
( c0
= ( cP @ B @ A ) ) ) )
= ( (=) @ iS @ c0 ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ( ( ! [A: iS,B: iS] :
( ( cP @ A @ B )
!= c0 )
& ! [A: iS,B: iS,C: iS,D: iS] :
( ( ( cP @ A @ C )
= ( cP @ B @ D ) )
=> ( ( A = B )
& ( C = D ) ) )
& ! [A: iS > $o] :
( ( ( A @ c0 )
& ! [B: iS,C: iS] :
( ( ( A @ B )
& ( A @ C ) )
=> ( A @ ( cP @ B @ C ) ) ) )
=> ! [B: iS] : ( A @ B ) ) )
=> ( ( ( ^ [A: iS] :
( ( A = c0 )
| ? [B: iS] :
( c0
= ( cP @ A @ B ) ) ) )
= ( (=) @ iS @ c0 ) )
& ( ( ^ [A: iS] :
( ( A = c0 )
| ? [B: iS] :
( c0
= ( cP @ B @ A ) ) ) )
= ( (=) @ iS @ c0 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
~ ( ( ~ ? [A: iS,B: iS] :
( ( cP @ A @ B )
= c0 )
& ! [A: iS,B: iS,C: iS,D: iS] :
( ( ( cP @ A @ C )
= ( cP @ B @ D ) )
=> ( ( A = B )
& ( C = D ) ) )
& ! [A: iS > $o] :
( ( ( A @ c0 )
& ! [B: iS,C: iS] :
( ( ( A @ B )
& ( A @ C ) )
=> ( A @ ( cP @ B @ C ) ) ) )
=> ! [B: iS] : ( A @ B ) ) )
=> ( ( ( ^ [A: iS] :
( ( A = c0 )
| ? [B: iS] :
( c0
= ( cP @ A @ B ) ) ) )
= ( (=) @ iS @ c0 ) )
& ( ( ^ [A: iS] :
( ( A = c0 )
| ? [B: iS] :
( c0
= ( cP @ B @ A ) ) ) )
= ( (=) @ iS @ c0 ) ) ) ),
inference(miniscope,[status(thm)],[3]) ).
thf(5,plain,
! [H: iS,G: iS > $o,F: iS,E: iS,D: iS,C: iS,B: iS,A: iS] :
( ( ( cP @ A @ B )
!= c0 )
& ( ( ( cP @ C @ E )
!= ( cP @ D @ F ) )
| ( C = D ) )
& ( ( ( cP @ C @ E )
!= ( cP @ D @ F ) )
| ( E = F ) )
& ( ~ ( G @ c0 )
| ( G @ ( sk1 @ G ) )
| ( G @ H ) )
& ( ~ ( G @ c0 )
| ( G @ ( sk2 @ G ) )
| ( G @ H ) )
& ( ~ ( G @ c0 )
| ~ ( G @ ( cP @ ( sk1 @ G ) @ ( sk2 @ G ) ) )
| ( G @ H ) )
& ( ( ( ^ [I: iS] :
( ( I = c0 )
| ? [J: iS] :
( c0
= ( cP @ I @ J ) ) ) )
!= ( (=) @ iS @ c0 ) )
| ( ( ^ [I: iS] :
( ( I = c0 )
| ? [J: iS] :
( c0
= ( cP @ J @ I ) ) ) )
!= ( (=) @ iS @ c0 ) ) ) ),
inference(cnf,[status(esa)],[4]) ).
thf(7,plain,
( ( ( ^ [A: iS] :
( ( A = c0 )
| ? [B: iS] :
( c0
= ( cP @ A @ B ) ) ) )
!= ( (=) @ iS @ c0 ) )
| ( ( ^ [A: iS] :
( ( A = c0 )
| ? [B: iS] :
( c0
= ( cP @ B @ A ) ) ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(27,plain,
( ( ( ^ [A: iS] :
( ( A = c0 )
| ? [B: iS] :
( c0
= ( cP @ A @ B ) ) ) )
!= ( (=) @ iS @ c0 ) )
| ( ( ^ [A: iS] :
( ( A = c0 )
| ? [B: iS] :
( c0
= ( cP @ B @ A ) ) ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(lifteq,[status(thm)],[7]) ).
thf(61,plain,
( ( ( ( sk5 = c0 )
| ? [A: iS] :
( c0
= ( cP @ sk5 @ A ) ) )
!= ( c0 = sk5 ) )
| ( ( ( sk6 = c0 )
| ? [A: iS] :
( c0
= ( cP @ A @ sk6 ) ) )
!= ( c0 = sk6 ) ) ),
inference(func_ext,[status(esa)],[27]) ).
thf(945,plain,
( ( sk5 = c0 )
| ? [A: iS] :
( c0
= ( cP @ sk5 @ A ) )
| ( c0 = sk5 )
| ( sk6 = c0 )
| ? [A: iS] :
( c0
= ( cP @ A @ sk6 ) )
| ( c0 = sk6 ) ),
inference(bool_ext,[status(thm)],[61]) ).
thf(1022,plain,
( ( sk5 = c0 )
| ( sk6 = c0 )
| ( sk5 = c0 )
| ? [A: iS] :
( c0
= ( cP @ sk5 @ A ) )
| ( sk6 = c0 )
| ? [A: iS] :
( c0
= ( cP @ A @ sk6 ) ) ),
inference(lifteq,[status(thm)],[945]) ).
thf(1133,plain,
( ( sk5 = c0 )
| ( sk6 = c0 )
| ( sk5 = c0 )
| ( c0
= ( cP @ sk5 @ sk41 ) )
| ( sk6 = c0 )
| ( c0
= ( cP @ sk42 @ sk6 ) ) ),
inference(cnf,[status(esa)],[1022]) ).
thf(1134,plain,
( ( sk5 = c0 )
| ( ( cP @ sk5 @ sk41 )
= c0 )
| ( sk6 = c0 )
| ( ( cP @ sk42 @ sk6 )
= c0 )
| ( sk5 = c0 )
| ( sk6 = c0 ) ),
inference(lifteq,[status(thm)],[1133]) ).
thf(1135,plain,
( ( sk5 = c0 )
| ( ( cP @ sk5 @ sk41 )
= c0 )
| ( sk6 = c0 )
| ( ( cP @ sk42 @ sk6 )
= c0 ) ),
inference(simp,[status(thm)],[1134]) ).
thf(8,plain,
! [B: iS,A: iS] :
( ( cP @ A @ B )
!= c0 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(32,plain,
! [B: iS,A: iS] :
( ( cP @ A @ B )
!= c0 ),
inference(lifteq,[status(thm)],[8]) ).
thf(1234,plain,
( ( sk5 = c0 )
| ( sk6 = c0 ) ),
inference(simplifyReflect,[status(thm)],[1135,32]) ).
thf(943,plain,
( ( sk5 = c0 )
| ? [A: iS] :
( c0
= ( cP @ sk5 @ A ) )
| ( c0 = sk5 )
| ~ ( ( sk6 = c0 )
| ? [A: iS] :
( c0
= ( cP @ A @ sk6 ) ) )
| ( c0 != sk6 ) ),
inference(bool_ext,[status(thm)],[61]) ).
thf(1028,plain,
( ( sk5 = c0 )
| ( sk6 != c0 )
| ( sk5 = c0 )
| ? [A: iS] :
( c0
= ( cP @ sk5 @ A ) )
| ~ ( ( sk6 = c0 )
| ? [A: iS] :
( c0
= ( cP @ A @ sk6 ) ) ) ),
inference(lifteq,[status(thm)],[943]) ).
thf(1095,plain,
! [A: iS] :
( ( ( sk5 = c0 )
| ( sk6 != c0 )
| ( sk5 = c0 )
| ( c0
= ( cP @ sk5 @ sk39 ) )
| ( sk6 != c0 ) )
& ( ( sk5 = c0 )
| ( sk6 != c0 )
| ( sk5 = c0 )
| ( c0
= ( cP @ sk5 @ sk39 ) )
| ( c0
!= ( cP @ A @ sk6 ) ) ) ),
inference(cnf,[status(esa)],[1028]) ).
thf(1096,plain,
( ( sk5 = c0 )
| ( sk6 != c0 )
| ( sk5 = c0 )
| ( c0
= ( cP @ sk5 @ sk39 ) )
| ( sk6 != c0 ) ),
inference(cnfConj,[status(thm)],[1095]) ).
thf(1098,plain,
( ( sk5 = c0 )
| ( ( cP @ sk5 @ sk39 )
= c0 )
| ( sk6 != c0 )
| ( sk5 = c0 )
| ( sk6 != c0 ) ),
inference(lifteq,[status(thm)],[1096]) ).
thf(1099,plain,
( ( sk5 = c0 )
| ( ( cP @ sk5 @ sk39 )
= c0 )
| ( sk6 != c0 ) ),
inference(simp,[status(thm)],[1098]) ).
thf(1244,plain,
( ( sk5 = c0 )
| ( sk6 != c0 ) ),
inference(simplifyReflect,[status(thm)],[1099,32]) ).
thf(1245,plain,
( ( sk5 = c0 )
| ( sk5 = c0 )
| ( c0 != c0 )
| ( sk6 != sk6 ) ),
inference(paramod_ordered,[status(thm)],[1234,1244]) ).
thf(1246,plain,
( ( sk5 = c0 )
| ( sk6 != sk6 ) ),
inference(simp,[status(thm)],[1245]) ).
thf(1247,plain,
sk5 = c0,
inference(pattern_uni,[status(thm)],[1246:[]]) ).
thf(1248,plain,
( ( ( ( c0 = c0 )
| ? [A: iS] :
( c0
= ( cP @ c0 @ A ) ) )
!= ( c0 = c0 ) )
| ( ( ( sk6 = c0 )
| ? [A: iS] :
( c0
= ( cP @ A @ sk6 ) ) )
!= ( c0 = sk6 ) ) ),
inference(rewrite,[status(thm)],[61,1247]) ).
thf(1249,plain,
( ( ( sk6 = c0 )
| ? [A: iS] :
( c0
= ( cP @ A @ sk6 ) ) )
!= ( c0 = sk6 ) ),
inference(simp,[status(thm)],[1248]) ).
thf(1255,plain,
( ( sk6 = c0 )
| ? [A: iS] :
( c0
= ( cP @ A @ sk6 ) )
| ( c0 = sk6 ) ),
inference(bool_ext,[status(thm)],[1249]) ).
thf(1296,plain,
( ( sk6 = c0 )
| ( sk6 = c0 )
| ? [A: iS] :
( c0
= ( cP @ A @ sk6 ) ) ),
inference(lifteq,[status(thm)],[1255]) ).
thf(1325,plain,
( ( sk6 = c0 )
| ( sk6 = c0 )
| ( c0
= ( cP @ sk44 @ sk6 ) ) ),
inference(cnf,[status(esa)],[1296]) ).
thf(1326,plain,
( ( sk6 = c0 )
| ( ( cP @ sk44 @ sk6 )
= c0 )
| ( sk6 = c0 ) ),
inference(lifteq,[status(thm)],[1325]) ).
thf(1327,plain,
( ( sk6 = c0 )
| ( ( cP @ sk44 @ sk6 )
= c0 ) ),
inference(simp,[status(thm)],[1326]) ).
thf(942,plain,
( ~ ( ( sk5 = c0 )
| ? [A: iS] :
( c0
= ( cP @ sk5 @ A ) ) )
| ( c0 != sk5 )
| ~ ( ( sk6 = c0 )
| ? [A: iS] :
( c0
= ( cP @ A @ sk6 ) ) )
| ( c0 != sk6 ) ),
inference(bool_ext,[status(thm)],[61]) ).
thf(1024,plain,
( ( sk5 != c0 )
| ( sk6 != c0 )
| ~ ( ( sk5 = c0 )
| ? [A: iS] :
( c0
= ( cP @ sk5 @ A ) ) )
| ~ ( ( sk6 = c0 )
| ? [A: iS] :
( c0
= ( cP @ A @ sk6 ) ) ) ),
inference(lifteq,[status(thm)],[942]) ).
thf(1082,plain,
! [B: iS,A: iS] :
( ( ( sk5 != c0 )
| ( sk6 != c0 )
| ( sk5 != c0 )
| ( sk6 != c0 ) )
& ( ( sk5 != c0 )
| ( sk6 != c0 )
| ( sk5 != c0 )
| ( c0
!= ( cP @ B @ sk6 ) ) )
& ( ( sk5 != c0 )
| ( sk6 != c0 )
| ( c0
!= ( cP @ sk5 @ A ) )
| ( sk6 != c0 ) )
& ( ( sk5 != c0 )
| ( sk6 != c0 )
| ( c0
!= ( cP @ sk5 @ A ) )
| ( c0
!= ( cP @ B @ sk6 ) ) ) ),
inference(cnf,[status(esa)],[1024]) ).
thf(1083,plain,
( ( sk5 != c0 )
| ( sk6 != c0 )
| ( sk5 != c0 )
| ( sk6 != c0 ) ),
inference(cnfConj,[status(thm)],[1082]) ).
thf(1087,plain,
( ( sk5 != c0 )
| ( sk6 != c0 )
| ( sk5 != c0 )
| ( sk6 != c0 ) ),
inference(lifteq,[status(thm)],[1083]) ).
thf(1088,plain,
( ( sk5 != c0 )
| ( sk6 != c0 ) ),
inference(simp,[status(thm)],[1087]) ).
thf(1250,plain,
( ( c0 != c0 )
| ( sk6 != c0 ) ),
inference(rewrite,[status(thm)],[1088,1247]) ).
thf(1251,plain,
sk6 != c0,
inference(simp,[status(thm)],[1250]) ).
thf(1343,plain,
$false,
inference(simplifyReflect,[status(thm)],[1327,32,1251]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV214^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.11/0.21 % Computer : n002.cluster.edu
% 0.11/0.21 % Model : x86_64 x86_64
% 0.11/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.21 % Memory : 8046.5625MB
% 0.11/0.21 % OS : Linux 6.8.0-71-generic
% 0.11/0.21 % CPULimit : 300
% 0.11/0.21 % WCLimit : 300
% 0.11/0.21 % DateTime : Tue Sep 29 15:24:38 UTC 2026
% 0.11/0.22 % CPUTime :
% 0.11/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.66/0.52 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.91/0.62 % [INFO] Parsing done (97ms).
% 0.91/0.63 % [INFO] Running in sequential loop mode.
% 1.37/0.83 % [INFO] eprover registered as external prover.
% 1.37/0.83 % [INFO] Scanning for conjecture ...
% 1.37/0.89 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 1.62/0.91 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 1.62/0.91 % [INFO] Problem is higher-order (TPTP THF).
% 1.62/0.91 % [INFO] Type checking passed.
% 1.62/0.91 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 13.64/3.35 % [INFO] Killing All external provers ...
% 13.64/3.36 % Time passed: 3055ms (effective reasoning time: 2719ms)
% 13.64/3.36 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 13.64/3.36 % Axioms used in derivation (0):
% 13.64/3.36 % No. of inferences in proof: 42
% 13.64/3.36 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 3055 ms resp. 2719 ms w/o parsing
% 12.08/3.44 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 12.08/3.44 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------