%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR062+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 09:42:29 AM UTC 2026
% Result : Theorem 4.44s 1.58s
% Output : Refutation 4.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 10
% Syntax : Number of formulae : 46 ( 13 unt; 2 def)
% Number of atoms : 83 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 67 ( 30 ~; 26 |; 2 &)
% ( 2 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 3 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 30 ( 0 sgn 28 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f86,axiom,
genlmt(c_tptp_spindleheadmt,c_cyclistsmt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3_86) ).
fof(f6288,axiom,
genlmt(c_tptp_member3205_mt,c_tptp_spindleheadmt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3_6288) ).
fof(f6493,axiom,
! [X0,X1] :
( tptptypes_7_389(X0,X1)
=> tptptypes_6_388(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3_6493) ).
fof(f10910,axiom,
! [X0,X1] :
( tptptypes_8_390(X0,X1)
=> tptptypes_7_389(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3_10910) ).
fof(f11372,axiom,
! [X0,X1] :
( tptptypes_6_388(X0,X1)
=> tptptypes_5_387(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3_11372) ).
fof(f18623,axiom,
( mtvisible(c_cyclistsmt)
=> tptptypes_8_390(c_pushingwithfingers,c_tptpcol_15_4027) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3_18623) ).
fof(f44208,axiom,
! [X0,X1] :
( ( mtvisible(X0)
& genlmt(X0,X1) )
=> mtvisible(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3_44208) ).
fof(f44217,conjecture,
? [X0] :
( mtvisible(c_tptp_member3205_mt)
=> tptptypes_5_387(X0,c_pushingwithfingers) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query212) ).
fof(f44218,negated_conjecture,
~ ? [X0] :
( mtvisible(c_tptp_member3205_mt)
=> tptptypes_5_387(X0,c_pushingwithfingers) ),
inference(negated_conjecture,[status(cth)],[f44217]) ).
fof(f44240,plain,
! [X0] :
( ~ tptptypes_5_387(X0,c_pushingwithfingers)
& mtvisible(c_tptp_member3205_mt) ),
inference(ennf_transformation,[],[f44218]) ).
fof(f44241,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(ennf_transformation,[],[f44208]) ).
fof(f44242,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(flattening,[],[f44241]) ).
fof(f44244,plain,
! [X0,X1] :
( tptptypes_5_387(X0,X1)
| ~ tptptypes_6_388(X0,X1) ),
inference(ennf_transformation,[],[f11372]) ).
fof(f44247,plain,
( tptptypes_8_390(c_pushingwithfingers,c_tptpcol_15_4027)
| ~ mtvisible(c_cyclistsmt) ),
inference(ennf_transformation,[],[f18623]) ).
fof(f44252,plain,
! [X0,X1] :
( tptptypes_6_388(X1,X0)
| ~ tptptypes_7_389(X0,X1) ),
inference(ennf_transformation,[],[f6493]) ).
fof(f44254,plain,
! [X0,X1] :
( tptptypes_7_389(X0,X1)
| ~ tptptypes_8_390(X0,X1) ),
inference(ennf_transformation,[],[f10910]) ).
fof(f44257,plain,
mtvisible(c_tptp_member3205_mt),
inference(cnf_transformation,[],[f44240]) ).
fof(f44258,plain,
! [X0] : ~ tptptypes_5_387(X0,c_pushingwithfingers),
inference(cnf_transformation,[],[f44240]) ).
fof(f44259,plain,
! [X0,X1] :
( ~ genlmt(X0,X1)
| ~ mtvisible(X0)
| mtvisible(X1) ),
inference(cnf_transformation,[],[f44242]) ).
fof(f44262,plain,
! [X0,X1] :
( ~ tptptypes_6_388(X0,X1)
| tptptypes_5_387(X0,X1) ),
inference(cnf_transformation,[],[f44244]) ).
fof(f44265,plain,
genlmt(c_tptp_member3205_mt,c_tptp_spindleheadmt),
inference(cnf_transformation,[],[f6288]) ).
fof(f44268,plain,
( tptptypes_8_390(c_pushingwithfingers,c_tptpcol_15_4027)
| ~ mtvisible(c_cyclistsmt) ),
inference(cnf_transformation,[],[f44247]) ).
fof(f44272,plain,
! [X0,X1] :
( ~ tptptypes_7_389(X0,X1)
| tptptypes_6_388(X1,X0) ),
inference(cnf_transformation,[],[f44252]) ).
fof(f44276,plain,
genlmt(c_tptp_spindleheadmt,c_cyclistsmt),
inference(cnf_transformation,[],[f86]) ).
fof(f44278,plain,
! [X0,X1] :
( ~ tptptypes_8_390(X0,X1)
| tptptypes_7_389(X0,X1) ),
inference(cnf_transformation,[],[f44254]) ).
fof(f44282,definition,
( spl0_1
<=> mtvisible(c_cyclistsmt) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f44284,plain,
( ~ mtvisible(c_cyclistsmt)
| spl0_1 ),
inference(avatar_component_clause,[],[f44282]) ).
fof(f44286,definition,
( spl0_2
<=> tptptypes_8_390(c_pushingwithfingers,c_tptpcol_15_4027) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f44288,plain,
( tptptypes_8_390(c_pushingwithfingers,c_tptpcol_15_4027)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f44286]) ).
fof(f44290,plain,
( ~ spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f44268,f44286,f44282]) ).
fof(f44294,plain,
( ~ mtvisible(c_tptp_member3205_mt)
| mtvisible(c_tptp_spindleheadmt) ),
inference(resolution,[],[f44259,f44265]) ).
fof(f44296,plain,
( ~ mtvisible(c_tptp_spindleheadmt)
| mtvisible(c_cyclistsmt) ),
inference(resolution,[],[f44259,f44276]) ).
fof(f44298,plain,
( ~ mtvisible(c_tptp_spindleheadmt)
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f44296,f44284]) ).
fof(f44299,plain,
mtvisible(c_tptp_spindleheadmt),
inference(forward_subsumption_resolution,[],[f44294,f44257]) ).
fof(f44300,plain,
( $false
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f44299,f44298]) ).
fof(f44301,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f44300]) ).
fof(f44302,plain,
( tptptypes_7_389(c_pushingwithfingers,c_tptpcol_15_4027)
| ~ spl0_2 ),
inference(resolution,[],[f44288,f44278]) ).
fof(f44303,plain,
( tptptypes_6_388(c_tptpcol_15_4027,c_pushingwithfingers)
| ~ spl0_2 ),
inference(resolution,[],[f44302,f44272]) ).
fof(f44309,plain,
( tptptypes_5_387(c_tptpcol_15_4027,c_pushingwithfingers)
| ~ spl0_2 ),
inference(resolution,[],[f44303,f44262]) ).
fof(f44310,plain,
( $false
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f44309,f44258]) ).
fof(f44311,plain,
~ spl0_2,
inference(avatar_contradiction_clause,[],[f44310]) ).
cnf(s2,plain,
( ~ spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f44290]) ).
cnf(s3,plain,
spl0_1,
inference(sat_conversion,[],[f44301]) ).
cnf(s4,plain,
~ spl0_2,
inference(sat_conversion,[],[f44311]) ).
cnf(s5,plain,
$false,
inference(rat,[],[s2,s4,s3]) ).
fof(f44312,plain,
$false,
inference(avatar_sat_refutation,[],[s5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR062+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n014.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 22:22:15 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.44/1.58 % (2252188)Detected formulas, will run a generic FOF schedule.
% 4.44/1.58 % (2252199)dis-21_1_sil=8000:lcm=predicate:random_seed=1724946785:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2995 on theBenchmark for (2995ds/129Mi)
% 4.44/1.58 % (2252194)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3422209966:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2995 on theBenchmark for (2995ds/134677Mi)
% 4.44/1.58 % (2252197)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1978223942:i=119:av=off:ss=axioms_2995 on theBenchmark for (2995ds/119Mi)
% 4.44/1.58 % (2252193)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2476631169:i=141193_2995 on theBenchmark for (2995ds/141193Mi)
% 4.44/1.58 % (2252195)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=431640962:i=141695:sd=1:nm=32:gsp=on:ss=included_2995 on theBenchmark for (2995ds/141695Mi)
% 4.44/1.58 % (2252198)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3600538605:s2a=on:i=139:gtg=position_2995 on theBenchmark for (2995ds/139Mi)
% 4.44/1.58 % (2252199)Instruction limit reached!
% 4.44/1.58 % (2252199)------------------------------
% 4.44/1.58 % (2252199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.58 % (2252199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.58 % (2252199)CaDiCaL version: 2.1.3
% 4.44/1.58 % (2252199)Termination reason: Instruction limit
% 4.44/1.58 % (2252199)Termination phase: SInE selection
% 4.44/1.58 % (2252199)Time elapsed: 0.044 s
% 4.44/1.58 % (2252199)Peak memory usage: 111 MB
% 4.44/1.58 % (2252199)Instructions burned: 131 (million)
% 4.44/1.58 % (2252196)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2830339329:i=109:sd=1:ins=1:gsp=on:ss=axioms_2995 on theBenchmark for (2995ds/109Mi)
% 4.44/1.58 % (2252198)Instruction limit reached!
% 4.44/1.58 % (2252198)------------------------------
% 4.44/1.58 % (2252198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.58 % (2252198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.58 % (2252198)CaDiCaL version: 2.1.3
% 4.44/1.58 % (2252198)Termination reason: Instruction limit
% 4.44/1.58 % (2252198)Termination phase: Property scanning
% 4.44/1.58 % (2252198)Time elapsed: 0.065 s
% 4.44/1.58 % (2252198)Peak memory usage: 110 MB
% 4.44/1.58 % (2252198)Instructions burned: 140 (million)
% 4.44/1.58 % (2252197)Instruction limit reached!
% 4.44/1.58 % (2252197)------------------------------
% 4.44/1.58 % (2252197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.58 % (2252197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.58 % (2252197)CaDiCaL version: 2.1.3
% 4.44/1.58 % (2252197)Termination reason: Instruction limit
% 4.44/1.58 % (2252197)Termination phase: Saturation
% 4.44/1.58 % (2252197)Time elapsed: 0.083 s
% 4.44/1.58 % (2252197)Peak memory usage: 116 MB
% 4.44/1.58 % (2252197)Instructions burned: 121 (million)
% 4.44/1.58 % (2252207)lrs+10_1_sil=8000:sp=occurrence:random_seed=1004444499:i=285:sd=3:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/285Mi)
% 4.44/1.58 % (2252196)Instruction limit reached!
% 4.44/1.58 % (2252196)------------------------------
% 4.44/1.58 % (2252196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.58 % (2252196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.58 % (2252196)CaDiCaL version: 2.1.3
% 4.44/1.58 % (2252196)Termination reason: Instruction limit
% 4.44/1.58 % (2252196)Termination phase: Saturation
% 4.44/1.58 % (2252196)Time elapsed: 0.125 s
% 4.44/1.58 % (2252196)Peak memory usage: 116 MB
% 4.44/1.58 % (2252196)Instructions burned: 110 (million)
% 4.44/1.58 % (2252207)First to succeed.
% 4.44/1.58 % (2252207)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2252188"
% 4.44/1.58 % (2252208)lrs+10_1_sil=32000:urr=on:br=off:random_seed=250674353:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/157Mi)
% 4.44/1.58 % (2252209)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1656272848:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 4.44/1.58 % (2252208)Instruction limit reached!
% 4.44/1.58 % (2252208)------------------------------
% 4.44/1.58 % (2252208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.58 % (2252208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.58 % (2252208)CaDiCaL version: 2.1.3
% 4.44/1.58 % (2252208)Termination reason: Instruction limit
% 4.44/1.58 % (2252208)Termination phase: Property scanning
% 4.44/1.58 % (2252208)Time elapsed: 0.073 s
% 4.44/1.58 % (2252208)Peak memory usage: 111 MB
% 4.44/1.58 % (2252208)Instructions burned: 157 (million)
% 4.44/1.58 % (2252211)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3226449884:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 4.44/1.58 % (2252209)Refutation not found, incomplete strategy
% 4.44/1.58 % (2252209)------------------------------
% 4.44/1.58 % (2252209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.58 % (2252209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.58 % (2252209)CaDiCaL version: 2.1.3
% 4.44/1.58 % (2252209)Termination reason: Refutation not found, incomplete strategy
% 4.44/1.58 % (2252209)Time elapsed: 0.085 s
% 4.44/1.58 % (2252209)Peak memory usage: 118 MB
% 4.44/1.58 % (2252209)Instructions burned: 113 (million)
% 4.44/1.58 % (2252207)Refutation found. Thanks to Tanya!
% 4.44/1.58 % SZS status Theorem for theBenchmark
% 4.44/1.58 % SZS output start Proof for theBenchmark
% See solution above
% 4.44/1.58 % (2252207)------------------------------
% 4.44/1.58 % (2252207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.58 % (2252207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.58 % (2252207)CaDiCaL version: 2.1.3
% 4.44/1.58 % (2252207)Termination reason: Refutation
% 4.44/1.58 % (2252207)Time elapsed: 0.052 s
% 4.44/1.58 % (2252207)Peak memory usage: 120 MB
% 4.44/1.58 % (2252207)Instructions burned: 115 (million)
% 4.44/1.58 % (2252207)------------------------------
% 4.44/1.58 % (2252207)------------------------------
% 4.44/1.58 % (2252188)Success in time 0.931 s
% 4.44/1.58 % Vampire exiting
%------------------------------------------------------------------------------