%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : PUZ092^5 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Feb 25 09:28:27 AM UTC 2026
% Result : Theorem 1.53s 1.27s
% Output : Refutation 1.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : PUZ092^5 : TPTP v9.2.1. Released v4.0.0.
% 0.13/0.12 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.17/0.33 % Computer : n015.cluster.edu
% 0.17/0.33 % Model : x86_64 x86_64
% 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.33 % Memory : 8042.1875MB
% 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.33 % CPULimit : 300
% 0.17/0.33 % WCLimit : 300
% 0.17/0.33 % DateTime : Tue Feb 24 11:32:31 EST 2026
% 0.17/0.33 % CPUTime :
% 0.17/0.33 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.20/0.45 ---- Original DTF file ---
% 0.20/0.45 thf(spec,logic,$$dhol).
% 0.20/0.45 %------------------------------------------------------------------------------
% 0.20/0.45 % File : PUZ092^5 : TPTP v9.2.1. Released v4.0.0.
% 0.20/0.45 % Domain : Puzzles
% 0.20/0.45 % Problem : TPS problem from BASIC-HO-EQ-THMS
% 0.20/0.45 % Version : Especial.
% 0.20/0.45 % English :
% 0.20/0.45
% 0.20/0.45 % Refs : [Bro09] Brown (2009), Email to Geoff Sutcliffe
% 0.20/0.45 % Source : [Bro09]
% 0.20/0.45 % Names : tps_1179 [Bro09]
% 0.20/0.45
% 0.20/0.45 % Status : Theorem
% 0.20/0.45 % Rating : 0.00 v9.0.0, 0.10 v8.2.0, 0.08 v8.1.0, 0.09 v7.5.0, 0.14 v7.4.0, 0.22 v7.2.0, 0.12 v7.1.0, 0.25 v7.0.0, 0.29 v6.4.0, 0.33 v6.3.0, 0.40 v6.2.0, 0.29 v6.1.0, 0.43 v5.5.0, 0.33 v5.4.0, 0.40 v5.1.0, 0.60 v5.0.0, 0.40 v4.1.0, 0.67 v4.0.0
% 0.20/0.45 % Syntax : Number of formulae : 1 ( 0 unt; 0 typ; 0 def)
% 0.20/0.45 % Number of atoms : 32 ( 32 equ; 0 cnn)
% 0.20/0.45 % Maximal formula atoms : 32 ( 32 avg)
% 0.20/0.45 % Number of connectives : 43 ( 12 ~; 5 |; 19 &; 0 @)
% 0.20/0.45 % ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% 0.20/0.45 % Maximal formula depth : 24 ( 24 avg)
% 0.20/0.45 % Number of types : 1 ( 0 usr)
% 0.20/0.45 % Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% 0.20/0.45 % Number of symbols : 1 ( 0 usr; 0 con; 2-2 aty)
% 0.20/0.45 % Number of variables : 12 ( 0 ^; 12 !; 0 ?; 12 :)
% 0.20/0.45 % SPC : TH0_THM_EQU_NAR
% 0.20/0.45
% 0.20/0.45 % Comments : This problem is from the TPS library. Copyright (c) 2009 The TPS
% 0.20/0.45 % project in the Department of Mathematical Sciences at Carnegie
% 0.20/0.45 % Mellon University. Distributed under the Creative Commons copyleft
% 0.20/0.45 % license: http://creativecommons.org/licenses/by-sa/3.0/
% 0.20/0.45 %------------------------------------------------------------------------------
% 0.20/0.45 thf(cSIXFRIENDS_EASIER,conjecture,
% 0.20/0.45 ! [ACRES: $i,MRSACRES: $i,BARRY: $i,MRSBARRY: $i,COLE: $i,MRSCOLE: $i,DIX: $i,MRSDIX: $i,EDEN: $i,MRSEDEN: $i,HALL: $i,MRSHALL: $i] :
% 0.20/0.45 ( ( ( ( ( ACRES = MRSACRES )
% 0.20/0.45 & ( BARRY = MRSBARRY )
% 0.20/0.45 & ( EDEN = MRSHALL ) )
% 0.20/0.45 => ( COLE = MRSDIX ) )
% 0.20/0.45 & ( ( ( ACRES = MRSACRES )
% 0.20/0.45 & ( HALL = MRSHALL )
% 0.20/0.45 & ( BARRY = MRSCOLE ) )
% 0.20/0.45 => ( DIX != MRSEDEN ) )
% 0.20/0.45 & ( ( ( COLE = MRSCOLE )
% 0.20/0.45 & ( DIX = MRSDIX )
% 0.20/0.45 & ( DIX = COLE )
% 0.20/0.45 & ( ACRES != MRSBARRY ) )
% 0.20/0.45 => ( EDEN != MRSHALL ) )
% 0.20/0.45 & ( ( ( ACRES = MRSACRES )
% 0.20/0.45 & ( DIX = MRSDIX )
% 0.20/0.45 & ( BARRY != MRSCOLE ) )
% 0.20/0.45 => ( EDEN = MRSHALL ) )
% 0.20/0.45 & ( ( ( EDEN = MRSEDEN )
% 0.20/0.45 & ( HALL = MRSHALL )
% 0.20/0.45 & ( COLE = MRSDIX ) )
% 0.20/0.45 => ( ACRES != MRSBARRY ) )
% 0.20/0.45 & ( ( ( BARRY = MRSBARRY )
% 0.20/0.45 & ( COLE = MRSCOLE )
% 0.20/0.45 & ( COLE = BARRY )
% 0.20/0.45 & ( EDEN != MRSHALL ) )
% 0.20/0.45 => ( DIX = MRSEDEN ) ) )
% 0.20/0.45 => ( ( ACRES != MRSACRES )
% 0.20/0.45 | ( BARRY != MRSBARRY )
% 0.20/0.45 | ( COLE != MRSCOLE )
% 0.20/0.45 | ( DIX != MRSDIX )
% 0.20/0.45 | ( EDEN != MRSEDEN )
% 0.20/0.45 | ( HALL != MRSHALL ) ) ) ).
% 0.20/0.45
% 0.20/0.45 %------------------------------------------------------------------------------
% 0.20/0.45 ------------------------
% 1.53/1.24 ---- Embedded in THF ---
% 1.53/1.24 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.53/1.24 %%% Generated on Tue Feb 24 11:32:32 EST 2026
% 1.53/1.24 %%% using '$$dhol' embedding, version 1.3.0.
% 1.53/1.24 %%% Logic specification used:
% 1.53/1.24 %%% thf(spec, logic, $$dhol).
% 1.53/1.24
% 1.53/1.24 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.cdT8uQjeHW/DTF2DTF7556.p
% 1.53/1.24 thf(cSIXFRIENDS_EASIER, conjecture, (! [ACRES:$i,MRSACRES:$i,BARRY:$i,MRSBARRY:$i,COLE:$i,MRSCOLE:$i,DIX:$i,MRSDIX:$i,EDEN:$i,MRSEDEN:$i,HALL:$i,MRSHALL:$i]: ((((((ACRES = MRSACRES) & ((BARRY = MRSBARRY) & (EDEN = MRSHALL))) => (COLE = MRSDIX)) & ((((ACRES = MRSACRES) & ((HALL = MRSHALL) & (BARRY = MRSCOLE))) => (DIX != MRSEDEN)) & ((((COLE = MRSCOLE) & ((DIX = MRSDIX) & ((DIX = COLE) & (ACRES != MRSBARRY)))) => (EDEN != MRSHALL)) & ((((ACRES = MRSACRES) & ((DIX = MRSDIX) & (BARRY != MRSCOLE))) => (EDEN = MRSHALL)) & ((((EDEN = MRSEDEN) & ((HALL = MRSHALL) & (COLE = MRSDIX))) => (ACRES != MRSBARRY)) & (((BARRY = MRSBARRY) & ((COLE = MRSCOLE) & ((COLE = BARRY) & (EDEN != MRSHALL)))) => (DIX = MRSEDEN))))))) => ((ACRES != MRSACRES) | ((BARRY != MRSBARRY) | ((COLE != MRSCOLE) | ((DIX != MRSDIX) | ((EDEN != MRSEDEN) | (HALL != MRSHALL)))))))))).
% 1.53/1.24 % SZS output end ListOfTHF for /export/starexec/sandbox2/tmp/tmp.cdT8uQjeHW/DTF2DTF7556.p
% 1.53/1.24 ------------------------
% 1.53/1.25 ---- Cleaned THF ---
% 1.53/1.25 thf(cSIXFRIENDS_EASIER,conjecture,
% 1.53/1.25 ! [ACRES: $i,MRSACRES: $i,BARRY: $i,MRSBARRY: $i,COLE: $i,MRSCOLE: $i,DIX: $i,MRSDIX: $i,EDEN: $i,MRSEDEN: $i,HALL: $i,MRSHALL: $i] :
% 1.53/1.25 ( ( ( ( ( ACRES = MRSACRES )
% 1.53/1.25 & ( BARRY = MRSBARRY )
% 1.53/1.25 & ( EDEN = MRSHALL ) )
% 1.53/1.25 => ( COLE = MRSDIX ) )
% 1.53/1.25 & ( ( ( ACRES = MRSACRES )
% 1.53/1.25 & ( HALL = MRSHALL )
% 1.53/1.25 & ( BARRY = MRSCOLE ) )
% 1.53/1.25 => ( DIX != MRSEDEN ) )
% 1.53/1.25 & ( ( ( COLE = MRSCOLE )
% 1.53/1.25 & ( DIX = MRSDIX )
% 1.53/1.25 & ( DIX = COLE )
% 1.53/1.25 & ( ACRES != MRSBARRY ) )
% 1.53/1.25 => ( EDEN != MRSHALL ) )
% 1.53/1.25 & ( ( ( ACRES = MRSACRES )
% 1.53/1.25 & ( DIX = MRSDIX )
% 1.53/1.25 & ( BARRY != MRSCOLE ) )
% 1.53/1.25 => ( EDEN = MRSHALL ) )
% 1.53/1.25 & ( ( ( EDEN = MRSEDEN )
% 1.53/1.25 & ( HALL = MRSHALL )
% 1.53/1.25 & ( COLE = MRSDIX ) )
% 1.53/1.25 => ( ACRES != MRSBARRY ) )
% 1.53/1.25 & ( ( ( BARRY = MRSBARRY )
% 1.53/1.25 & ( COLE = MRSCOLE )
% 1.53/1.25 & ( COLE = BARRY )
% 1.53/1.25 & ( EDEN != MRSHALL ) )
% 1.53/1.25 => ( DIX = MRSEDEN ) ) )
% 1.53/1.25 => ( ( ACRES != MRSACRES )
% 1.53/1.25 | ( BARRY != MRSBARRY )
% 1.53/1.25 | ( COLE != MRSCOLE )
% 1.53/1.25 | ( DIX != MRSDIX )
% 1.53/1.25 | ( EDEN != MRSEDEN )
% 1.53/1.25 | ( HALL != MRSHALL ) ) ) ).
% 1.53/1.25 ------------------------
% 1.53/1.27 % (7660)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_7556 for (3000ds/183Mi)
% 1.53/1.27 % (7665)lrs+1002_1:1_au=on:bd=off:e2e=on:sd=2:sos=on:ss=axioms:i=275:si=on:rtra=on_0 on DTF2THF_7556 for (3000ds/275Mi)
% 1.53/1.27 % (7660)First to succeed.
% 1.53/1.27 % (7665)Also succeeded, but the first one will report.
% 1.53/1.27 % (7660)Refutation found. Thanks to Tanya!
% 1.53/1.27 % SZS status Theorem for DTF2THF_7556
% 1.53/1.27 % SZS output start Proof for DTF2THF_7556
% 1.53/1.27 fof(f59,plain,(
% 1.53/1.27 $false),
% 1.53/1.27 inference(avatar_sat_refutation,[status(thm)],[f45,f54,f55,f56,f57,f58])).
% 1.53/1.27 fof(f58,plain,(
% 1.53/1.27 spl12_3 | spl12_1),
% 1.53/1.27 inference(avatar_split_clause,[status(thm)],[f27,f34,f42])).
% 1.53/1.27 fof(f42,definition,(
% 1.53/1.27 spl12_3 <=> sK6 = sK11),
% 1.53/1.27 introduced(definition,[new_symbols(naming,[spl12_3])],[avatar_definition])).
% 1.53/1.27 fof(f34,definition,(
% 1.53/1.27 spl12_1 <=> sK3 = sK10),
% 1.53/1.27 introduced(definition,[new_symbols(naming,[spl12_1])],[avatar_definition])).
% 1.53/1.27 fof(f27,plain,(
% 1.53/1.27 sK3 = sK10 | sK6 = sK11),
% 1.53/1.27 inference(trivial_inequality_removal,[status(thm)],[f21])).
% 1.53/1.27 fof(f21,plain,(
% 1.53/1.27 sK6 = sK11 | sK3 = sK10 | sK4 != sK4 | sK9 != sK9),
% 1.53/1.27 inference(definition_unfolding,[status(thm)],[f20,f13,f18,f11])).
% 1.53/1.27 fof(f11,plain,(
% 1.53/1.27 sK8 = sK4),
% 1.53/1.27 inference(cnf_transformation,[status(thm)],[f8])).
% 1.53/1.27 fof(f8,plain,(
% 1.53/1.27 (sK6 = sK11 | sK5 = sK10 | sK7 != sK9 | sK8 != sK4) & (sK7 != sK2 | sK4 != sK0 | sK1 != sK10 | sK5 != sK3) & sK7 = sK9 & sK0 = sK11 & (sK0 != sK11 | sK8 != sK4 | sK7 = sK2 | sK5 != sK10) & sK2 = sK6 & sK1 = sK10 & sK5 = sK3 & (sK9 = sK3 | sK2 != sK11 | sK2 != sK6 | sK0 != sK11 | sK5 = sK10) & sK8 = sK4 & (sK9 != sK3 | sK1 != sK10 | sK8 != sK4 | sK6 != sK11) & (sK2 != sK6 | sK7 != sK9 | sK4 = sK0 | sK2 != sK9 | sK5 != sK10)),
% 1.53/1.27 inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11])],[f6,f7])).
% 1.53/1.27 fof(f7,plain,(
% 1.53/1.27 ? [X0 : $i,X1 : $i,X2 : $i,X3 : $i,X4 : $i,X5 : $i,X6 : $i,X7 : $i,X8 : $i,X9 : $i,X10 : $i,X11 : $i] : ((X6 = X11 | X5 = X10 | X7 != X9 | X4 != X8) & (X2 != X7 | X0 != X4 | X1 != X10 | X3 != X5) & X7 = X9 & X0 = X11 & (X0 != X11 | X4 != X8 | X2 = X7 | X5 != X10) & X2 = X6 & X1 = X10 & X3 = X5 & (X3 = X9 | X2 != X11 | X2 != X6 | X0 != X11 | X5 = X10) & X4 = X8 & (X3 != X9 | X1 != X10 | X4 != X8 | X6 != X11) & (X2 != X6 | X7 != X9 | X0 = X4 | X2 != X9 | X5 != X10)) => ((sK6 = sK11 | sK5 = sK10 | sK7 != sK9 | sK8 != sK4) & (sK7 != sK2 | sK4 != sK0 | sK1 != sK10 | sK5 != sK3) & sK7 = sK9 & sK0 = sK11 & (sK0 != sK11 | sK8 != sK4 | sK7 = sK2 | sK5 != sK10) & sK2 = sK6 & sK1 = sK10 & sK5 = sK3 & (sK9 = sK3 | sK2 != sK11 | sK2 != sK6 | sK0 != sK11 | sK5 = sK10) & sK8 = sK4 & (sK9 != sK3 | sK1 != sK10 | sK8 != sK4 | sK6 != sK11) & (sK2 != sK6 | sK7 != sK9 | sK4 = sK0 | sK2 != sK9 | sK5 != sK10))),
% 1.53/1.27 introduced(definition,[],[choice_axiom])).
% 1.53/1.27 fof(f6,plain,(
% 1.53/1.27 ? [X0 : $i,X1 : $i,X2 : $i,X3 : $i,X4 : $i,X5 : $i,X6 : $i,X7 : $i,X8 : $i,X9 : $i,X10 : $i,X11 : $i] : ((X6 = X11 | X5 = X10 | X7 != X9 | X4 != X8) & (X2 != X7 | X0 != X4 | X1 != X10 | X3 != X5) & X7 = X9 & X0 = X11 & (X0 != X11 | X4 != X8 | X2 = X7 | X5 != X10) & X2 = X6 & X1 = X10 & X3 = X5 & (X3 = X9 | X2 != X11 | X2 != X6 | X0 != X11 | X5 = X10) & X4 = X8 & (X3 != X9 | X1 != X10 | X4 != X8 | X6 != X11) & (X2 != X6 | X7 != X9 | X0 = X4 | X2 != X9 | X5 != X10))),
% 1.53/1.27 inference(rectify,[status(thm)],[f5])).
% 1.53/1.27 fof(f5,plain,(
% 1.53/1.27 ? [X6 : $i,X8 : $i,X9 : $i,X3 : $i,X2 : $i,X10 : $i,X7 : $i,X4 : $i,X0 : $i,X1 : $i,X5 : $i,X11 : $i] : ((X7 = X11 | X5 = X10 | X1 != X4 | X0 != X2) & (X4 != X9 | X2 != X6 | X5 != X8 | X3 != X10) & X1 = X4 & X6 = X11 & (X6 != X11 | X0 != X2 | X4 = X9 | X5 != X10) & X7 = X9 & X5 = X8 & X3 = X10 & (X1 = X3 | X9 != X11 | X7 != X9 | X6 != X11 | X5 = X10) & X0 = X2 & (X1 != X3 | X5 != X8 | X0 != X2 | X7 != X11) & (X7 != X9 | X1 != X4 | X2 = X6 | X1 != X9 | X5 != X10))),
% 1.53/1.27 inference(flattening,[status(thm)],[f4])).
% 1.53/1.27 fof(f4,plain,(
% 1.53/1.27 ? [X8 : $i,X11 : $i,X0 : $i,X7 : $i,X10 : $i,X6 : $i,X2 : $i,X9 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((X7 = X9 & X1 = X4 & X0 = X2 & X6 = X11 & X3 = X10 & X5 = X8) & ((X5 != X10 | (X2 = X6 | X7 != X9 | X1 != X4 | X1 != X9)) & (X2 != X6 | (X3 != X10 | X5 != X8 | X4 != X9)) & (X1 = X3 | (X6 != X11 | X5 = X10 | X7 != X9 | X9 != X11)) & (X4 = X9 | (X5 != X10 | X6 != X11 | X0 != X2)) & (X5 = X10 | (X0 != X2 | X1 != X4 | X7 = X11)) & (X1 != X3 | (X0 != X2 | X7 != X11 | X5 != X8))))),
% 1.53/1.27 inference(ennf_transformation,[status(thm)],[f3])).
% 1.53/1.27 fof(f3,plain,(
% 1.53/1.27 ~! [X8 : $i,X11 : $i,X0 : $i,X7 : $i,X10 : $i,X6 : $i,X2 : $i,X9 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((X2 != X6 & X7 = X9 & X1 = X4 & X1 = X9) => X5 != X10) & ((X3 = X10 & X5 = X8 & X4 = X9) => X2 != X6) & ((X6 = X11 & X5 != X10 & X7 = X9 & X9 = X11) => X1 = X3) & ((X5 = X10 & X6 = X11 & X0 = X2) => X4 = X9) & ((X0 = X2 & X1 = X4 & X7 != X11) => X5 = X10) & ((X0 = X2 & X7 = X11 & X5 = X8) => X1 != X3)) => (X7 != X9 | X1 != X4 | X0 != X2 | X6 != X11 | X3 != X10 | X5 != X8))),
% 1.53/1.27 inference(rectify,[status(thm)],[f2])).
% 1.53/1.27 fof(f2,negated_conjecture,(
% 1.53/1.27 ~! [X1 : $i,X6 : $i,X0 : $i,X9 : $i,X7 : $i,X11 : $i,X3 : $i,X5 : $i,X10 : $i,X4 : $i,X8 : $i,X2 : $i] : ((((X10 = X11 & X0 = X1 & X2 = X5) => X6 != X9) & ((X2 = X4 & X4 = X5 & X8 != X11 & X2 = X3) => X6 = X9) & ((X6 = X7 & X4 = X5 & X4 = X6 & X0 != X3) => X8 != X11) & ((X2 != X5 & X6 = X7 & X0 = X1) => X8 = X11) & ((X8 = X11 & X2 = X3 & X0 = X1) => X4 = X7) & ((X4 = X7 & X8 = X9 & X10 = X11) => X0 != X3)) => (X4 != X5 | X6 != X7 | X8 != X9 | X0 != X1 | X10 != X11 | X2 != X3))),
% 1.53/1.27 inference(negated_conjecture,[status(cth)],[f1])).
% 1.53/1.27 fof(f1,conjecture,(
% 1.53/1.27 ! [X1 : $i,X6 : $i,X0 : $i,X9 : $i,X7 : $i,X11 : $i,X3 : $i,X5 : $i,X10 : $i,X4 : $i,X8 : $i,X2 : $i] : ((((X10 = X11 & X0 = X1 & X2 = X5) => X6 != X9) & ((X2 = X4 & X4 = X5 & X8 != X11 & X2 = X3) => X6 = X9) & ((X6 = X7 & X4 = X5 & X4 = X6 & X0 != X3) => X8 != X11) & ((X2 != X5 & X6 = X7 & X0 = X1) => X8 = X11) & ((X8 = X11 & X2 = X3 & X0 = X1) => X4 = X7) & ((X4 = X7 & X8 = X9 & X10 = X11) => X0 != X3)) => (X4 != X5 | X6 != X7 | X8 != X9 | X0 != X1 | X10 != X11 | X2 != X3))),
% 1.53/1.27 file('/export/starexec/sandbox2/tmp/tmp.cdT8uQjeHW/DTF2THF_7556.p',cSIXFRIENDS_EASIER)).
% 1.53/1.27 fof(f18,plain,(
% 1.53/1.27 sK7 = sK9),
% 1.53/1.27 inference(cnf_transformation,[status(thm)],[f8])).
% 1.53/1.27 fof(f13,plain,(
% 1.53/1.27 sK5 = sK3),
% 1.53/1.27 inference(cnf_transformation,[status(thm)],[f8])).
% 1.53/1.27 fof(f20,plain,(
% 1.53/1.27 sK6 = sK11 | sK5 = sK10 | sK7 != sK9 | sK8 != sK4),
% 1.53/1.27 inference(cnf_transformation,[status(thm)],[f8])).
% 1.53/1.27 fof(f57,plain,(
% 1.53/1.27 ~spl12_2 | ~spl12_3),
% 1.53/1.27 inference(avatar_split_clause,[status(thm)],[f28,f42,f38])).
% 1.53/1.27 fof(f38,definition,(
% 1.53/1.27 spl12_2 <=> sK9 = sK3),
% 1.53/1.27 introduced(definition,[new_symbols(naming,[spl12_2])],[avatar_definition])).
% 1.53/1.27 fof(f28,plain,(
% 1.53/1.27 sK9 != sK3 | sK6 != sK11),
% 1.53/1.27 inference(trivial_inequality_removal,[status(thm)],[f25])).
% 1.53/1.27 fof(f25,plain,(
% 1.53/1.27 sK10 != sK10 | sK4 != sK4 | sK9 != sK3 | sK6 != sK11),
% 1.53/1.27 inference(definition_unfolding,[status(thm)],[f10,f14,f11])).
% 1.53/1.27 fof(f14,plain,(
% 1.53/1.27 sK1 = sK10),
% 1.53/1.27 inference(cnf_transformation,[status(thm)],[f8])).
% 1.53/1.27 fof(f10,plain,(
% 1.53/1.27 sK9 != sK3 | sK1 != sK10 | sK8 != sK4 | sK6 != sK11),
% 1.53/1.27 inference(cnf_transformation,[status(thm)],[f8])).
% 1.53/1.27 fof(f56,plain,(
% 1.53/1.27 spl12_4 | ~spl12_1),
% 1.53/1.27 inference(avatar_split_clause,[status(thm)],[f29,f34,f47])).
% 1.53/1.27 fof(f47,definition,(
% 1.53/1.27 spl12_4 <=> sK9 = sK6),
% 1.53/1.27 introduced(definition,[new_symbols(naming,[spl12_4])],[avatar_definition])).
% 1.53/1.27 fof(f29,plain,(
% 1.53/1.27 sK9 = sK6 | sK3 != sK10),
% 1.53/1.27 inference(trivial_inequality_removal,[status(thm)],[f23])).
% 1.53/1.27 fof(f23,plain,(
% 1.53/1.27 sK11 != sK11 | sK3 != sK10 | sK4 != sK4 | sK9 = sK6),
% 1.53/1.27 inference(definition_unfolding,[status(thm)],[f16,f17,f11,f18,f15,f13])).
% 1.53/1.27 fof(f15,plain,(
% 1.53/1.27 sK2 = sK6),
% 1.53/1.27 inference(cnf_transformation,[status(thm)],[f8])).
% 1.53/1.27 fof(f17,plain,(
% 1.53/1.27 sK0 = sK11),
% 1.53/1.27 inference(cnf_transformation,[status(thm)],[f8])).
% 1.53/1.27 fof(f16,plain,(
% 1.53/1.27 sK0 != sK11 | sK8 != sK4 | sK7 = sK2 | sK5 != sK10),
% 1.53/1.27 inference(cnf_transformation,[status(thm)],[f8])).
% 1.53/1.27 fof(f55,plain,(
% 1.53/1.27 ~spl12_4 | ~spl12_5),
% 1.53/1.27 inference(avatar_split_clause,[status(thm)],[f30,f51,f47])).
% 1.53/1.27 fof(f51,definition,(
% 1.53/1.27 spl12_5 <=> sK4 = sK11),
% 1.53/1.27 introduced(definition,[new_symbols(naming,[spl12_5])],[avatar_definition])).
% 1.53/1.27 fof(f30,plain,(
% 1.53/1.27 sK4 != sK11 | sK9 != sK6),
% 1.53/1.27 inference(trivial_inequality_removal,[status(thm)],[f22])).
% 1.53/1.27 fof(f22,plain,(
% 1.53/1.27 sK9 != sK6 | sK4 != sK11 | sK3 != sK3 | sK10 != sK10),
% 1.53/1.27 inference(definition_unfolding,[status(thm)],[f19,f18,f15,f17,f14,f13])).
% 1.53/1.27 fof(f19,plain,(
% 1.53/1.27 sK7 != sK2 | sK4 != sK0 | sK1 != sK10 | sK5 != sK3),
% 1.53/1.27 inference(cnf_transformation,[status(thm)],[f8])).
% 1.53/1.27 fof(f54,plain,(
% 1.53/1.27 ~spl12_4 | ~spl12_1 | spl12_5),
% 1.53/1.27 inference(avatar_split_clause,[status(thm)],[f31,f51,f34,f47])).
% 1.53/1.27 fof(f31,plain,(
% 1.53/1.27 sK4 = sK11 | sK3 != sK10 | sK9 != sK6),
% 1.53/1.27 inference(trivial_inequality_removal,[status(thm)],[f26])).
% 1.53/1.27 fof(f26,plain,(
% 1.53/1.27 sK9 != sK6 | sK9 != sK9 | sK6 != sK6 | sK3 != sK10 | sK4 = sK11),
% 1.53/1.27 inference(definition_unfolding,[status(thm)],[f9,f15,f18,f17,f15,f13])).
% 1.53/1.27 fof(f9,plain,(
% 1.53/1.27 sK2 != sK6 | sK7 != sK9 | sK4 = sK0 | sK2 != sK9 | sK5 != sK10),
% 1.53/1.27 inference(cnf_transformation,[status(thm)],[f8])).
% 1.53/1.27 fof(f45,plain,(
% 1.53/1.27 spl12_1 | spl12_2 | ~spl12_3),
% 1.53/1.27 inference(avatar_split_clause,[status(thm)],[f32,f42,f38,f34])).
% 1.53/1.27 fof(f32,plain,(
% 1.53/1.27 sK9 = sK3 | sK3 = sK10 | sK6 != sK11),
% 1.53/1.27 inference(trivial_inequality_removal,[status(thm)],[f24])).
% 1.53/1.27 fof(f24,plain,(
% 1.53/1.27 sK6 != sK6 | sK6 != sK11 | sK3 = sK10 | sK11 != sK11 | sK9 = sK3),
% 1.53/1.27 inference(definition_unfolding,[status(thm)],[f12,f15,f15,f17,f13])).
% 1.53/1.27 fof(f12,plain,(
% 1.53/1.27 sK9 = sK3 | sK2 != sK11 | sK2 != sK6 | sK0 != sK11 | sK5 = sK10),
% 1.53/1.27 inference(cnf_transformation,[status(thm)],[f8])).
% 1.53/1.27 % SZS output end Proof for DTF2THF_7556
% 1.53/1.27 % (7660)------------------------------
% 1.53/1.27 % (7660)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.53/1.27 % (7660)Termination reason: Refutation
% 1.53/1.27
% 1.53/1.27 % (7660)Memory used [KB]: 5500
% 1.53/1.27 % (7660)Time elapsed: 0.003 s
% 1.53/1.27 % (7660)Instructions burned: 1 (million)
% 1.53/1.27 % (7660)------------------------------
% 1.53/1.27 % (7660)------------------------------
% 1.53/1.27 % (7655)Success in time 0.002 s
%------------------------------------------------------------------------------