%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL092-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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 : Tue Sep 29 11:57:37 AM UTC 2026
% Result : Unsatisfiable 1.98s 0.72s
% Output : Refutation 1.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 14
% Syntax : Number of formulae : 94 ( 23 unt; 11 def)
% Number of atoms : 200 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 195 ( 89 ~; 95 |; 0 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 13 ( 12 usr; 12 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 239 ( 0 sgn 239 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X3)),implies(implies(X3,X0),implies(X4,implies(X2,X0))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic_JLukasiewicz_5) ).
fof(f3,negated_conjecture,
~ is_a_theorem(implies(implies(implies(a,b),a),a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_ic_3) ).
fof(f4,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))
| is_a_theorem(implies(implies(X3,X0),implies(X4,implies(X2,X0)))) ),
inference(resolution,[],[f2,f1]) ).
fof(f5,plain,
! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(implies(implies(X0,implies(X1,X2)),implies(X2,X3)),implies(X4,implies(implies(X5,X2),implies(X2,X3))))),
inference(resolution,[],[f4,f2]) ).
fof(f6,plain,
! [X2,X3,X0,X1,X6,X4,X5] : is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X1,X2)),implies(X3,implies(X4,X1))),implies(X5,implies(X6,implies(X3,implies(X4,X1)))))),
inference(resolution,[],[f5,f4]) ).
fof(f7,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X2,X3)))
| is_a_theorem(implies(X4,implies(implies(X5,X2),implies(X2,X3)))) ),
inference(resolution,[],[f5,f1]) ).
fof(f8,plain,
! [X2,X3,X0,X1,X4] : is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X2,implies(implies(X3,X4),implies(X4,X2)))))),
inference(resolution,[],[f7,f5]) ).
fof(f11,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(X1,X2),implies(X2,implies(implies(X3,X4),implies(X4,X2))))) ),
inference(resolution,[],[f8,f1]) ).
fof(f13,definition,
( spl0_1
<=> ! [X2,X1,X3,X4] : is_a_theorem(implies(implies(X1,X2),implies(X2,implies(implies(X3,X4),implies(X4,X2))))) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f14,plain,
( ! [X2,X3,X1,X4] : is_a_theorem(implies(implies(X1,X2),implies(X2,implies(implies(X3,X4),implies(X4,X2)))))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f13]) ).
fof(f16,definition,
( spl0_2
<=> ! [X0] : ~ is_a_theorem(X0) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f17,plain,
( ! [X0] : ~ is_a_theorem(X0)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f16]) ).
fof(f18,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f11,f16,f13]) ).
fof(f20,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : is_a_theorem(implies(implies(implies(X0,implies(X1,implies(X2,X3))),implies(implies(X4,X3),implies(X3,X5))),implies(X6,implies(X7,implies(implies(X4,X3),implies(X3,X5)))))),
inference(resolution,[],[f6,f4]) ).
fof(f28,plain,
( $false
| ~ spl0_2 ),
inference(backward_subsumption_resolution,[],[f8,f17]) ).
fof(f32,plain,
~ spl0_2,
inference(avatar_contradiction_clause,[],[f28]) ).
fof(f35,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X1,X2)),X3),implies(X4,implies(X2,X3))))
| ~ spl0_1 ),
inference(resolution,[],[f14,f4]) ).
fof(f52,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X2,implies(X3,implies(X4,X2))))))
| ~ spl0_1 ),
inference(resolution,[],[f35,f7]) ).
fof(f66,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(X1,X2),implies(X2,implies(X3,implies(X4,X2))))) )
| ~ spl0_1 ),
inference(resolution,[],[f52,f1]) ).
fof(f68,definition,
( spl0_4
<=> ! [X2,X1,X3,X4] : is_a_theorem(implies(implies(X1,X2),implies(X2,implies(X3,implies(X4,X2))))) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f69,plain,
( ! [X2,X3,X1,X4] : is_a_theorem(implies(implies(X1,X2),implies(X2,implies(X3,implies(X4,X2)))))
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f68]) ).
fof(f70,plain,
( spl0_4
| spl0_2
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f66,f13,f16,f68]) ).
fof(f75,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : is_a_theorem(implies(implies(implies(X0,implies(implies(X1,X2),implies(X2,X3))),implies(X4,implies(X5,implies(X6,X2)))),implies(X7,implies(X8,implies(X4,implies(X5,implies(X6,X2))))))),
inference(resolution,[],[f20,f4]) ).
fof(f77,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ is_a_theorem(implies(implies(X0,implies(X1,implies(X2,X3))),implies(implies(X4,X3),implies(X3,X5))))
| is_a_theorem(implies(X6,implies(X7,implies(implies(X4,X3),implies(X3,X5))))) ),
inference(resolution,[],[f20,f1]) ).
fof(f78,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(X0,implies(X1,X2)),X3),implies(X4,implies(X2,X3))))
| ~ spl0_4 ),
inference(resolution,[],[f69,f4]) ).
fof(f195,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ is_a_theorem(implies(implies(X0,implies(implies(X1,X2),implies(X2,X3))),implies(X4,implies(X5,implies(X6,X2)))))
| is_a_theorem(implies(X7,implies(X8,implies(X4,implies(X5,implies(X6,X2)))))) ),
inference(resolution,[],[f75,f1]) ).
fof(f313,plain,
! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(X0,implies(X1,implies(implies(implies(X2,X3),X2),implies(X4,implies(implies(X5,X2),X2)))))),
inference(resolution,[],[f195,f2]) ).
fof(f448,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(implies(implies(X2,X3),X2),implies(X4,implies(implies(X5,X2),X2))))) ),
inference(resolution,[],[f313,f1]) ).
fof(f450,definition,
( spl0_11
<=> ! [X3,X4,X5,X2,X1] : is_a_theorem(implies(X1,implies(implies(implies(X2,X3),X2),implies(X4,implies(implies(X5,X2),X2))))) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f451,plain,
( ! [X2,X3,X1,X4,X5] : is_a_theorem(implies(X1,implies(implies(implies(X2,X3),X2),implies(X4,implies(implies(X5,X2),X2)))))
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f450]) ).
fof(f452,plain,
( spl0_11
| spl0_2 ),
inference(avatar_split_clause,[],[f448,f16,f450]) ).
fof(f1210,plain,
( ! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(implies(implies(X0,implies(implies(X1,X2),X2)),X3),implies(X4,implies(implies(implies(X2,X5),X2),X3))))
| ~ spl0_11 ),
inference(resolution,[],[f451,f4]) ).
fof(f1225,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(implies(X1,X2),X1),implies(X3,implies(implies(X4,X1),X1)))) )
| ~ spl0_11 ),
inference(resolution,[],[f451,f1]) ).
fof(f1227,definition,
( spl0_42
<=> ! [X4,X3,X2,X1] : is_a_theorem(implies(implies(implies(X1,X2),X1),implies(X3,implies(implies(X4,X1),X1)))) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f1228,plain,
( ! [X2,X3,X1,X4] : is_a_theorem(implies(implies(implies(X1,X2),X1),implies(X3,implies(implies(X4,X1),X1))))
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f1227]) ).
fof(f1229,plain,
( spl0_42
| spl0_2
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1225,f450,f16,f1227]) ).
fof(f1240,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X0))
| is_a_theorem(implies(X2,implies(implies(X3,X0),X0))) )
| ~ spl0_42 ),
inference(resolution,[],[f1228,f1]) ).
fof(f1246,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(X0,implies(implies(X1,implies(X2,implies(X3,X3))),implies(X2,implies(X3,X3)))))
| ~ spl0_4
| ~ spl0_42 ),
inference(resolution,[],[f1240,f78]) ).
fof(f2829,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(X1,implies(X2,implies(X3,X3))),implies(X2,implies(X3,X3)))) )
| ~ spl0_4
| ~ spl0_42 ),
inference(resolution,[],[f1246,f1]) ).
fof(f2831,definition,
( spl0_82
<=> ! [X2,X1,X3] : is_a_theorem(implies(implies(X1,implies(X2,implies(X3,X3))),implies(X2,implies(X3,X3)))) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f2832,plain,
( ! [X2,X3,X1] : is_a_theorem(implies(implies(X1,implies(X2,implies(X3,X3))),implies(X2,implies(X3,X3))))
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f2831]) ).
fof(f2833,plain,
( spl0_82
| spl0_2
| ~ spl0_4
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f2829,f1227,f68,f16,f2831]) ).
fof(f2878,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(implies(X2,X3),implies(X3,X3)))))
| ~ spl0_82 ),
inference(resolution,[],[f2832,f77]) ).
fof(f3443,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(implies(X2,X3),implies(X3,X3)))) )
| ~ spl0_82 ),
inference(resolution,[],[f2878,f1]) ).
fof(f3445,definition,
( spl0_94
<=> ! [X2,X1,X3] : is_a_theorem(implies(X1,implies(implies(X2,X3),implies(X3,X3)))) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f3446,plain,
( ! [X2,X3,X1] : is_a_theorem(implies(X1,implies(implies(X2,X3),implies(X3,X3))))
| ~ spl0_94 ),
inference(avatar_component_clause,[],[f3445]) ).
fof(f3447,plain,
( spl0_94
| spl0_2
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f3443,f2831,f16,f3445]) ).
fof(f3482,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(X1,X2),implies(X2,X2))) )
| ~ spl0_94 ),
inference(resolution,[],[f3446,f1]) ).
fof(f3484,definition,
( spl0_96
<=> ! [X2,X1] : is_a_theorem(implies(implies(X1,X2),implies(X2,X2))) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f3485,plain,
( ! [X2,X1] : is_a_theorem(implies(implies(X1,X2),implies(X2,X2)))
| ~ spl0_96 ),
inference(avatar_component_clause,[],[f3484]) ).
fof(f3486,plain,
( spl0_96
| spl0_2
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f3482,f3445,f16,f3484]) ).
fof(f3487,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X2,implies(X0,X1))))
| ~ spl0_96 ),
inference(resolution,[],[f3485,f4]) ).
fof(f3673,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),implies(X2,implies(X3,X0))))
| ~ spl0_96 ),
inference(resolution,[],[f3487,f4]) ).
fof(f5148,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X0))
| is_a_theorem(implies(X2,implies(X3,X0))) )
| ~ spl0_96 ),
inference(resolution,[],[f3673,f1]) ).
fof(f12628,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(X0,implies(X1,implies(X2,implies(implies(implies(X3,X4),X3),X3)))))
| ~ spl0_11
| ~ spl0_96 ),
inference(resolution,[],[f1210,f5148]) ).
fof(f12734,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,implies(implies(implies(X3,X4),X3),X3)))) )
| ~ spl0_11
| ~ spl0_96 ),
inference(resolution,[],[f12628,f1]) ).
fof(f12751,definition,
( spl0_281
<=> ! [X4,X2,X1,X3] : is_a_theorem(implies(X1,implies(X2,implies(implies(implies(X3,X4),X3),X3)))) ),
introduced(definition,[new_symbols(definition,[spl0_281])],[avatar_definition]) ).
fof(f12752,plain,
( ! [X2,X3,X1,X4] : is_a_theorem(implies(X1,implies(X2,implies(implies(implies(X3,X4),X3),X3))))
| ~ spl0_281 ),
inference(avatar_component_clause,[],[f12751]) ).
fof(f12753,plain,
( spl0_281
| spl0_2
| ~ spl0_11
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f12734,f3484,f450,f16,f12751]) ).
fof(f12803,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(implies(implies(X2,X3),X2),X2))) )
| ~ spl0_281 ),
inference(resolution,[],[f12752,f1]) ).
fof(f12813,definition,
( spl0_282
<=> ! [X2,X1,X3] : is_a_theorem(implies(X1,implies(implies(implies(X2,X3),X2),X2))) ),
introduced(definition,[new_symbols(definition,[spl0_282])],[avatar_definition]) ).
fof(f12814,plain,
( ! [X2,X3,X1] : is_a_theorem(implies(X1,implies(implies(implies(X2,X3),X2),X2)))
| ~ spl0_282 ),
inference(avatar_component_clause,[],[f12813]) ).
fof(f12815,plain,
( spl0_282
| spl0_2
| ~ spl0_281 ),
inference(avatar_split_clause,[],[f12803,f12751,f16,f12813]) ).
fof(f12854,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(implies(X1,X2),X1),X1)) )
| ~ spl0_282 ),
inference(resolution,[],[f12814,f1]) ).
fof(f12863,definition,
( spl0_283
<=> ! [X2,X1] : is_a_theorem(implies(implies(implies(X1,X2),X1),X1)) ),
introduced(definition,[new_symbols(definition,[spl0_283])],[avatar_definition]) ).
fof(f12864,plain,
( ! [X2,X1] : is_a_theorem(implies(implies(implies(X1,X2),X1),X1))
| ~ spl0_283 ),
inference(avatar_component_clause,[],[f12863]) ).
fof(f12865,plain,
( spl0_283
| spl0_2
| ~ spl0_282 ),
inference(avatar_split_clause,[],[f12854,f12813,f16,f12863]) ).
fof(f13041,plain,
( $false
| ~ spl0_283 ),
inference(backward_subsumption_resolution,[],[f3,f12864]) ).
fof(f13070,plain,
~ spl0_283,
inference(avatar_contradiction_clause,[],[f13041]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f18]) ).
cnf(s5,plain,
~ spl0_2,
inference(sat_conversion,[],[f32]) ).
cnf(s7,plain,
( ~ spl0_1
| spl0_2
| spl0_4 ),
inference(sat_conversion,[],[f70]) ).
cnf(s14,plain,
( spl0_2
| spl0_11 ),
inference(sat_conversion,[],[f452]) ).
cnf(s182,plain,
( spl0_2
| ~ spl0_11
| spl0_42 ),
inference(sat_conversion,[],[f1229]) ).
cnf(s546,plain,
( spl0_2
| ~ spl0_4
| ~ spl0_42
| spl0_82 ),
inference(sat_conversion,[],[f2833]) ).
cnf(s734,plain,
( spl0_2
| ~ spl0_82
| spl0_94 ),
inference(sat_conversion,[],[f3447]) ).
cnf(s748,plain,
( spl0_2
| ~ spl0_94
| spl0_96 ),
inference(sat_conversion,[],[f3486]) ).
cnf(s3241,plain,
( spl0_2
| ~ spl0_11
| ~ spl0_96
| spl0_281 ),
inference(sat_conversion,[],[f12753]) ).
cnf(s3266,plain,
( spl0_2
| ~ spl0_281
| spl0_282 ),
inference(sat_conversion,[],[f12815]) ).
cnf(s3271,plain,
( spl0_2
| ~ spl0_282
| spl0_283 ),
inference(sat_conversion,[],[f12865]) ).
cnf(s3326,plain,
~ spl0_283,
inference(sat_conversion,[],[f13070]) ).
cnf(s3327,plain,
( spl0_2
| ~ spl0_282 ),
inference(rat,[],[s3271,s3326]) ).
cnf(s3328,plain,
~ spl0_282,
inference(rat,[],[s3327,s5]) ).
cnf(s3329,plain,
~ spl0_281,
inference(rat,[],[s3266,s3328,s5]) ).
cnf(s3354,plain,
spl0_11,
inference(rat,[],[s14,s5]) ).
cnf(s3360,plain,
~ spl0_96,
inference(rat,[],[s3241,s3329,s5,s3354]) ).
cnf(s3361,plain,
spl0_42,
inference(rat,[],[s182,s5,s3354]) ).
cnf(s3363,plain,
~ spl0_94,
inference(rat,[],[s748,s5,s3360]) ).
cnf(s3364,plain,
~ spl0_82,
inference(rat,[],[s734,s5,s3363]) ).
cnf(s3365,plain,
~ spl0_4,
inference(rat,[],[s546,s3361,s5,s3364]) ).
cnf(s3366,plain,
~ spl0_1,
inference(rat,[],[s7,s5,s3365]) ).
cnf(s3367,plain,
$false,
inference(rat,[],[s1,s5,s3366]) ).
fof(f13071,plain,
$false,
inference(avatar_sat_refutation,[],[s3367]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL092-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.37 % Computer : n013.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 : Sun Sep 27 15:20:51 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.40 Running first-order model finding
% 0.12/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.98/0.72 % (341715)Will run a generic schedule for satisfiability detection.
% 1.98/0.72 % (341725)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3958854154:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 1.98/0.72 % (341721)% WARNING: option uhcvi not known.
% 1.98/0.72 % (341721)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=652700055:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 1.98/0.72 % (341723)dis+10_1_sil=32000:sp=arity:random_seed=443177723:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 1.98/0.72 % (341724)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1891828826:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 1.98/0.72 % (341726)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3820576262:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 1.98/0.72 % (341720)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=233823899_3000 on theBenchmark for (3000ds/0Mi)
% 1.98/0.72 % (341722)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2014512019:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 1.98/0.72 % TRYING [1]
% 1.98/0.72 % TRYING [2]
% 1.98/0.72 % TRYING [3]
% 1.98/0.72 % TRYING [4]
% 1.98/0.72 % (341725)Instruction limit reached!
% 1.98/0.72 % (341725)------------------------------
% 1.98/0.72 % (341725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.72 % (341725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.72 % (341725)CaDiCaL version: 2.1.3
% 1.98/0.72 % (341725)Termination reason: Instruction limit
% 1.98/0.72 % (341725)Termination phase: Saturation
% 1.98/0.72 % (341725)Time elapsed: 0.045 s
% 1.98/0.72 % (341725)Peak memory usage: 13 MB
% 1.98/0.72 % (341725)Instructions burned: 133 (million)
% 1.98/0.72 % (341734)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=195980588:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.98/0.72 % TRYING [1]
% 1.98/0.72 % TRYING [2]
% 1.98/0.72 % TRYING [3]
% 1.98/0.72 % TRYING [4]
% 1.98/0.72 % (341723)Instruction limit reached!
% 1.98/0.72 % (341723)------------------------------
% 1.98/0.72 % (341723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.72 % (341723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.72 % (341723)CaDiCaL version: 2.1.3
% 1.98/0.72 % (341723)Termination reason: Instruction limit
% 1.98/0.72 % (341723)Termination phase: Saturation
% 1.98/0.72 % (341723)Time elapsed: 0.066 s
% 1.98/0.72 % (341723)Peak memory usage: 12 MB
% 1.98/0.72 % (341723)Instructions burned: 103 (million)
% 1.98/0.72 % (341724)Instruction limit reached!
% 1.98/0.72 % (341724)------------------------------
% 1.98/0.72 % (341724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.72 % (341724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.72 % (341724)CaDiCaL version: 2.1.3
% 1.98/0.72 % (341724)Termination reason: Instruction limit
% 1.98/0.72 % (341724)Termination phase: Saturation
% 1.98/0.72 % (341724)Time elapsed: 0.071 s
% 1.98/0.72 % (341724)Peak memory usage: 11 MB
% 1.98/0.72 % (341724)Instructions burned: 117 (million)
% 1.98/0.72 % (341736)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=681837119:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.98/0.72 % (341737)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3798818959:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.98/0.72 % (341726)Instruction limit reached!
% 1.98/0.72 % (341726)------------------------------
% 1.98/0.72 % (341726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.72 % (341726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.72 % (341726)CaDiCaL version: 2.1.3
% 1.98/0.72 % (341726)Termination reason: Instruction limit
% 1.98/0.72 % (341726)Termination phase: Saturation
% 1.98/0.72 % (341726)Time elapsed: 0.102 s
% 1.98/0.72 % (341726)Peak memory usage: 13 MB
% 1.98/0.72 % (341726)Instructions burned: 163 (million)
% 1.98/0.72 % (341740)ott-21_1_sil=16000:fs=off:random_seed=350153476:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.98/0.72 % TRYING [5]
% 1.98/0.72 % (341736)Instruction limit reached!
% 1.98/0.72 % (341736)------------------------------
% 1.98/0.72 % (341736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.72 % (341736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.72 % (341736)CaDiCaL version: 2.1.3
% 1.98/0.72 % (341736)Termination reason: Instruction limit
% 1.98/0.72 % (341736)Termination phase: Saturation
% 1.98/0.72 % (341736)Time elapsed: 0.077 s
% 1.98/0.72 % (341736)Peak memory usage: 11 MB
% 1.98/0.72 % (341736)Instructions burned: 133 (million)
% 1.98/0.72 % TRYING [5]
% 1.98/0.72 % (341742)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2390852878:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.98/0.72 % (341740)Instruction limit reached!
% 1.98/0.72 % (341740)------------------------------
% 1.98/0.72 % (341740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.72 % (341740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.72 % (341740)CaDiCaL version: 2.1.3
% 1.98/0.72 % (341740)Termination reason: Instruction limit
% 1.98/0.72 % (341740)Termination phase: Saturation
% 1.98/0.72 % (341740)Time elapsed: 0.099 s
% 1.98/0.72 % (341740)Peak memory usage: 12 MB
% 1.98/0.72 % (341740)Instructions burned: 181 (million)
% 1.98/0.72 % (341744)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3358780517:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.98/0.72 % TRYING [1]
% 1.98/0.72 % TRYING [2]
% 1.98/0.72 % TRYING [3]
% 1.98/0.72 % TRYING [4]
% 1.98/0.72 % (341721) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-341715-341721"...
% 1.98/0.72 % (341721)...printing done.
% 1.98/0.72 % (341721)Refutation found. Thanks to Tanya!
% 1.98/0.72 % SZS status Unsatisfiable for theBenchmark
% 1.98/0.72 % SZS output start Proof for theBenchmark
% See solution above
% 1.98/0.72 % (341721)------------------------------
% 1.98/0.72 % (341721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.72 % (341721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.72 % (341721)CaDiCaL version: 2.1.3
% 1.98/0.72 % (341721)Termination reason: Refutation
% 1.98/0.72 % (341721)Time elapsed: 0.279 s
% 1.98/0.72 % (341721)Peak memory usage: 17 MB
% 1.98/0.72 % (341721)Instructions burned: 480 (million)
% 1.98/0.72 % (341715)Success in time 0.304 s
% 1.98/0.72 % Vampire exiting
%------------------------------------------------------------------------------