%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO090^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:46:36 AM UTC 2026
% Result : Theorem 0.19s 0.26s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 14
% Syntax : Number of formulae : 43 ( 20 unt; 0 typ; 13 def)
% Number of atoms : 631 ( 142 equ)
% Maximal formula atoms : 26 ( 14 avg)
% Number of connectives : 401 ( 160 ~; 140 |; 96 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of FOOLs : 347 ( 347 fml; 0 var)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 57 ( 54 usr; 6 prp; 0-2 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
t: $o ).
tff(func_def_1,type,
s: $o ).
tff(func_def_2,type,
q: $o ).
tff(func_def_3,type,
p: $o ).
tff(pred_def_1,type,
sP0: $o > $o ).
tff(pred_def_2,type,
sP1: $o > $o ).
tff(pred_def_3,type,
sP2: $o > $o ).
tff(pred_def_4,type,
sP3: $o > $o ).
tff(pred_def_5,type,
sP4: $o > $o ).
tff(pred_def_6,type,
sP5: $o > $o ).
tff(pred_def_7,type,
sP6: $o > $o ).
tff(pred_def_8,type,
sP7: $o > $o ).
tff(pred_def_9,type,
sP8: $o > $o ).
tff(pred_def_10,type,
sP9: $o > $o ).
tff(pred_def_11,type,
sP10: $o > $o ).
tff(pred_def_12,type,
sP11: $o > $o ).
tff(pred_def_13,type,
sP12: $o > $o ).
tff(pred_def_14,type,
sP13: $o > $o ).
tff(pred_def_15,type,
sP14: $o > $o ).
tff(pred_def_16,type,
sP15: $o > $o ).
tff(pred_def_17,type,
sP16: $o > $o ).
tff(pred_def_18,type,
sP17: $o > $o ).
tff(pred_def_19,type,
sP18: $o > $o ).
tff(pred_def_20,type,
sP19: $o > $o ).
tff(pred_def_21,type,
sP20: $o > $o ).
tff(pred_def_22,type,
sP21: $o > $o ).
tff(pred_def_23,type,
sP22: $o > $o ).
tff(pred_def_24,type,
sP23: $o > $o ).
tff(pred_def_25,type,
sP24: $o > $o ).
tff(pred_def_26,type,
sP25: $o > $o ).
tff(pred_def_27,type,
sP26: $o > $o ).
tff(pred_def_28,type,
sP27: $o > $o ).
tff(pred_def_29,type,
sP28: $o > $o ).
tff(pred_def_30,type,
sP29: $o > $o ).
tff(pred_def_31,type,
sP30: $o > $o ).
tff(pred_def_32,type,
sP31: $o > $o ).
tff(pred_def_33,type,
sP32: $o > $o ).
tff(pred_def_34,type,
sP33: $o > $o ).
tff(pred_def_35,type,
sP34: $o > $o ).
tff(pred_def_36,type,
sP35: $o > $o ).
tff(pred_def_37,type,
sP36: $o > $o ).
tff(pred_def_38,type,
sP37: $o > $o ).
tff(pred_def_39,type,
sP38: $o > $o ).
tff(pred_def_40,type,
sP39: $o > $o ).
tff(pred_def_41,type,
sP40: $o > $o ).
tff(pred_def_42,type,
sP41: $o > $o ).
tff(pred_def_43,type,
sP42: $o > $o ).
tff(pred_def_44,type,
sP43: $o > $o ).
tff(pred_def_45,type,
sP44: $o > $o ).
tff(pred_def_46,type,
sP45: $o > $o ).
tff(pred_def_47,type,
sP46: $o > $o ).
tff(pred_def_48,type,
sP47: $o > $o ).
tff(pred_def_49,type,
sP48: $o > $o ).
tff(pred_def_50,type,
sP49: $o > $o ).
tff(f1,conjecture,
( ( ~ t
| ~ s
| ~ q
| ~ ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& p ) ) ) ) ) ) )
=> ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& p ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cDMG8) ).
tff(f2,negated_conjecture,
~ ( ( ~ t
| ~ s
| ~ q
| ~ ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& p ) ) ) ) ) ) )
=> ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& p ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
tff(f3,plain,
~ ( ( ~ t
| ~ s
| ~ q
| ~ ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& p ) ) ) ) ) ) )
=> ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& ( ~ ( t
& s )
| ~ ( q
& p ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f2]) ).
tff(f4,plain,
~ ( ( ( t != $true )
| ( s != $true )
| ( q != $true )
| ~ ( ~ ( ( t = $true )
& ( s = $true ) )
| ~ ( ( q = $true )
& ( ~ ( ( t = $true )
& ( s = $true ) )
| ~ ( ( q = $true )
& ( ~ ( ( t = $true )
& ( s = $true ) )
| ~ ( ( q = $true )
& ( p = $true ) ) ) ) ) ) ) )
=> ( ~ ( ( t = $true )
& ( s = $true ) )
| ~ ( ( q = $true )
& ( ~ ( ( t = $true )
& ( s = $true ) )
| ~ ( ( q = $true )
& ( ~ ( ( t = $true )
& ( s = $true ) )
| ~ ( ( q = $true )
& ( ~ ( ( t = $true )
& ( s = $true ) )
| ~ ( ( q = $true )
& ( p = $true ) ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f3]) ).
tff(f5,plain,
~ ( ( ( t != $true )
| ( s != $true )
| ( q != $true )
| ~ ( ~ ( ( t = $true )
& ( s = $true ) )
| ~ ( ( q = $true )
& ( ~ ( ( t = $true )
& ( s = $true ) )
| ~ ( ( q = $true )
& ( ~ ( ( t = $true )
& ( s = $true ) )
| ~ ( ( q = $true )
& ( p = $true ) ) ) ) ) ) ) )
=> ( ~ ( ( t = $true )
& ( s = $true ) )
| ~ ( ( q = $true )
& ( ~ ( ( t = $true )
& ( s = $true ) )
| ~ ( ( q = $true )
& ( ~ ( ( t = $true )
& ( s = $true ) )
| ~ ( ( q = $true )
& ( ~ ( ( t = $true )
& ( s = $true ) )
| ~ ( ( q = $true )
& ( p = $true ) ) ) ) ) ) ) ) ) ),
inference(flattening,[],[f4]) ).
tff(f6,plain,
( ( t = $true )
& ( s = $true )
& ( q = $true )
& ( ( t != $true )
| ( s != $true )
| ( q != $true )
| ( ( t = $true )
& ( s = $true )
& ( q = $true )
& ( ( t != $true )
| ( s != $true )
| ( q != $true )
| ( p != $true ) ) ) )
& ( ( t != $true )
| ( s != $true )
| ( q != $true )
| ( ( t = $true )
& ( s = $true )
& ( q = $true )
& ( ( t != $true )
| ( s != $true )
| ( q != $true )
| ( ( t = $true )
& ( s = $true )
& ( q = $true )
& ( p = $true ) ) ) ) ) ),
inference(ennf_transformation,[],[f5]) ).
tff(f7,plain,
( ( t = $true )
& ( s = $true )
& ( q = $true )
& ( ( t != $true )
| ( s != $true )
| ( q != $true )
| ( ( t = $true )
& ( s = $true )
& ( q = $true )
& ( ( t != $true )
| ( s != $true )
| ( q != $true )
| ( p != $true ) ) ) )
& ( ( t != $true )
| ( s != $true )
| ( q != $true )
| ( ( t = $true )
& ( s = $true )
& ( q = $true )
& ( ( t != $true )
| ( s != $true )
| ( q != $true )
| ( ( t = $true )
& ( s = $true )
& ( q = $true )
& ( p = $true ) ) ) ) ) ),
inference(flattening,[],[f6]) ).
tff(f8,plain,
( ( t != $true )
| ( s != $true )
| ( q != $true )
| ( t != $true )
| ( s != $true )
| ( q != $true )
| ( p = $true ) ),
inference(cnf_transformation,[],[f7]) ).
tff(f15,plain,
( ( t != $true )
| ( s != $true )
| ( q != $true )
| ( t != $true )
| ( s != $true )
| ( q != $true )
| ( p != $true ) ),
inference(cnf_transformation,[],[f7]) ).
tff(f19,plain,
q = $true,
inference(cnf_transformation,[],[f7]) ).
tff(f20,plain,
s = $true,
inference(cnf_transformation,[],[f7]) ).
tff(f21,plain,
t = $true,
inference(cnf_transformation,[],[f7]) ).
tff(f27,plain,
( ( $true != $true )
| ( $true != $true )
| ( $true != $true )
| ( $true != $true )
| ( $true != $true )
| ( $true != $true )
| ( p != $true ) ),
inference(definition_unfolding,[],[f15,f21,f20,f19,f21,f20,f19]) ).
tff(f34,plain,
( ( $true != $true )
| ( $true != $true )
| ( $true != $true )
| ( $true != $true )
| ( $true != $true )
| ( $true != $true )
| ( p = $true ) ),
inference(definition_unfolding,[],[f8,f21,f20,f19,f21,f20,f19]) ).
tff(f49,definition,
~ sP10($true),
introduced(definition,[new_symbols(definition,[sP10])],[inequality_splitting_name_introduction]) ).
tff(f50,definition,
~ sP11($true),
introduced(definition,[new_symbols(definition,[sP11])],[inequality_splitting_name_introduction]) ).
tff(f51,definition,
~ sP12($true),
introduced(definition,[new_symbols(definition,[sP12])],[inequality_splitting_name_introduction]) ).
tff(f52,definition,
~ sP13($true),
introduced(definition,[new_symbols(definition,[sP13])],[inequality_splitting_name_introduction]) ).
tff(f53,definition,
~ sP14($true),
introduced(definition,[new_symbols(definition,[sP14])],[inequality_splitting_name_introduction]) ).
tff(f54,definition,
~ sP15($true),
introduced(definition,[new_symbols(definition,[sP15])],[inequality_splitting_name_introduction]) ).
tff(f55,definition,
~ sP16(p),
introduced(definition,[new_symbols(definition,[sP16])],[inequality_splitting_name_introduction]) ).
tff(f56,plain,
( sP10($true)
| sP11($true)
| sP12($true)
| sP13($true)
| sP14($true)
| sP15($true)
| sP16($true) ),
inference(inequality_splitting,[],[f27,f55,f54,f53,f52,f51,f50,f49]) ).
tff(f90,definition,
~ sP44($true),
introduced(definition,[new_symbols(definition,[sP44])],[inequality_splitting_name_introduction]) ).
tff(f91,definition,
~ sP45($true),
introduced(definition,[new_symbols(definition,[sP45])],[inequality_splitting_name_introduction]) ).
tff(f92,definition,
~ sP46($true),
introduced(definition,[new_symbols(definition,[sP46])],[inequality_splitting_name_introduction]) ).
tff(f93,definition,
~ sP47($true),
introduced(definition,[new_symbols(definition,[sP47])],[inequality_splitting_name_introduction]) ).
tff(f94,definition,
~ sP48($true),
introduced(definition,[new_symbols(definition,[sP48])],[inequality_splitting_name_introduction]) ).
tff(f95,definition,
~ sP49($true),
introduced(definition,[new_symbols(definition,[sP49])],[inequality_splitting_name_introduction]) ).
tff(f96,plain,
( sP44($true)
| sP45($true)
| sP46($true)
| sP47($true)
| sP48($true)
| sP49($true)
| ( p = $true ) ),
inference(inequality_splitting,[],[f34,f95,f94,f93,f92,f91,f90]) ).
tff(f149,plain,
( sP11($true)
| sP12($true)
| sP13($true)
| sP14($true)
| sP15($true)
| sP16($true) ),
inference(forward_subsumption_resolution,[],[f56,f49]) ).
tff(f150,plain,
( sP12($true)
| sP13($true)
| sP14($true)
| sP15($true)
| sP16($true) ),
inference(forward_subsumption_resolution,[],[f149,f50]) ).
tff(f151,plain,
( sP13($true)
| sP14($true)
| sP15($true)
| sP16($true) ),
inference(forward_subsumption_resolution,[],[f150,f51]) ).
tff(f152,plain,
( sP14($true)
| sP15($true)
| sP16($true) ),
inference(forward_subsumption_resolution,[],[f151,f52]) ).
tff(f153,plain,
( sP15($true)
| sP16($true) ),
inference(forward_subsumption_resolution,[],[f152,f53]) ).
tff(f154,plain,
sP16($true),
inference(forward_subsumption_resolution,[],[f153,f54]) ).
tff(f228,plain,
( sP45($true)
| sP46($true)
| sP47($true)
| sP48($true)
| sP49($true)
| ( p = $true ) ),
inference(forward_subsumption_resolution,[],[f96,f90]) ).
tff(f229,plain,
( sP46($true)
| sP47($true)
| sP48($true)
| sP49($true)
| ( p = $true ) ),
inference(forward_subsumption_resolution,[],[f228,f91]) ).
tff(f230,plain,
( sP47($true)
| sP48($true)
| sP49($true)
| ( p = $true ) ),
inference(forward_subsumption_resolution,[],[f229,f92]) ).
tff(f231,plain,
( sP48($true)
| sP49($true)
| ( p = $true ) ),
inference(forward_subsumption_resolution,[],[f230,f93]) ).
tff(f232,plain,
( sP49($true)
| ( p = $true ) ),
inference(forward_subsumption_resolution,[],[f231,f94]) ).
tff(f233,plain,
p = $true,
inference(forward_subsumption_resolution,[],[f232,f95]) ).
tff(f234,plain,
~ sP16($true),
inference(superposition,[],[f55,f233]) ).
tff(f235,plain,
$false,
inference(forward_subsumption_resolution,[],[f234,f154]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO090^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.18 % Computer : n026.cluster.edu
% 0.10/0.18 % Model : x86_64 x86_64
% 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.18 % Memory : 8046.5625MB
% 0.10/0.18 % OS : Linux 6.8.0-71-generic
% 0.10/0.18 % CPULimit : 300
% 0.10/0.18 % WCLimit : 300
% 0.10/0.18 % DateTime : Tue Sep 29 16:35:58 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.21 Running higher-order theorem proving
% 0.10/0.22 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.19/0.26 % (821989)Detected formulas, will run a generic FOF schedule.
% 0.19/0.26 % (821999)dis+1010_16_tgt=full:drc=ordering:sp=reverse_frequency:nwc=1:random_seed=3694278829:i=261632:kws=inv_arity_squared:ins=1:av=off:fsd=on_2999 on theBenchmark for (2999ds/261632Mi)
% 0.19/0.26 % (821999) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-821989-821999"...
% 0.19/0.26 % (821999)...printing done.
% 0.19/0.26 % (821999)Refutation found. Thanks to Tanya!
% 0.19/0.26 % SZS status Theorem for theBenchmark
% 0.19/0.26 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.26 % (821999)------------------------------
% 0.19/0.26 % (821999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.26 % (821999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.26 % (821999)CaDiCaL version: 2.1.3
% 0.19/0.26 % (821999)Termination reason: Refutation
% 0.19/0.26 % (821999)Time elapsed: 0.003 s
% 0.19/0.26 % (821999)Peak memory usage: 12 MB
% 0.19/0.26 % (821999)Instructions burned: 9 (million)
% 0.19/0.26 % (821989)Success in time 0.031 s
% 0.19/0.26 % Vampire exiting
%------------------------------------------------------------------------------