%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PLA031-1.001 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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:28:38 PM UTC 2026
% Result : Unsatisfiable 23.94s 8.34s
% Output : Refutation 23.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 106
% Syntax : Number of formulae : 195 ( 151 unt; 0 def)
% Number of atoms : 259 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 190 ( 126 ~; 64 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-6 aty)
% Number of functors : 8 ( 8 usr; 8 con; 0-0 aty)
% Number of variables : 236 ( 236 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X0,X4)
| s(truck1,X1,X2,X3,X0,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',load1) ).
fof(f2,axiom,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X0,X4)
| ~ s(truck1,X1,X2,X3,X0,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',load2) ).
fof(f3,axiom,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X4,X0)
| s(truck2,X1,X2,X3,X4,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',load3) ).
fof(f4,axiom,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X4,X0)
| ~ s(truck2,X1,X2,X3,X4,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',load4) ).
fof(f5,axiom,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X1,X4)
| s(X0,truck1,X2,X3,X1,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',load5) ).
fof(f6,axiom,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X1,X4)
| ~ s(X0,truck1,X2,X3,X1,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',load6) ).
fof(f7,axiom,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X4,X1)
| s(X0,truck2,X2,X3,X4,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',load7) ).
fof(f8,axiom,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X4,X1)
| ~ s(X0,truck2,X2,X3,X4,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',load8) ).
fof(f9,axiom,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X2,X4)
| ~ neq(X3,truck1)
| s(X0,X1,truck1,X3,X2,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',board1) ).
fof(f10,axiom,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X2,X4)
| ~ s(X0,X1,truck1,X3,X2,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',board2) ).
fof(f11,axiom,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X4,X2)
| ~ neq(X3,truck2)
| s(X0,X1,truck2,X3,X4,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',board3) ).
fof(f12,axiom,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X4,X2)
| ~ s(X0,X1,truck2,X3,X4,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',board4) ).
fof(f13,axiom,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X3,X4)
| ~ neq(X2,truck1)
| s(X0,X1,X2,truck1,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',board5) ).
fof(f14,axiom,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X3,X4)
| ~ s(X0,X1,X2,truck1,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',board6) ).
fof(f15,axiom,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X4,X3)
| ~ neq(X2,truck2)
| s(X0,X1,X2,truck2,X4,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',board7) ).
fof(f16,axiom,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X4,X3)
| ~ s(X0,X1,X2,truck2,X4,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',board8) ).
fof(f17,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ s(X0,X1,truck1,X2,X3,X4)
| ~ link(X3,X5)
| s(X0,X1,truck1,X2,X5,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',drive1) ).
fof(f18,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ s(X0,X1,truck2,X2,X3,X4)
| ~ link(X4,X5)
| s(X0,X1,truck2,X2,X3,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',drive2) ).
fof(f19,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ s(X0,X1,X2,truck1,X3,X4)
| ~ link(X3,X5)
| s(X0,X1,X2,truck1,X5,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',drive3) ).
fof(f20,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ s(X0,X1,X2,truck2,X3,X4)
| ~ link(X4,X5)
| s(X0,X1,X2,truck2,X3,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',drive4) ).
fof(f21,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ s(X0,X1,X2,X3,X4,X5)
| ~ path(X2,X6)
| s(X0,X1,X6,X3,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',walk1) ).
fof(f22,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ s(X0,X1,X2,X3,X4,X5)
| ~ path(X3,X6)
| s(X0,X1,X2,X6,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',walk2) ).
fof(f23,axiom,
~ neq(truck1,truck1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq1) ).
fof(f24,axiom,
neq(truck1,truck2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq2) ).
fof(f25,axiom,
neq(truck1,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq3) ).
fof(f26,axiom,
neq(truck1,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq4) ).
fof(f27,axiom,
neq(truck1,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq5) ).
fof(f28,axiom,
neq(truck1,p1_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq6) ).
fof(f29,axiom,
neq(truck1,p2_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq7) ).
fof(f30,axiom,
neq(truck1,p2_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq8) ).
fof(f31,axiom,
neq(truck2,truck1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq9) ).
fof(f32,axiom,
~ neq(truck2,truck2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq10) ).
fof(f33,axiom,
neq(truck2,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq11) ).
fof(f34,axiom,
neq(truck2,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq12) ).
fof(f35,axiom,
neq(truck2,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq13) ).
fof(f36,axiom,
neq(truck2,p1_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq14) ).
fof(f37,axiom,
neq(truck2,p2_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq15) ).
fof(f38,axiom,
neq(truck2,p2_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq16) ).
fof(f39,axiom,
neq(s0,truck1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq17) ).
fof(f40,axiom,
neq(s0,truck2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq18) ).
fof(f41,axiom,
~ neq(s0,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq19) ).
fof(f42,axiom,
neq(s0,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq20) ).
fof(f43,axiom,
neq(s0,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq21) ).
fof(f44,axiom,
neq(s0,p1_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq22) ).
fof(f45,axiom,
neq(s0,p2_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq23) ).
fof(f46,axiom,
neq(s0,p2_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq24) ).
fof(f47,axiom,
neq(s1,truck1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq25) ).
fof(f48,axiom,
neq(s1,truck2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq26) ).
fof(f49,axiom,
neq(s1,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq27) ).
fof(f50,axiom,
~ neq(s1,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq28) ).
fof(f51,axiom,
neq(s1,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq29) ).
fof(f52,axiom,
neq(s1,p1_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq30) ).
fof(f53,axiom,
neq(s1,p2_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq31) ).
fof(f54,axiom,
neq(s1,p2_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq32) ).
fof(f55,axiom,
neq(s2,truck1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq33) ).
fof(f56,axiom,
neq(s2,truck2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq34) ).
fof(f57,axiom,
neq(s2,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq35) ).
fof(f58,axiom,
neq(s2,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq36) ).
fof(f59,axiom,
~ neq(s2,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq37) ).
fof(f60,axiom,
neq(s2,p1_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq38) ).
fof(f61,axiom,
neq(s2,p2_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq39) ).
fof(f62,axiom,
neq(s2,p2_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq40) ).
fof(f63,axiom,
neq(p1_0,truck1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq41) ).
fof(f64,axiom,
neq(p1_0,truck2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq42) ).
fof(f65,axiom,
neq(p1_0,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq43) ).
fof(f66,axiom,
neq(p1_0,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq44) ).
fof(f67,axiom,
neq(p1_0,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq45) ).
fof(f68,axiom,
~ neq(p1_0,p1_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq46) ).
fof(f69,axiom,
neq(p1_0,p2_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq47) ).
fof(f70,axiom,
neq(p1_0,p2_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq48) ).
fof(f71,axiom,
neq(p2_0,truck1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq49) ).
fof(f72,axiom,
neq(p2_0,truck2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq50) ).
fof(f73,axiom,
neq(p2_0,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq51) ).
fof(f74,axiom,
neq(p2_0,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq52) ).
fof(f75,axiom,
neq(p2_0,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq53) ).
fof(f76,axiom,
neq(p2_0,p1_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq54) ).
fof(f77,axiom,
~ neq(p2_0,p2_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq55) ).
fof(f78,axiom,
neq(p2_0,p2_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq56) ).
fof(f79,axiom,
neq(p2_1,truck1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq57) ).
fof(f80,axiom,
neq(p2_1,truck2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq58) ).
fof(f81,axiom,
neq(p2_1,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq59) ).
fof(f82,axiom,
neq(p2_1,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq60) ).
fof(f83,axiom,
neq(p2_1,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq61) ).
fof(f84,axiom,
neq(p2_1,p1_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq62) ).
fof(f85,axiom,
neq(p2_1,p2_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq63) ).
fof(f86,axiom,
~ neq(p2_1,p2_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq64) ).
fof(f87,axiom,
path(s1,p1_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map1) ).
fof(f88,axiom,
path(p1_0,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map2) ).
fof(f89,axiom,
path(s0,p1_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map3) ).
fof(f90,axiom,
path(p1_0,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map4) ).
fof(f91,axiom,
path(s2,p2_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map5) ).
fof(f92,axiom,
path(p2_0,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map6) ).
fof(f93,axiom,
path(s0,p2_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map7) ).
fof(f94,axiom,
path(p2_0,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map8) ).
fof(f95,axiom,
path(s2,p2_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map9) ).
fof(f96,axiom,
path(p2_1,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map10) ).
fof(f97,axiom,
path(s1,p2_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map11) ).
fof(f98,axiom,
path(p2_1,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map12) ).
fof(f99,axiom,
link(s0,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map13) ).
fof(f100,axiom,
link(s1,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map14) ).
fof(f101,axiom,
link(s0,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map15) ).
fof(f102,axiom,
link(s2,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map16) ).
fof(f103,axiom,
link(s1,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map17) ).
fof(f104,axiom,
link(s2,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map18) ).
fof(f105,axiom,
s(s2,s2,s0,s1,s0,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',init) ).
fof(f106,negated_conjecture,
~ s(s2,s1,s2,s2,s2,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f107,plain,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X0,X4)
| ~ s(truck1,X1,X2,X3,X0,X4) ),
inference(consistent_polarity_flipping,[],[f1]) ).
fof(f108,plain,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X0,X4)
| s(truck1,X1,X2,X3,X0,X4) ),
inference(consistent_polarity_flipping,[],[f2]) ).
fof(f109,plain,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X4,X0)
| ~ s(truck2,X1,X2,X3,X4,X0) ),
inference(consistent_polarity_flipping,[],[f3]) ).
fof(f110,plain,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X4,X0)
| s(truck2,X1,X2,X3,X4,X0) ),
inference(consistent_polarity_flipping,[],[f4]) ).
fof(f111,plain,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X1,X4)
| ~ s(X0,truck1,X2,X3,X1,X4) ),
inference(consistent_polarity_flipping,[],[f5]) ).
fof(f112,plain,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X1,X4)
| s(X0,truck1,X2,X3,X1,X4) ),
inference(consistent_polarity_flipping,[],[f6]) ).
fof(f113,plain,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X4,X1)
| ~ s(X0,truck2,X2,X3,X4,X1) ),
inference(consistent_polarity_flipping,[],[f7]) ).
fof(f114,plain,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X4,X1)
| s(X0,truck2,X2,X3,X4,X1) ),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f115,plain,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X2,X4)
| neq(X3,truck1)
| ~ s(X0,X1,truck1,X3,X2,X4) ),
inference(consistent_polarity_flipping,[],[f9]) ).
fof(f116,plain,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X2,X4)
| s(X0,X1,truck1,X3,X2,X4) ),
inference(consistent_polarity_flipping,[],[f10]) ).
fof(f117,plain,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X4,X2)
| neq(X3,truck2)
| ~ s(X0,X1,truck2,X3,X4,X2) ),
inference(consistent_polarity_flipping,[],[f11]) ).
fof(f118,plain,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X4,X2)
| s(X0,X1,truck2,X3,X4,X2) ),
inference(consistent_polarity_flipping,[],[f12]) ).
fof(f119,plain,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X3,X4)
| neq(X2,truck1)
| ~ s(X0,X1,X2,truck1,X3,X4) ),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f120,plain,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X3,X4)
| s(X0,X1,X2,truck1,X3,X4) ),
inference(consistent_polarity_flipping,[],[f14]) ).
fof(f121,plain,
! [X2,X3,X0,X1,X4] :
( s(X0,X1,X2,X3,X4,X3)
| neq(X2,truck2)
| ~ s(X0,X1,X2,truck2,X4,X3) ),
inference(consistent_polarity_flipping,[],[f15]) ).
fof(f122,plain,
! [X2,X3,X0,X1,X4] :
( ~ s(X0,X1,X2,X3,X4,X3)
| s(X0,X1,X2,truck2,X4,X3) ),
inference(consistent_polarity_flipping,[],[f16]) ).
fof(f123,plain,
! [X2,X3,X0,X1,X4,X5] :
( s(X0,X1,truck1,X2,X3,X4)
| ~ link(X3,X5)
| ~ s(X0,X1,truck1,X2,X5,X4) ),
inference(consistent_polarity_flipping,[],[f17]) ).
fof(f124,plain,
! [X2,X3,X0,X1,X4,X5] :
( s(X0,X1,truck2,X2,X3,X4)
| ~ link(X4,X5)
| ~ s(X0,X1,truck2,X2,X3,X5) ),
inference(consistent_polarity_flipping,[],[f18]) ).
fof(f125,plain,
! [X2,X3,X0,X1,X4,X5] :
( s(X0,X1,X2,truck1,X3,X4)
| ~ link(X3,X5)
| ~ s(X0,X1,X2,truck1,X5,X4) ),
inference(consistent_polarity_flipping,[],[f19]) ).
fof(f126,plain,
! [X2,X3,X0,X1,X4,X5] :
( s(X0,X1,X2,truck2,X3,X4)
| ~ link(X4,X5)
| ~ s(X0,X1,X2,truck2,X3,X5) ),
inference(consistent_polarity_flipping,[],[f20]) ).
fof(f127,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( s(X0,X1,X2,X3,X4,X5)
| ~ path(X2,X6)
| ~ s(X0,X1,X6,X3,X4,X5) ),
inference(consistent_polarity_flipping,[],[f21]) ).
fof(f128,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( s(X0,X1,X2,X3,X4,X5)
| ~ path(X3,X6)
| ~ s(X0,X1,X2,X6,X4,X5) ),
inference(consistent_polarity_flipping,[],[f22]) ).
fof(f129,plain,
neq(truck1,truck1),
inference(consistent_polarity_flipping,[],[f23]) ).
fof(f130,plain,
~ neq(truck1,truck2),
inference(consistent_polarity_flipping,[],[f24]) ).
fof(f131,plain,
~ neq(truck1,s0),
inference(consistent_polarity_flipping,[],[f25]) ).
fof(f132,plain,
~ neq(truck1,s1),
inference(consistent_polarity_flipping,[],[f26]) ).
fof(f133,plain,
~ neq(truck1,s2),
inference(consistent_polarity_flipping,[],[f27]) ).
fof(f134,plain,
~ neq(truck1,p1_0),
inference(consistent_polarity_flipping,[],[f28]) ).
fof(f135,plain,
~ neq(truck1,p2_0),
inference(consistent_polarity_flipping,[],[f29]) ).
fof(f136,plain,
~ neq(truck1,p2_1),
inference(consistent_polarity_flipping,[],[f30]) ).
fof(f137,plain,
~ neq(truck2,truck1),
inference(consistent_polarity_flipping,[],[f31]) ).
fof(f138,plain,
neq(truck2,truck2),
inference(consistent_polarity_flipping,[],[f32]) ).
fof(f139,plain,
~ neq(truck2,s0),
inference(consistent_polarity_flipping,[],[f33]) ).
fof(f140,plain,
~ neq(truck2,s1),
inference(consistent_polarity_flipping,[],[f34]) ).
fof(f141,plain,
~ neq(truck2,s2),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f142,plain,
~ neq(truck2,p1_0),
inference(consistent_polarity_flipping,[],[f36]) ).
fof(f143,plain,
~ neq(truck2,p2_0),
inference(consistent_polarity_flipping,[],[f37]) ).
fof(f144,plain,
~ neq(truck2,p2_1),
inference(consistent_polarity_flipping,[],[f38]) ).
fof(f145,plain,
~ neq(s0,truck1),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f146,plain,
~ neq(s0,truck2),
inference(consistent_polarity_flipping,[],[f40]) ).
fof(f147,plain,
neq(s0,s0),
inference(consistent_polarity_flipping,[],[f41]) ).
fof(f148,plain,
~ neq(s0,s1),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f149,plain,
~ neq(s0,s2),
inference(consistent_polarity_flipping,[],[f43]) ).
fof(f150,plain,
~ neq(s0,p1_0),
inference(consistent_polarity_flipping,[],[f44]) ).
fof(f151,plain,
~ neq(s0,p2_0),
inference(consistent_polarity_flipping,[],[f45]) ).
fof(f152,plain,
~ neq(s0,p2_1),
inference(consistent_polarity_flipping,[],[f46]) ).
fof(f153,plain,
~ neq(s1,truck1),
inference(consistent_polarity_flipping,[],[f47]) ).
fof(f154,plain,
~ neq(s1,truck2),
inference(consistent_polarity_flipping,[],[f48]) ).
fof(f155,plain,
~ neq(s1,s0),
inference(consistent_polarity_flipping,[],[f49]) ).
fof(f156,plain,
neq(s1,s1),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f157,plain,
~ neq(s1,s2),
inference(consistent_polarity_flipping,[],[f51]) ).
fof(f158,plain,
~ neq(s1,p1_0),
inference(consistent_polarity_flipping,[],[f52]) ).
fof(f159,plain,
~ neq(s1,p2_0),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f160,plain,
~ neq(s1,p2_1),
inference(consistent_polarity_flipping,[],[f54]) ).
fof(f161,plain,
~ neq(s2,truck1),
inference(consistent_polarity_flipping,[],[f55]) ).
fof(f162,plain,
~ neq(s2,truck2),
inference(consistent_polarity_flipping,[],[f56]) ).
fof(f163,plain,
~ neq(s2,s0),
inference(consistent_polarity_flipping,[],[f57]) ).
fof(f164,plain,
~ neq(s2,s1),
inference(consistent_polarity_flipping,[],[f58]) ).
fof(f165,plain,
neq(s2,s2),
inference(consistent_polarity_flipping,[],[f59]) ).
fof(f166,plain,
~ neq(s2,p1_0),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f167,plain,
~ neq(s2,p2_0),
inference(consistent_polarity_flipping,[],[f61]) ).
fof(f168,plain,
~ neq(s2,p2_1),
inference(consistent_polarity_flipping,[],[f62]) ).
fof(f169,plain,
~ neq(p1_0,truck1),
inference(consistent_polarity_flipping,[],[f63]) ).
fof(f170,plain,
~ neq(p1_0,truck2),
inference(consistent_polarity_flipping,[],[f64]) ).
fof(f171,plain,
~ neq(p1_0,s0),
inference(consistent_polarity_flipping,[],[f65]) ).
fof(f172,plain,
~ neq(p1_0,s1),
inference(consistent_polarity_flipping,[],[f66]) ).
fof(f173,plain,
~ neq(p1_0,s2),
inference(consistent_polarity_flipping,[],[f67]) ).
fof(f174,plain,
neq(p1_0,p1_0),
inference(consistent_polarity_flipping,[],[f68]) ).
fof(f175,plain,
~ neq(p1_0,p2_0),
inference(consistent_polarity_flipping,[],[f69]) ).
fof(f176,plain,
~ neq(p1_0,p2_1),
inference(consistent_polarity_flipping,[],[f70]) ).
fof(f177,plain,
~ neq(p2_0,truck1),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f178,plain,
~ neq(p2_0,truck2),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f179,plain,
~ neq(p2_0,s0),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f180,plain,
~ neq(p2_0,s1),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f181,plain,
~ neq(p2_0,s2),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f182,plain,
~ neq(p2_0,p1_0),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f183,plain,
neq(p2_0,p2_0),
inference(consistent_polarity_flipping,[],[f77]) ).
fof(f184,plain,
~ neq(p2_0,p2_1),
inference(consistent_polarity_flipping,[],[f78]) ).
fof(f185,plain,
~ neq(p2_1,truck1),
inference(consistent_polarity_flipping,[],[f79]) ).
fof(f186,plain,
~ neq(p2_1,truck2),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f187,plain,
~ neq(p2_1,s0),
inference(consistent_polarity_flipping,[],[f81]) ).
fof(f188,plain,
~ neq(p2_1,s1),
inference(consistent_polarity_flipping,[],[f82]) ).
fof(f189,plain,
~ neq(p2_1,s2),
inference(consistent_polarity_flipping,[],[f83]) ).
fof(f190,plain,
~ neq(p2_1,p1_0),
inference(consistent_polarity_flipping,[],[f84]) ).
fof(f191,plain,
~ neq(p2_1,p2_0),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f192,plain,
neq(p2_1,p2_1),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f193,plain,
~ s(s2,s2,s0,s1,s0,s2),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f194,plain,
s(s2,s1,s2,s2,s2,s0),
inference(consistent_polarity_flipping,[],[f106]) ).
fof(f323,plain,
$false,
inference(finite_model_not_found_(exhaustively_excluded_all_possible_domain_size_assignments),[],[f107,f108,f109,f110,f111,f112,f113,f114,f115,f116,f117,f118,f119,f120,f121,f122,f123,f124,f125,f126,f127,f128,f129,f130,f131,f132,f133,f134,f135,f136,f137,f138,f139,f140,f141,f142,f143,f144,f145,f146,f147,f148,f149,f150,f151,f152,f153,f154,f155,f156,f157,f158,f159,f160,f161,f162,f163,f164,f165,f166,f167,f168,f169,f170,f171,f172,f173,f174,f175,f176,f177,f178,f179,f180,f181,f182,f183,f184,f185,f186,f187,f188,f189,f190,f191,f192,f87,f88,f89,f90,f91,f92,f93,f94,f95,f96,f97,f98,f99,f100,f101,f102,f103,f104,f193,f194]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PLA031-1.001 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.15/0.41 % Computer : n018.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Sun Sep 27 22:13:24 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.15/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.15/0.46 Running first-order model finding
% 0.15/0.46 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
% 8.59/1.95 % (2785432)Will run a generic schedule for satisfiability detection.
% 8.59/1.95 % (2785443)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2283174214:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.59/1.95 % (2785445)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=809698370:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.59/1.95 % (2785440)% WARNING: option uhcvi not known.
% 8.59/1.95 % (2785444)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3968943105:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.59/1.95 % (2785439)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1447046655_2999 on theBenchmark for (2999ds/0Mi)
% 8.59/1.95 % (2785440)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=360256340:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.59/1.95 % (2785441)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3256676660:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.59/1.95 % (2785442)dis+10_1_sil=32000:sp=arity:random_seed=539519082:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.59/1.95 % Detected minimum model sizes of [1]
% 8.59/1.95 % Detected maximum model sizes of [8]
% 8.59/1.95 % TRYING [1]
% 8.59/1.95 % TRYING [2]
% 8.59/1.95 % TRYING [3]
% 8.59/1.95 % (2785443)Instruction limit reached!
% 8.59/1.95 % (2785443)------------------------------
% 8.59/1.95 % (2785443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.59/1.95 % (2785443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/1.95 % (2785443)CaDiCaL version: 2.1.3
% 8.59/1.95 % (2785443)Termination reason: Instruction limit
% 8.59/1.95 % (2785443)Termination phase: Saturation
% 8.59/1.95 % (2785443)Time elapsed: 0.047 s
% 8.59/1.95 % (2785443)Peak memory usage: 12 MB
% 8.59/1.95 % (2785443)Instructions burned: 121 (million)
% 8.59/1.95 % (2785453)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2415927200:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 8.59/1.95 % Detected minimum model sizes of [1]
% 8.59/1.95 % Detected maximum model sizes of [8]
% 8.59/1.95 % TRYING [1]
% 8.59/1.95 % TRYING [2]
% 8.59/1.95 % TRYING [3]
% 8.59/1.95 % TRYING [4]
% 8.59/1.95 % TRYING [4]
% 8.59/1.95 % (2785444)Instruction limit reached!
% 8.59/1.95 % (2785444)------------------------------
% 8.59/1.95 % (2785444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.59/1.95 % (2785444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/1.95 % (2785444)CaDiCaL version: 2.1.3
% 8.59/1.95 % (2785444)Termination reason: Instruction limit
% 8.59/1.95 % (2785444)Termination phase: Saturation
% 8.59/1.95 % (2785444)Time elapsed: 0.100 s
% 8.59/1.95 % (2785444)Peak memory usage: 11 MB
% 8.59/1.95 % (2785444)Instructions burned: 132 (million)
% 8.59/1.95 % (2785442)Instruction limit reached!
% 8.59/1.95 % (2785442)------------------------------
% 8.59/1.95 % (2785442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.59/1.95 % (2785442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/1.95 % (2785442)CaDiCaL version: 2.1.3
% 8.59/1.95 % (2785442)Termination reason: Instruction limit
% 8.59/1.95 % (2785442)Termination phase: Saturation
% 8.59/1.95 % (2785442)Time elapsed: 0.103 s
% 8.59/1.95 % (2785442)Peak memory usage: 12 MB
% 8.59/1.95 % (2785442)Instructions burned: 103 (million)
% 8.59/1.95 % (2785456)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3694426549:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.59/1.95 % (2785457)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=2223689482:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.59/1.95 % (2785445)Instruction limit reached!
% 8.59/1.95 % (2785445)------------------------------
% 8.59/1.95 % (2785445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.59/1.95 % (2785445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/1.95 % (2785445)CaDiCaL version: 2.1.3
% 8.59/1.95 % (2785445)Termination reason: Instruction limit
% 8.59/1.95 % (2785445)Termination phase: Saturation
% 8.59/1.95 % (2785445)Time elapsed: 0.146 s
% 8.59/1.95 % (2785445)Peak memory usage: 13 MB
% 8.59/1.95 % (2785445)Instructions burned: 159 (million)
% 8.59/1.95 % (2785462)ott-21_1_sil=16000:fs=off:random_seed=2865296220:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.59/1.95 % TRYING [5]
% 8.59/1.95 % (2785456)Instruction limit reached!
% 22.93/3.79 % (2785456)------------------------------
% 22.93/3.79 % (2785456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.93/3.79 % (2785456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.79 % (2785456)CaDiCaL version: 2.1.3
% 22.93/3.79 % (2785456)Termination reason: Instruction limit
% 22.93/3.79 % (2785456)Termination phase: Saturation
% 22.93/3.79 % (2785456)Time elapsed: 0.106 s
% 22.93/3.79 % (2785456)Peak memory usage: 11 MB
% 22.93/3.79 % (2785456)Instructions burned: 131 (million)
% 22.93/3.79 % (2785466)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1556194:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 22.93/3.79 % (2785453)Instruction limit reached!
% 22.93/3.79 % (2785453)------------------------------
% 22.93/3.79 % (2785453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.93/3.79 % (2785453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.79 % (2785453)CaDiCaL version: 2.1.3
% 22.93/3.79 % (2785453)Termination reason: Instruction limit
% 22.93/3.79 % (2785453)Termination phase: Finite model building constraint generation
% 22.93/3.79 % (2785453)Time elapsed: 0.227 s
% 22.93/3.79 % (2785453)Peak memory usage: 29 MB
% 22.93/3.79 % (2785453)Instructions burned: 715 (million)
% 22.93/3.79 % (2785468)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1757758435:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 22.93/3.79 % TRYING [5]
% 22.93/3.79 % Detected minimum model sizes of [1]
% 22.93/3.79 % Detected maximum model sizes of [8]
% 22.93/3.79 % TRYING [1]
% 22.93/3.79 % TRYING [2]
% 22.93/3.79 % TRYING [3]
% 22.93/3.79 % (2785462)Instruction limit reached!
% 22.93/3.79 % (2785462)------------------------------
% 22.93/3.79 % (2785462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.93/3.79 % (2785462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.79 % (2785462)CaDiCaL version: 2.1.3
% 22.93/3.79 % (2785462)Termination reason: Instruction limit
% 22.93/3.79 % (2785462)Termination phase: Saturation
% 22.93/3.79 % (2785462)Time elapsed: 0.159 s
% 22.93/3.79 % (2785462)Peak memory usage: 12 MB
% 22.93/3.79 % (2785462)Instructions burned: 180 (million)
% 22.93/3.79 % TRYING [4]
% 22.93/3.79 % (2785470)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=119495594:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 22.93/3.79 % (2785466)Instruction limit reached!
% 22.93/3.79 % (2785466)------------------------------
% 22.93/3.79 % (2785466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.93/3.79 % (2785466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.79 % (2785466)CaDiCaL version: 2.1.3
% 22.93/3.79 % (2785466)Termination reason: Instruction limit
% 22.93/3.79 % (2785466)Termination phase: Saturation
% 22.93/3.79 % (2785466)Time elapsed: 0.354 s
% 22.93/3.79 % (2785466)Peak memory usage: 15 MB
% 22.93/3.79 % (2785466)Instructions burned: 477 (million)
% 22.93/3.79 % (2785477)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3096506035:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 22.93/3.79 % Detected minimum model sizes of [1]
% 22.93/3.79 % Detected maximum model sizes of [8]
% 22.93/3.79 % fmb_start_size (= 14) larger than a detected sort maximum size!
% 22.93/3.79 % (2785477)Refutation not found, incomplete strategy
% 22.93/3.79 % (2785477)------------------------------
% 22.93/3.79 % (2785477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.93/3.79 % (2785477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.79 % (2785477)CaDiCaL version: 2.1.3
% 22.93/3.79 % (2785477)Termination reason: Refutation not found, incomplete strategy
% 22.93/3.79 % (2785477)Time elapsed: 0.002 s
% 22.93/3.79 % (2785477)Peak memory usage: 10 MB
% 22.93/3.79 % (2785477)Instructions burned: 5 (million)
% 22.93/3.79 % (2785477)------------------------------
% 22.93/3.79 % (2785477)------------------------------
% 22.93/3.79 % (2785457)Instruction limit reached!
% 22.93/3.79 % (2785457)------------------------------
% 22.93/3.79 % (2785457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.93/3.79 % (2785457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.79 % (2785457)CaDiCaL version: 2.1.3
% 22.93/3.79 % (2785457)Termination reason: Instruction limit
% 22.93/3.79 % (2785457)Termination phase: Saturation
% 22.93/3.79 % (2785457)Time elapsed: 0.526 s
% 22.93/3.79 % (2785457)Peak memory usage: 18 MB
% 22.93/3.79 % (2785457)Instructions burned: 685 (million)
% 22.93/3.79 % (2785480)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1172488332:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 23.94/8.34 % (2785481)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2254463057:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 23.94/8.34 % TRYING [5]
% 23.94/8.34 % (2785468)Instruction limit reached!
% 23.94/8.34 % (2785468)------------------------------
% 23.94/8.34 % (2785468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785468)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785468)Termination reason: Instruction limit
% 23.94/8.34 % (2785468)Termination phase: Finite model building constraint generation
% 23.94/8.34 % (2785468)Time elapsed: 0.594 s
% 23.94/8.34 % (2785468)Peak memory usage: 32 MB
% 23.94/8.34 % (2785468)Instructions burned: 865 (million)
% 23.94/8.34 % (2785486)fmb+10_1_sil=64000:random_seed=3250002611:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 23.94/8.34 % Detected minimum model sizes of [1]
% 23.94/8.34 % Detected maximum model sizes of [8]
% 23.94/8.34 % TRYING [1]
% 23.94/8.34 % TRYING [2]
% 23.94/8.34 % TRYING [3]
% 23.94/8.34 % (2785480)Instruction limit reached!
% 23.94/8.34 % (2785480)------------------------------
% 23.94/8.34 % (2785480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785480)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785480)Termination reason: Instruction limit
% 23.94/8.34 % (2785480)Termination phase: Saturation
% 23.94/8.34 % (2785480)Time elapsed: 0.342 s
% 23.94/8.34 % (2785480)Peak memory usage: 20 MB
% 23.94/8.34 % (2785480)Instructions burned: 693 (million)
% 23.94/8.34 % TRYING [4]
% 23.94/8.34 % (2785489)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3061183002:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 23.94/8.34 % Detected minimum model sizes of [1]
% 23.94/8.34 % Detected maximum model sizes of [8]
% 23.94/8.34 % fmb_start_size (= 20) larger than a detected sort maximum size!
% 23.94/8.34 % (2785489)Refutation not found, incomplete strategy
% 23.94/8.34 % (2785489)------------------------------
% 23.94/8.34 % (2785489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785489)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785489)Termination reason: Refutation not found, incomplete strategy
% 23.94/8.34 % (2785489)Time elapsed: 0.002 s
% 23.94/8.34 % (2785489)Peak memory usage: 10 MB
% 23.94/8.34 % (2785489)Instructions burned: 5 (million)
% 23.94/8.34 % (2785489)------------------------------
% 23.94/8.34 % (2785489)------------------------------
% 23.94/8.34 % (2785492)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1990346181:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 23.94/8.34 % Detected minimum model sizes of [1]
% 23.94/8.34 % Detected maximum model sizes of [8]
% 23.94/8.34 % TRYING [8]
% 23.94/8.34 % TRYING [6]
% 23.94/8.34 % TRYING [5]
% 23.94/8.34 % (2785481)Instruction limit reached!
% 23.94/8.34 % (2785481)------------------------------
% 23.94/8.34 % (2785481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785481)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785481)Termination reason: Instruction limit
% 23.94/8.34 % (2785481)Termination phase: Saturation
% 23.94/8.34 % (2785481)Time elapsed: 0.709 s
% 23.94/8.34 % (2785481)Peak memory usage: 16 MB
% 23.94/8.34 % (2785481)Instructions burned: 879 (million)
% 23.94/8.34 % (2785492)Instruction limit reached!
% 23.94/8.34 % (2785492)------------------------------
% 23.94/8.34 % (2785492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785492)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785492)Termination reason: Instruction limit
% 23.94/8.34 % (2785492)Termination phase: Finite model building constraint generation
% 23.94/8.34 % (2785492)Time elapsed: 0.339 s
% 23.94/8.34 % (2785492)Peak memory usage: 60 MB
% 23.94/8.34 % (2785492)Instructions burned: 926 (million)
% 23.94/8.34 % (2785498)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1937834799:i=5131_2985 on theBenchmark for (2985ds/5131Mi)
% 23.94/8.34 % (2785499)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3588957662:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 23.94/8.34 % (2785470)Instruction limit reached!
% 23.94/8.34 % (2785470)------------------------------
% 23.94/8.34 % (2785470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785470)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785470)Termination reason: Instruction limit
% 23.94/8.34 % (2785470)Termination phase: Saturation
% 23.94/8.34 % (2785470)Time elapsed: 1.249 s
% 23.94/8.34 % (2785470)Peak memory usage: 21 MB
% 23.94/8.34 % (2785470)Instructions burned: 1179 (million)
% 23.94/8.34 % (2785502)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2822543542:i=6324_2983 on theBenchmark for (2983ds/6324Mi)
% 23.94/8.34 % Detected minimum model sizes of [1]
% 23.94/8.34 % Detected maximum model sizes of [8]
% 23.94/8.34 % fmb_start_size (= 77) larger than a detected sort maximum size!
% 23.94/8.34 % (2785502)Refutation not found, incomplete strategy
% 23.94/8.34 % (2785502)------------------------------
% 23.94/8.34 % (2785502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785502)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785502)Termination reason: Refutation not found, incomplete strategy
% 23.94/8.34 % (2785502)Time elapsed: 0.006 s
% 23.94/8.34 % (2785502)Peak memory usage: 10 MB
% 23.94/8.34 % (2785502)Instructions burned: 6 (million)
% 23.94/8.34 % (2785502)------------------------------
% 23.94/8.34 % (2785502)------------------------------
% 23.94/8.34 % (2785504)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=588936658:fmbsr=2.30978:i=2174_2982 on theBenchmark for (2982ds/2174Mi)
% 23.94/8.34 % Detected minimum model sizes of [1]
% 23.94/8.34 % Detected maximum model sizes of [8]
% 23.94/8.34 % fmb_start_size (= 16) larger than a detected sort maximum size!
% 23.94/8.34 % (2785504)Refutation not found, incomplete strategy
% 23.94/8.34 % (2785504)------------------------------
% 23.94/8.34 % (2785504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785504)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785504)Termination reason: Refutation not found, incomplete strategy
% 23.94/8.34 % (2785504)Time elapsed: 0.005 s
% 23.94/8.34 % (2785504)Peak memory usage: 10 MB
% 23.94/8.34 % (2785504)Instructions burned: 5 (million)
% 23.94/8.34 % (2785504)------------------------------
% 23.94/8.34 % (2785504)------------------------------
% 23.94/8.34 % (2785506)ott-2_1_sil=16000:newcnf=on:random_seed=1904013407:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2982 on theBenchmark for (2982ds/869Mi)
% 23.94/8.34 % TRYING [6]
% 23.94/8.34 % (2785506)Instruction limit reached!
% 23.94/8.34 % (2785506)------------------------------
% 23.94/8.34 % (2785506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785506)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785506)Termination reason: Instruction limit
% 23.94/8.34 % (2785506)Termination phase: Saturation
% 23.94/8.34 % (2785506)Time elapsed: 0.572 s
% 23.94/8.34 % (2785506)Peak memory usage: 18 MB
% 23.94/8.34 % (2785506)Instructions burned: 870 (million)
% 23.94/8.34 % (2785572)ott+10_1_sil=32000:tgt=ground:random_seed=1474770857:i=5114:av=off_2976 on theBenchmark for (2976ds/5114Mi)
% 23.94/8.34 % (2785499)Instruction limit reached!
% 23.94/8.34 % (2785499)------------------------------
% 23.94/8.34 % (2785499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785499)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785499)Termination reason: Instruction limit
% 23.94/8.34 % (2785499)Termination phase: Saturation
% 23.94/8.34 % (2785499)Time elapsed: 0.947 s
% 23.94/8.34 % (2785499)Peak memory usage: 20 MB
% 23.94/8.34 % (2785499)Instructions burned: 1473 (million)
% 23.94/8.34 % (2785600)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1786768432:i=54282_2975 on theBenchmark for (2975ds/54282Mi)
% 23.94/8.34 % Detected minimum model sizes of [1]
% 23.94/8.34 % Detected maximum model sizes of [8]
% 23.94/8.34 % TRYING [1]
% 23.94/8.34 % TRYING [2]
% 23.94/8.34 % TRYING [3]
% 23.94/8.34 % TRYING [4]
% 23.94/8.34 % TRYING [5]
% 23.94/8.34 % TRYING [6]
% 23.94/8.34 % TRYING [7]
% 23.94/8.34 % (2785498)Instruction limit reached!
% 23.94/8.34 % (2785498)------------------------------
% 23.94/8.34 % (2785498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785498)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785498)Termination reason: Instruction limit
% 23.94/8.34 % (2785498)Termination phase: Saturation
% 23.94/8.34 % (2785498)Time elapsed: 1.867 s
% 23.94/8.34 % (2785498)Peak memory usage: 36 MB
% 23.94/8.34 % (2785498)Instructions burned: 5132 (million)
% 23.94/8.34 % (2785666)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2028385590:i=3512:aac=none_2966 on theBenchmark for (2966ds/3512Mi)
% 23.94/8.34 % (2785666)Instruction limit reached!
% 23.94/8.34 % (2785666)------------------------------
% 23.94/8.34 % (2785666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785666)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785666)Termination reason: Instruction limit
% 23.94/8.34 % (2785666)Termination phase: Saturation
% 23.94/8.34 % (2785666)Time elapsed: 1.165 s
% 23.94/8.34 % (2785666)Peak memory usage: 32 MB
% 23.94/8.34 % (2785666)Instructions burned: 3512 (million)
% 23.94/8.34 % (2785668)dis+21_1_sil=32000:sas=cadical:random_seed=346845749:i=3773:amm=off_2955 on theBenchmark for (2955ds/3773Mi)
% 23.94/8.34 % TRYING [7]
% 23.94/8.34 % TRYING [7]
% 23.94/8.34 % (2785668)Instruction limit reached!
% 23.94/8.34 % (2785668)------------------------------
% 23.94/8.34 % (2785668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785668)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785668)Termination reason: Instruction limit
% 23.94/8.34 % (2785668)Termination phase: Saturation
% 23.94/8.34 % (2785668)Time elapsed: 1.254 s
% 23.94/8.34 % (2785668)Peak memory usage: 41 MB
% 23.94/8.34 % (2785668)Instructions burned: 3775 (million)
% 23.94/8.34 % (2785670)ott+11_1_sil=16000:gs=on:random_seed=81213308:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2942 on theBenchmark for (2942ds/2251Mi)
% 23.94/8.34 % (2785572)Instruction limit reached!
% 23.94/8.34 % (2785572)------------------------------
% 23.94/8.34 % (2785572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785572)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785572)Termination reason: Instruction limit
% 23.94/8.34 % (2785572)Termination phase: Saturation
% 23.94/8.34 % (2785572)Time elapsed: 3.427 s
% 23.94/8.34 % (2785572)Peak memory usage: 43 MB
% 23.94/8.34 % (2785572)Instructions burned: 5115 (million)
% 23.94/8.34 % (2785672)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2851026014:fmbsr=1.6:i=67534_2942 on theBenchmark for (2942ds/67534Mi)
% 23.94/8.34 % Detected minimum model sizes of [1]
% 23.94/8.34 % Detected maximum model sizes of [8]
% 23.94/8.34 % TRYING [7]
% 23.94/8.34 % (2785670)Instruction limit reached!
% 23.94/8.34 % (2785670)------------------------------
% 23.94/8.34 % (2785670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785670)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785670)Termination reason: Instruction limit
% 23.94/8.34 % (2785670)Termination phase: Saturation
% 23.94/8.34 % (2785670)Time elapsed: 0.719 s
% 23.94/8.34 % (2785670)Peak memory usage: 107 MB
% 23.94/8.34 % (2785670)Instructions burned: 2252 (million)
% 23.94/8.34 % (2785674)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=381269854:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2934 on theBenchmark for (2934ds/4591Mi)
% 23.94/8.34 % (2785439) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2785432-2785439"...
% 23.94/8.34 % (2785439)...printing done.
% 23.94/8.34 % (2785439)Refutation found. Thanks to Tanya!
% 23.94/8.34 % SZS status Unsatisfiable for theBenchmark
% 23.94/8.34 % SZS output start Proof for theBenchmark
% See solution above
% 23.94/8.34 % (2785439)------------------------------
% 23.94/8.34 % (2785439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/8.34 % (2785439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/8.34 % (2785439)CaDiCaL version: 2.1.3
% 23.94/8.34 % (2785439)Termination reason: Refutation
% 23.94/8.34 % (2785439)Time elapsed: 7.720 s
% 23.94/8.34 % (2785439)Peak memory usage: 451 MB
% 23.94/8.34 % (2785439)Instructions burned: 17424 (million)
% 23.94/8.34 % (2785432)Success in time 7.863 s
% 23.94/8.34 % Vampire exiting
%------------------------------------------------------------------------------