%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PHI017+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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 12:27:20 PM UTC 2026
% Result : CounterSatisfiable 16.75s 3.34s
% Output : Saturation 16.75s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u90,axiom,
( isMethodExistence(X1)
| isMethodAction(X1) ) ).
cnf(u94,axiom,
( ~ expressesInfiniteEssentiality(X1)
| ~ expressesEternalEssentiality(X1) ) ).
cnf(u104,axiom,
substance(X1) ).
cnf(u60,axiom,
( ~ absolutelyInfinite(X0)
| substance(X0) ) ).
cnf(u59,axiom,
( ~ absolutelyInfinite(X0)
| constInInfAttributes(X0) ) ).
cnf(u66,axiom,
( ~ determinedByItselfAlone(X1,X0)
| ~ existsOnlyByNecessityOfOwnNature(X0)
| free(X0) ) ).
cnf(u46,axiom,
( canBeLimitedBy(X0,X1)
| ~ finiteAfterItsKind(X0) ) ).
cnf(u80,axiom,
( effectNecessarilyFollowsFrom(X1,X0)
| ~ definiteCause(X0) ) ).
cnf(u116,axiom,
( ~ existsIn(X0,X0)
| mode(X0) ) ).
cnf(u48,axiom,
( ~ substance(X0)
| conceivedThruItself(X0) ) ).
cnf(u63,axiom,
( ~ actionOf(X1,X0)
| determinedByItselfAlone(X1,X0)
| ~ free(X0) ) ).
cnf(u70,axiom,
( externalTo(X1,X0)
| ~ necessary(X0) ) ).
cnf(u84,axiom,
conceivedThru(X1,X1) ).
cnf(u58,axiom,
( ~ attributeOf(X1,X0)
| expressesEternalEssentiality(X1)
| ~ absolutelyInfinite(X0) ) ).
cnf(u53,axiom,
( conceivedThru(X0,X2)
| modification(X0,X1)
| ~ mode(X0) ) ).
cnf(u83,axiom,
( existsIn(X1,X1)
| ~ exists(X1) ) ).
cnf(u76,axiom,
( ~ existsIn(X0,X0)
| exists(X0) ) ).
cnf(u75,axiom,
( ~ existsIn(X0,X1)
| exists(X0)
| X0 = X1 ) ).
cnf(u45,axiom,
( sameKind(X0,X1)
| ~ finiteAfterItsKind(X0) ) ).
cnf(u72,axiom,
( ~ determinedByDefiniteMethod(X0,X1)
| ~ externalTo(X1,X0)
| ~ determinedByFixedMethod(X0,X1)
| necessary(X0)
| ~ isMethodAction(X1) ) ).
cnf(u120,axiom,
( modification(X0,X1)
| ~ mode(X0)
| exists(X0) ) ).
cnf(u111,negated_conjecture,
inItself(sK0) ).
cnf(u55,axiom,
( ~ conceivedThru(X0,X2)
| ~ existsIn(X0,X2)
| mode(X0) ) ).
cnf(u82,negated_conjecture,
~ exists(sK0) ).
cnf(u124,axiom,
( ~ exists(X0)
| mode(X0) ) ).
cnf(u65,axiom,
( actionOf(X1,X0)
| ~ existsOnlyByNecessityOfOwnNature(X0)
| free(X0) ) ).
cnf(u81,negated_conjecture,
substance(sK0) ).
cnf(u50,axiom,
( ~ conceivedThruItself(X0)
| ~ inItself(X0)
| substance(X0) ) ).
cnf(u57,axiom,
( ~ attributeOf(X1,X0)
| expressesInfiniteEssentiality(X1)
| ~ absolutelyInfinite(X0) ) ).
cnf(u110,negated_conjecture,
conceivedThruItself(sK0) ).
cnf(u69,axiom,
( determinedByFixedMethod(X0,X1)
| ~ necessary(X0) ) ).
cnf(u64,axiom,
( ~ free(X0)
| existsOnlyByNecessityOfOwnNature(X0) ) ).
cnf(u113,axiom,
conceivedThruItself(X0) ).
cnf(u61,axiom,
( attributeOf(X1,X0)
| ~ substance(X0)
| ~ constInInfAttributes(X0)
| absolutelyInfinite(X0) ) ).
cnf(u71,axiom,
( ~ determinedByDefiniteMethod(X0,X1)
| ~ externalTo(X1,X0)
| ~ determinedByFixedMethod(X0,X1)
| necessary(X0)
| ~ isMethodExistence(X1) ) ).
cnf(u56,axiom,
( ~ modification(X0,X1)
| mode(X0)
| ~ substance(X1) ) ).
cnf(u54,axiom,
( existsIn(X0,X2)
| modification(X0,X1)
| ~ mode(X0) ) ).
cnf(u47,axiom,
( ~ sameKind(X0,X1)
| ~ canBeLimitedBy(X0,X1)
| finiteAfterItsKind(X0) ) ).
cnf(u49,axiom,
( ~ substance(X0)
| inItself(X0) ) ).
cnf(u112,axiom,
inItself(X0) ).
cnf(u68,axiom,
( determinedByDefiniteMethod(X0,X1)
| ~ necessary(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : PHI017+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.43 % Computer : n015.cluster.edu
% 0.14/0.43 % Model : x86_64 x86_64
% 0.14/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.43 % Memory : 8046.5625MB
% 0.14/0.43 % OS : Linux 6.8.0-71-generic
% 0.14/0.43 % CPULimit : 300
% 0.14/0.43 % WCLimit : 300
% 0.14/0.43 % DateTime : Sun Sep 27 22:10:31 UTC 2026
% 0.14/0.43 % CPUTime :
% 0.14/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.48 Running first-order theorem proving
% 0.20/0.48 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.94/2.10 % (2061448)Detected formulas, will run a generic FOF schedule.
% 8.94/2.10 % (2061457)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3276230239:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.94/2.10 % (2061457)Refutation not found, incomplete strategy
% 8.94/2.10 % (2061457)------------------------------
% 8.94/2.10 % (2061457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.94/2.10 % (2061457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.94/2.10 % (2061457)CaDiCaL version: 2.1.3
% 8.94/2.10 % (2061457)Termination reason: Refutation not found, incomplete strategy
% 8.94/2.10 % (2061457)Time elapsed: 0.001 s
% 8.94/2.10 % (2061457)Peak memory usage: 88 MB
% 8.94/2.10 % (2061456)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2631835779:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.94/2.10 % (2061455)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=3555703758:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.94/2.10 % (2061458)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=952116413:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.94/2.10 % (2061454)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=1050093810:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.94/2.10 % (2061459)dis-21_1_sil=8000:lcm=predicate:random_seed=3063654343:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 8.94/2.10 % (2061453)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=3479871836:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.94/2.10 % (2061456)Refutation not found, incomplete strategy
% 8.94/2.10 % (2061456)------------------------------
% 8.94/2.10 % (2061456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.94/2.10 % (2061456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.94/2.10 % (2061456)CaDiCaL version: 2.1.3
% 8.94/2.10 % (2061456)Termination reason: Refutation not found, incomplete strategy
% 8.94/2.10 % (2061456)Time elapsed: 0.001 s
% 8.94/2.10 % (2061456)Peak memory usage: 87 MB
% 8.94/2.10 % (2061459)Refutation not found, incomplete strategy
% 8.94/2.10 % (2061459)------------------------------
% 8.94/2.10 % (2061459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.94/2.10 % (2061459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.94/2.10 % (2061459)CaDiCaL version: 2.1.3
% 8.94/2.10 % (2061459)Termination reason: Refutation not found, incomplete strategy
% 8.94/2.10 % (2061459)Time elapsed: 0.003 s
% 8.94/2.10 % (2061459)Peak memory usage: 88 MB
% 8.94/2.10 % (2061459)Instructions burned: 1 (million)
% 8.94/2.10 % (2061458)Refutation not found, incomplete strategy
% 8.94/2.10 % (2061458)------------------------------
% 8.94/2.10 % (2061458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.94/2.10 % (2061458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.94/2.10 % (2061458)CaDiCaL version: 2.1.3
% 8.94/2.10 % (2061458)Termination reason: Refutation not found, incomplete strategy
% 8.94/2.10 % (2061458)Time elapsed: 0.004 s
% 8.94/2.10 % (2061458)Peak memory usage: 88 MB
% 8.94/2.10 % (2061458)Instructions burned: 2 (million)
% 8.94/2.10 % (2061457)------------------------------
% 8.94/2.10 % (2061457)------------------------------
% 8.94/2.10 % (2061467)lrs+10_1_sil=8000:sp=occurrence:random_seed=3869796094:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 8.94/2.10 % (2061467)Refutation not found, incomplete strategy
% 8.94/2.10 % (2061467)------------------------------
% 8.94/2.10 % (2061467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.94/2.10 % (2061467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.94/2.10 % (2061467)CaDiCaL version: 2.1.3
% 8.94/2.10 % (2061467)Termination reason: Refutation not found, incomplete strategy
% 8.94/2.10 % (2061467)Time elapsed: 0.002 s
% 8.94/2.10 % (2061467)Peak memory usage: 88 MB
% 8.94/2.10 % (2061467)Instructions burned: 1 (million)
% 8.94/2.10 % (2061459)------------------------------
% 10.74/2.73 % (2061459)------------------------------
% 10.74/2.73 % (2061456)------------------------------
% 10.74/2.73 % (2061456)------------------------------
% 10.74/2.73 % (2061458)------------------------------
% 10.74/2.73 % (2061458)------------------------------
% 10.74/2.73 % (2061467)------------------------------
% 10.74/2.73 % (2061467)------------------------------
% 10.74/2.73 [W927 22:10:32.896191231 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.74/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.74/2.73 [W927 22:10:32.896249725 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.74/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.74/2.73 [W927 22:10:32.896310239 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.74/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.74/2.73 [W927 22:10:32.896331426 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.74/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.74/2.73 [W927 22:10:32.896376056 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.74/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.74/2.73 [W927 22:10:32.896395536 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.74/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.74/2.73 [W927 22:10:32.896441150 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.74/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.74/2.73 [W927 22:10:32.896460063 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.74/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.74/2.73 [W927 22:10:32.896502957 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.74/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.74/2.73 [W927 22:10:32.896522540 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.74/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.74/2.73 [W927 22:10:32.896567937 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.74/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.74/2.73 [W927 22:10:32.896586907 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.74/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.74/2.73 % (2061469)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2029811118:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/157Mi)
% 15.35/3.13 % (2061471)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=4077923525:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 15.35/3.13 % (2061470)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3690952633:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 15.35/3.13 % (2061470)Refutation not found, incomplete strategy
% 15.35/3.13 % (2061470)------------------------------
% 15.35/3.13 % (2061470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.35/3.13 % (2061470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/3.13 % (2061470)CaDiCaL version: 2.1.3
% 15.35/3.13 % (2061470)Termination reason: Refutation not found, incomplete strategy
% 15.35/3.13 % (2061470)Time elapsed: 0.003 s
% 15.35/3.13 % (2061470)Peak memory usage: 88 MB
% 15.35/3.13 % (2061470)Instructions burned: 1 (million)
% 15.35/3.13 % (2061469)Refutation not found, incomplete strategy
% 15.35/3.13 % (2061469)------------------------------
% 15.35/3.13 % (2061469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.35/3.13 % (2061469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/3.13 % (2061469)CaDiCaL version: 2.1.3
% 15.35/3.13 % (2061469)Termination reason: Refutation not found, incomplete strategy
% 15.35/3.13 % (2061469)Time elapsed: 0.003 s
% 15.35/3.13 % (2061469)Peak memory usage: 88 MB
% 15.35/3.13 % (2061469)Instructions burned: 1 (million)
% 15.35/3.13 % (2061471)Refutation not found, incomplete strategy
% 15.35/3.13 % (2061471)------------------------------
% 15.35/3.13 % (2061471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.35/3.13 % (2061471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/3.13 % (2061471)CaDiCaL version: 2.1.3
% 15.35/3.13 % (2061471)Termination reason: Refutation not found, incomplete strategy
% 15.35/3.13 % (2061471)Time elapsed: 0.004 s
% 15.35/3.13 % (2061471)Peak memory usage: 89 MB
% 15.35/3.13 % (2061471)Instructions burned: 2 (million)
% 15.35/3.13 % (2061472)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2962596073:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 15.35/3.13 % (2061472)Refutation not found, incomplete strategy
% 15.35/3.13 % (2061472)------------------------------
% 15.35/3.13 % (2061472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.35/3.13 % (2061472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/3.13 % (2061472)CaDiCaL version: 2.1.3
% 15.35/3.13 % (2061472)Termination reason: Refutation not found, incomplete strategy
% 15.35/3.13 % (2061472)Time elapsed: 0.002 s
% 15.35/3.13 % (2061472)Peak memory usage: 88 MB
% 15.35/3.13 % (2061454)Refutation not found, incomplete strategy
% 15.35/3.13 % (2061454)------------------------------
% 15.35/3.13 % (2061454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.35/3.13 % (2061454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/3.13 % (2061454)CaDiCaL version: 2.1.3
% 15.35/3.13 % (2061454)Termination reason: Refutation not found, incomplete strategy
% 15.35/3.13 % (2061454)Time elapsed: 0.906 s
% 15.35/3.13 % (2061454)Peak memory usage: 126 MB
% 15.35/3.13 % (2061454)Instructions burned: 827 (million)
% 15.35/3.13 % (2061455)Refutation not found, incomplete strategy
% 15.35/3.13 % (2061455)------------------------------
% 15.35/3.13 % (2061455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.35/3.13 % (2061455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/3.13 % (2061455)CaDiCaL version: 2.1.3
% 15.35/3.13 % (2061455)Termination reason: Refutation not found, incomplete strategy
% 15.35/3.13 % (2061455)Time elapsed: 0.971 s
% 15.35/3.13 % (2061455)Peak memory usage: 127 MB
% 15.35/3.13 % (2061455)Instructions burned: 890 (million)
% 15.35/3.13 % (2061472)------------------------------
% 15.35/3.13 % (2061472)------------------------------
% 15.35/3.13 % (2061453)Refutation not found, incomplete strategy
% 15.35/3.13 % (2061453)------------------------------
% 15.35/3.13 % (2061453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.35/3.13 % (2061453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/3.13 % (2061453)CaDiCaL version: 2.1.3
% 15.35/3.13 % (2061453)Termination reason: Refutation not found, incomplete strategy
% 16.75/3.34 % (2061453)Time elapsed: 1.007 s
% 16.75/3.34 % (2061453)Peak memory usage: 128 MB
% 16.75/3.34 % (2061453)Instructions burned: 908 (million)
% 16.75/3.34 % (2061471)------------------------------
% 16.75/3.34 % (2061471)------------------------------
% 16.75/3.34 % (2061469)------------------------------
% 16.75/3.34 % (2061469)------------------------------
% 16.75/3.34 % (2061470)------------------------------
% 16.75/3.34 % (2061470)------------------------------
% 16.75/3.34 % (2061477)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1195147342:i=2350_2987 on theBenchmark for (2987ds/2350Mi)
% 16.75/3.34 % (2061454)------------------------------
% 16.75/3.34 % (2061454)------------------------------
% 16.75/3.34 % (2061479)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=365165043:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 16.75/3.34 % (2061478)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3451958423:cts=off:i=113:fsr=off:ss=included:sgt=4_2986 on theBenchmark for (2986ds/113Mi)
% 16.75/3.34 % (2061480)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2912842275:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 16.75/3.34 % (2061479)Refutation not found, incomplete strategy
% 16.75/3.34 % (2061479)------------------------------
% 16.75/3.34 % (2061479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.75/3.34 % (2061479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.34 % (2061479)CaDiCaL version: 2.1.3
% 16.75/3.34 % (2061479)Termination reason: Refutation not found, incomplete strategy
% 16.75/3.34 % (2061479)Time elapsed: 0.002 s
% 16.75/3.34 % (2061479)Peak memory usage: 87 MB
% 16.75/3.34 % (2061480)Refutation not found, incomplete strategy
% 16.75/3.34 % (2061480)------------------------------
% 16.75/3.34 % (2061480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.75/3.34 % (2061480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.34 % (2061480)CaDiCaL version: 2.1.3
% 16.75/3.34 % (2061480)Termination reason: Refutation not found, incomplete strategy
% 16.75/3.34 % (2061480)Time elapsed: 0.002 s
% 16.75/3.34 % (2061480)Peak memory usage: 88 MB
% 16.75/3.34 % (2061478)Refutation not found, incomplete strategy
% 16.75/3.34 % (2061478)------------------------------
% 16.75/3.34 % (2061478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.75/3.34 % (2061478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.34 % (2061478)CaDiCaL version: 2.1.3
% 16.75/3.34 % (2061478)Termination reason: Refutation not found, incomplete strategy
% 16.75/3.34 % (2061478)Time elapsed: 0.004 s
% 16.75/3.34 % (2061478)Peak memory usage: 88 MB
% 16.75/3.34 % (2061478)Instructions burned: 2 (million)
% 16.75/3.34 % (2061455)------------------------------
% 16.75/3.34 % (2061455)------------------------------
% 16.75/3.34 % (2061453)------------------------------
% 16.75/3.34 % (2061453)------------------------------
% 16.75/3.34 % (2061485)lrs+10_1_sil=8000:sp=occurrence:random_seed=2868270185:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 16.75/3.34 % (2061485)Refutation not found, incomplete strategy
% 16.75/3.34 % (2061485)------------------------------
% 16.75/3.34 % (2061485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.75/3.34 % (2061485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.34 % (2061485)CaDiCaL version: 2.1.3
% 16.75/3.34 % (2061485)Termination reason: Refutation not found, incomplete strategy
% 16.75/3.34 % (2061485)Time elapsed: 0.003 s
% 16.75/3.34 % (2061485)Peak memory usage: 88 MB
% 16.75/3.34 % (2061485)Instructions burned: 1 (million)
% 16.75/3.34 % (2061487)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3405987206:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 16.75/3.34 % (2061486)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3111734007:i=437:sd=1:aac=none:ss=included_2983 on theBenchmark for (2983ds/437Mi)
% 16.75/3.34 % (2061486)Refutation not found, incomplete strategy
% 16.75/3.34 % (2061486)------------------------------
% 16.75/3.34 % (2061486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.75/3.34 % (2061486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.34 % (2061486)CaDiCaL version: 2.1.3
% 16.75/3.34 % (2061486)Termination reason: Refutation not found, incomplete strategy
% 16.75/3.34 % (2061486)Time elapsed: 0.002 s
% 16.75/3.34 % (2061486)Peak memory usage: 88 MB
% 16.75/3.34 % (2061480)------------------------------
% 16.75/3.34 % (2061480)------------------------------
% 16.75/3.34 % (2061479)------------------------------
% 16.75/3.34 % (2061479)------------------------------
% 16.75/3.34 % (2061478)------------------------------
% 16.75/3.34 % (2061478)------------------------------
% 16.75/3.34 % (2061477)First to succeed.
% 16.75/3.34 % (2061477)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2061448"
% 16.75/3.34 % (2061493)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1679520453:st=3:i=13193:sd=3:ss=axioms_2980 on theBenchmark for (2980ds/13193Mi)
% 16.75/3.34 % (2061485)------------------------------
% 16.75/3.34 % (2061485)------------------------------
% 16.75/3.34 % (2061491)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1854591573:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 16.75/3.34 % (2061492)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2968569540:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 16.75/3.34 % (2061492)Refutation not found, incomplete strategy
% 16.75/3.34 % (2061492)------------------------------
% 16.75/3.34 % (2061492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.75/3.34 % (2061491)Refutation not found, incomplete strategy
% 16.75/3.34 % (2061491)------------------------------
% 16.75/3.34 % (2061491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.75/3.34 % (2061491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.34 % (2061491)CaDiCaL version: 2.1.3
% 16.75/3.34 % (2061492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.34 % (2061492)CaDiCaL version: 2.1.3
% 16.75/3.34 % (2061491)Termination reason: Refutation not found, incomplete strategy
% 16.75/3.34 % (2061491)Time elapsed: 0.002 s
% 16.75/3.34 % (2061491)Peak memory usage: 88 MB
% 16.75/3.34 % (2061492)Termination reason: Refutation not found, incomplete strategy
% 16.75/3.34 % (2061492)Time elapsed: 0.002 s
% 16.75/3.34 % (2061492)Peak memory usage: 88 MB
% 16.75/3.34 % (2061492)Instructions burned: 1 (million)
% 16.75/3.34 % SZS status CounterSatisfiable for theBenchmark
% 16.75/3.34 % SZS output start Saturation.
% See solution above
% 16.75/3.34 % SZS output start Definitions and Model Updates.
% 16.75/3.34 for all inputs,
% 16.75/3.34 define haveNothingInCommon(X0,X1) := $true
% 16.75/3.34 for all inputs,
% 16.75/3.34 define canBeUnderstoodInTermsOf(X0,X1) := $false
% 16.75/3.34 for all inputs,
% 16.75/3.34 define conceptionInvolves(X0,X1) := $false
% 16.75/3.34 for all inputs,
% 16.75/3.34 define trueIdea(X0) := $true
% 16.75/3.34 for all inputs,
% 16.75/3.34 define correspondWith(X0,X1) := $true
% 16.75/3.34 for all inputs,
% 16.75/3.34 define ideateOf(X0,X1) := $true
% 16.75/3.34 for all inputs,
% 16.75/3.34 define objectOf(X0,X1) := $true
% 16.75/3.34 for all inputs,
% 16.75/3.34 define canBeConceivedAsNonExisting(X0) := $true
% 16.75/3.34 for all inputs,
% 16.75/3.34 define essenceInvExistence(X0) := $false
% 16.75/3.34 for all inputs,
% 16.75/3.34 define selfCaused(X0) := essenceInvExistence(X0) & natureConcOnlyByExistence(X0)
% 16.75/3.34 for all inputs,
% 16.75/3.34 define attribute(X0) := intPercAsConstEssSub(X0)
% 16.75/3.34 for all inputs,
% 16.75/3.34 define god(X0) := being(X0) & absolutelyInfinite(X0)
% 16.75/3.34 for all inputs,
% 16.75/3.34 define eternity(X0) := existConcFollowFromDefEternal(X0)
% 16.75/3.34 for all inputs,
% 16.75/3.34 define knowledgeOfEffect(X0,X1) := knowledgeOfACause(X0)
% 16.75/3.34 % SZS output end Definitions and Model Updates.
% 16.75/3.34 % (2061477)------------------------------
% 16.75/3.34 % (2061477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.75/3.34 % (2061477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.34 % (2061477)CaDiCaL version: 2.1.3
% 16.75/3.34 % (2061477)Termination reason: Satisfiable
% 16.75/3.34 % (2061477)Time elapsed: 0.554 s
% 16.75/3.34 % (2061477)Peak memory usage: 128 MB
% 16.75/3.34 % (2061477)Instructions burned: 906 (million)
% 16.75/3.34 % (2061477)------------------------------
% 16.75/3.34 % (2061477)------------------------------
% 16.75/3.34 % (2061448)Success in time 2.298 s
% 16.75/3.34 % Vampire exiting
%------------------------------------------------------------------------------