%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN987^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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 : Wed Sep 30 08:41:45 AM UTC 2026
% Result : CounterSatisfiable 0.20s 0.30s
% Output : Saturation 0.20s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u96,negated_conjecture,
sK0 = $false ).
cnf(u170,negated_conjecture,
( X1 != X2
| $true = X1
| $false = X2
| X0 = X2 ) ).
cnf(u10,axiom,
( $true = X1
| X0 = X1
| $true = X0 ) ).
cnf(u20,negated_conjecture,
( sK0 = X0
| $true = X0 ) ).
cnf(u27,axiom,
( X0 != X1
| X1 = X2
| $true = X2
| $true = X0 ) ).
cnf(u133,negated_conjecture,
( X0 = X1
| $true = X1
| $false = X2
| X0 = X2 ) ).
cnf(u14,axiom,
( $false != X0
| X0 = X1
| $true = X1 ) ).
cnf(u176,negated_conjecture,
( X0 != X1
| $true = X0
| $false = X1 ) ).
cnf(u132,negated_conjecture,
( X0 != X1
| X1 = X2
| $true = X2
| $false = X3
| X0 = X3 ) ).
cnf(u9,axiom,
( $false = X0
| $true = X0 ) ).
cnf(u138,negated_conjecture,
( $true != X0
| $false = X1
| X0 = X1 ) ).
cnf(u7,negated_conjecture,
$true != sK0 ).
cnf(u55,negated_conjecture,
( sK0 = X2
| X1 = X2
| X0 = X1
| X0 = X2 ) ).
cnf(u31,axiom,
( X0 = X5
| X2 = X3
| X3 = X4
| X1 = X4
| X2 = X4
| X0 = X1
| $true = X5 ) ).
cnf(u33,axiom,
( $false != X0
| X1 = X2
| X2 = X3
| X0 = X3
| X1 = X3 ) ).
cnf(u76,negated_conjecture,
( X0 = X2
| X1 = X2
| X0 = X1 ) ).
cnf(u50,axiom,
( $true != X1
| X0 = X2
| X1 = X2
| X0 = X1 ) ).
cnf(u30,axiom,
( X5 = X7
| X2 = X3
| X3 = X4
| X1 = X4
| X2 = X4
| X5 = X6
| X6 = X7
| X0 = X7
| X0 = X1 ) ).
cnf(u13,axiom,
( $true = X3
| X1 = X2
| X0 = X2
| X0 = X3
| X0 = X1 ) ).
cnf(u32,axiom,
( X4 = X5
| X1 = X2
| X0 = X2
| X3 = X4
| X0 = X1
| X0 = X5
| X3 = X5 ) ).
cnf(u8,axiom,
$true != $false ).
cnf(u74,negated_conjecture,
( X0 = X1
| sK0 = X1
| sK0 = X0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN987^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n005.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 16:19:31 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.30 % (1865762)Detected formulas, will run a generic FOF schedule.
% 0.20/0.30 % (1865772)ott+1011_2_sil=4000:lsd=20:rnwc=on:rp=on:sac=on:newcnf=on:random_seed=512426655:i=132:kws=arity:er=filter_2999 on theBenchmark for (2999ds/132Mi)
% 0.20/0.30 % (1865772)Refutation not found, incomplete strategy
% 0.20/0.30 % (1865772)------------------------------
% 0.20/0.30 % (1865772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.30 % (1865772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.30 % (1865772)CaDiCaL version: 2.1.3
% 0.20/0.30 % (1865772)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.30 % (1865772)Time elapsed: 0.0000 s
% 0.20/0.30 % (1865772)Peak memory usage: 11 MB
% 0.20/0.30 % (1865772)------------------------------
% 0.20/0.30 % (1865772)------------------------------
% 0.20/0.30 % (1865769)lrs+10_1_sp=unary_first:urr=on:s2agt=32:random_seed=1422622737:s2a=on:i=272356:sd=1:bd=all:ss=included_2999 on theBenchmark for (2999ds/272356Mi)
% 0.20/0.30 % (1865767)lrs+1011_1_sp=occurrence:random_seed=581771271:st=6:sd=4:ss=included_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.30 % (1865768)dis+1010_16_tgt=full:drc=ordering:sp=reverse_frequency:nwc=1:random_seed=3797718394:i=261632:kws=inv_arity_squared:ins=1:av=off:fsd=on_2999 on theBenchmark for (2999ds/261632Mi)
% 0.20/0.30 % (1865770)lrs+1011_32_sil=2000:tgt=full:alpa=true:random_seed=778963349:st=5:i=107:sd=1:ss=included:er=filter_2999 on theBenchmark for (2999ds/107Mi)
% 0.20/0.30 % (1865771)lrs+10_2:3_to=lpo:sil=16000:sp=arity:random_seed=3509415351:i=114:bd=all:ss=axioms:sgt=4_2999 on theBenchmark for (2999ds/114Mi)
% 0.20/0.30 % (1865773)dis+1011_1_slsqr=8,1:sil=2000:spb=units:fd=off:kmz=on:flr=on:sac=on:slsq=on:random_seed=2897963019:st=2:i=121:sd=30:aac=none:ep=RS:ss=axioms:sgt=10_2999 on theBenchmark for (2999ds/121Mi)
% 0.20/0.30 % (1865773)Refutation not found, incomplete strategy
% 0.20/0.30 % (1865773)------------------------------
% 0.20/0.30 % (1865773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.30 % (1865773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.30 % (1865773)CaDiCaL version: 2.1.3
% 0.20/0.30 % (1865773)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.30 % (1865773)Time elapsed: 0.001 s
% 0.20/0.30 % (1865773)Peak memory usage: 12 MB
% 0.20/0.30 % (1865773)------------------------------
% 0.20/0.30 % (1865773)------------------------------
% 0.20/0.30 % (1865775)lrs+10_1_sil=2000:sos=on:random_seed=1411931280:i=135:sd=2:gtg=position:ss=axioms_2999 on theBenchmark for (2999ds/135Mi)
% 0.20/0.30 % (1865775)Refutation not found, incomplete strategy
% 0.20/0.30 % (1865775)------------------------------
% 0.20/0.30 % (1865775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.30 % (1865775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.30 % (1865775)CaDiCaL version: 2.1.3
% 0.20/0.30 % (1865775)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.30 % (1865775)Time elapsed: 0.0000 s
% 0.20/0.30 % (1865775)Peak memory usage: 12 MB
% 0.20/0.30 % (1865775)------------------------------
% 0.20/0.30 % (1865775)------------------------------
% 0.20/0.30 % (1865784)dis+1010_4_sil=2000:sos=on:sac=on:random_seed=2265706158:i=140:sd=1:ss=axioms_2999 on theBenchmark for (2999ds/140Mi)
% 0.20/0.30 % (1865784)Refutation not found, incomplete strategy
% 0.20/0.30 % (1865784)------------------------------
% 0.20/0.30 % (1865784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.30 % (1865784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.30 % (1865784)CaDiCaL version: 2.1.3
% 0.20/0.30 % (1865784)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.30 % (1865784)Time elapsed: 0.0000 s
% 0.20/0.30 % (1865784)Peak memory usage: 12 MB
% 0.20/0.30 % (1865784)------------------------------
% 0.20/0.30 % (1865784)------------------------------
% 0.20/0.30 % (1865770) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1865762-1865770"...
% 0.20/0.30 % (1865770)...printing done.
% 0.20/0.30 % SZS status CounterSatisfiable for theBenchmark
% 0.20/0.30 % SZS output start Saturation.
% See solution above
% 0.20/0.30 % SZS output start Definitions and Model Updates.
% 0.20/0.30 % SZS output end Definitions and Model Updates.
% 0.20/0.30 % (1865770)------------------------------
% 0.20/0.30 % (1865770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.30 % (1865770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.30 % (1865770)CaDiCaL version: 2.1.3
% 0.20/0.30 % (1865770)Termination reason: Satisfiable
% 0.20/0.30 % (1865770)Time elapsed: 0.018 s
% 0.20/0.30 % (1865770)Peak memory usage: 12 MB
% 0.20/0.30 % (1865770)Instructions burned: 42 (million)
% 0.20/0.30 % (1865762)Success in time 0.061 s
% 0.20/0.30 % Vampire exiting
%------------------------------------------------------------------------------