%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV420-1.010 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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 01:21:55 PM UTC 2026
% Result : Unsatisfiable 135.41s 19.34s
% Output : Refutation 135.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 1
% Number of leaves : 388
% Syntax : Number of formulae : 389 ( 20 unt; 0 def)
% Number of atoms : 1030 ( 0 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 1253 ( 612 ~; 641 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 104 ( 103 usr; 2 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 26 con; 0-0 aty)
% Number of variables : 693 ( 693 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
succ(s0,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound1) ).
fof(f2,axiom,
succ(s1,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound2) ).
fof(f3,axiom,
succ(s2,s3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound3) ).
fof(f4,axiom,
succ(s3,s4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound4) ).
fof(f5,axiom,
succ(s4,s5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound5) ).
fof(f6,axiom,
succ(s5,s6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound6) ).
fof(f7,axiom,
succ(s6,s7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound7) ).
fof(f8,axiom,
succ(s7,s8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound8) ).
fof(f9,axiom,
succ(s8,s9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound9) ).
fof(f10,axiom,
last(s9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound10) ).
fof(f11,axiom,
! [X0,X1] :
( ~ succ(X0,X1)
| trans(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound11) ).
fof(f12,axiom,
( ~ loop
| trans(s9,s0)
| trans(s9,s1)
| trans(s9,s2)
| trans(s9,s3)
| trans(s9,s4)
| trans(s9,s5)
| trans(s9,s6)
| trans(s9,s7)
| trans(s9,s8)
| trans(s9,s9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound12) ).
fof(f13,axiom,
! [X0] :
( m_main_v_CMD(X0,c_idle)
| m_main_v_CMD(X0,c_read_h_shared)
| m_main_v_CMD(X0,c_read_h_owned)
| m_main_v_CMD(X0,c_write_h_invalid)
| m_main_v_CMD(X0,c_write_h_shared)
| m_main_v_CMD(X0,c_write_h_resp_h_invalid)
| m_main_v_CMD(X0,c_write_h_resp_h_shared)
| m_main_v_CMD(X0,c_invalidate)
| m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_1) ).
fof(f14,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_read_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_2) ).
fof(f15,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_read_h_owned) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_3) ).
fof(f16,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_write_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_4) ).
fof(f17,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_write_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_5) ).
fof(f18,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_6) ).
fof(f19,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_7) ).
fof(f20,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_8) ).
fof(f21,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_9) ).
fof(f22,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_shared)
| ~ m_main_v_CMD(X0,c_read_h_owned) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_10) ).
fof(f23,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_shared)
| ~ m_main_v_CMD(X0,c_write_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_11) ).
fof(f24,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_shared)
| ~ m_main_v_CMD(X0,c_write_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_12) ).
fof(f25,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_shared)
| ~ m_main_v_CMD(X0,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_13) ).
fof(f26,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_shared)
| ~ m_main_v_CMD(X0,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_14) ).
fof(f27,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_shared)
| ~ m_main_v_CMD(X0,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_15) ).
fof(f28,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_shared)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_16) ).
fof(f29,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_owned)
| ~ m_main_v_CMD(X0,c_write_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_17) ).
fof(f30,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_owned)
| ~ m_main_v_CMD(X0,c_write_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_18) ).
fof(f31,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_owned)
| ~ m_main_v_CMD(X0,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_19) ).
fof(f32,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_owned)
| ~ m_main_v_CMD(X0,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_20) ).
fof(f33,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_owned)
| ~ m_main_v_CMD(X0,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_21) ).
fof(f34,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_owned)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_22) ).
fof(f35,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_invalid)
| ~ m_main_v_CMD(X0,c_write_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_23) ).
fof(f36,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_invalid)
| ~ m_main_v_CMD(X0,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_24) ).
fof(f37,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_invalid)
| ~ m_main_v_CMD(X0,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_25) ).
fof(f38,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_invalid)
| ~ m_main_v_CMD(X0,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_26) ).
fof(f39,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_invalid)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_27) ).
fof(f40,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_shared)
| ~ m_main_v_CMD(X0,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_28) ).
fof(f41,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_shared)
| ~ m_main_v_CMD(X0,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_29) ).
fof(f42,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_shared)
| ~ m_main_v_CMD(X0,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_30) ).
fof(f43,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_shared)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_31) ).
fof(f44,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_resp_h_invalid)
| ~ m_main_v_CMD(X0,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_32) ).
fof(f45,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_resp_h_invalid)
| ~ m_main_v_CMD(X0,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_33) ).
fof(f46,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_resp_h_invalid)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_34) ).
fof(f47,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_resp_h_shared)
| ~ m_main_v_CMD(X0,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_35) ).
fof(f48,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_resp_h_shared)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_36) ).
fof(f49,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_invalidate)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_37) ).
fof(f50,axiom,
! [X0,X1] :
( m_memory_v_CMD(c_m,X0,X1)
| ~ m_main_v_CMD(X0,X1)
| ~ node1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_38) ).
fof(f51,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(c_m,X0,X1)
| m_main_v_CMD(X0,X1)
| ~ node1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_39) ).
fof(f52,axiom,
! [X0] : node1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_40) ).
fof(f53,axiom,
! [X0] :
( m_memory_v_REPLY_h_OWNED(c_m,X0)
| ~ m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_41) ).
fof(f54,axiom,
! [X0] :
( ~ m_memory_v_REPLY_h_OWNED(c_m,X0)
| m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_42) ).
fof(f55,axiom,
! [X0] :
( m_memory_v_REPLY_h_WAITING(c_m,X0)
| ~ m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_43) ).
fof(f56,axiom,
! [X0] :
( ~ m_memory_v_REPLY_h_WAITING(c_m,X0)
| m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_44) ).
fof(f57,axiom,
! [X0] :
( m_memory_v_REPLY_h_STALL(c_m,X0)
| ~ m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_45) ).
fof(f58,axiom,
! [X0] :
( ~ m_memory_v_REPLY_h_STALL(c_m,X0)
| m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_46) ).
fof(f59,axiom,
! [X0,X1] :
( m_processor_v_CMD(c_p0,X0,X1)
| ~ m_main_v_CMD(X0,X1)
| ~ node2(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_47) ).
fof(f60,axiom,
! [X0,X1] :
( ~ m_processor_v_CMD(c_p0,X0,X1)
| m_main_v_CMD(X0,X1)
| ~ node2(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_48) ).
fof(f61,axiom,
! [X0] : node2(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_49) ).
fof(f62,axiom,
! [X0] :
( m_processor_v_REPLY_h_OWNED(c_p0,X0)
| ~ m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_50) ).
fof(f63,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_OWNED(c_p0,X0)
| m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_51) ).
fof(f64,axiom,
! [X0] :
( m_processor_v_REPLY_h_WAITING(c_p0,X0)
| ~ m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_52) ).
fof(f65,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_WAITING(c_p0,X0)
| m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_53) ).
fof(f66,axiom,
! [X0] :
( m_processor_v_REPLY_h_STALL(c_p0,X0)
| ~ m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_54) ).
fof(f67,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_STALL(c_p0,X0)
| m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_55) ).
fof(f68,axiom,
! [X0,X1] :
( m_processor_v_CMD(c_p1,X0,X1)
| ~ m_main_v_CMD(X0,X1)
| ~ node3(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_56) ).
fof(f69,axiom,
! [X0,X1] :
( ~ m_processor_v_CMD(c_p1,X0,X1)
| m_main_v_CMD(X0,X1)
| ~ node3(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_57) ).
fof(f70,axiom,
! [X0] : node3(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_58) ).
fof(f71,axiom,
! [X0] :
( m_processor_v_REPLY_h_OWNED(c_p1,X0)
| ~ m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_59) ).
fof(f72,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_OWNED(c_p1,X0)
| m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_60) ).
fof(f73,axiom,
! [X0] :
( m_processor_v_REPLY_h_WAITING(c_p1,X0)
| ~ m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_61) ).
fof(f74,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_WAITING(c_p1,X0)
| m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_62) ).
fof(f75,axiom,
! [X0] :
( m_processor_v_REPLY_h_STALL(c_p1,X0)
| ~ m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_63) ).
fof(f76,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_STALL(c_p1,X0)
| m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_64) ).
fof(f77,axiom,
! [X0,X1] :
( m_processor_v_CMD(c_p2,X0,X1)
| ~ m_main_v_CMD(X0,X1)
| ~ node4(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_65) ).
fof(f78,axiom,
! [X0,X1] :
( ~ m_processor_v_CMD(c_p2,X0,X1)
| m_main_v_CMD(X0,X1)
| ~ node4(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_66) ).
fof(f79,axiom,
! [X0] : node4(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_67) ).
fof(f80,axiom,
! [X0] :
( m_processor_v_REPLY_h_OWNED(c_p2,X0)
| ~ m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_68) ).
fof(f81,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_OWNED(c_p2,X0)
| m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_69) ).
fof(f82,axiom,
! [X0] :
( m_processor_v_REPLY_h_WAITING(c_p2,X0)
| ~ m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_70) ).
fof(f83,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_WAITING(c_p2,X0)
| m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_71) ).
fof(f84,axiom,
! [X0] :
( m_processor_v_REPLY_h_STALL(c_p2,X0)
| ~ m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_72) ).
fof(f85,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_STALL(c_p2,X0)
| m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_73) ).
fof(f86,axiom,
! [X0] :
( ~ m_processor_v_reply_h_owned(c_p0,X0)
| ~ node5(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_74) ).
fof(f87,axiom,
! [X0] :
( ~ m_processor_v_reply_h_owned(c_p1,X0)
| ~ node5(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_75) ).
fof(f88,axiom,
! [X0] :
( ~ m_processor_v_reply_h_owned(c_p2,X0)
| ~ node5(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_76) ).
fof(f89,axiom,
! [X0] :
( m_main_v_REPLY_h_OWNED(X0)
| node5(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_77) ).
fof(f90,axiom,
! [X0] :
( ~ m_main_v_REPLY_h_OWNED(X0)
| m_processor_v_reply_h_owned(c_p0,X0)
| m_processor_v_reply_h_owned(c_p1,X0)
| m_processor_v_reply_h_owned(c_p2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_78) ).
fof(f91,axiom,
! [X0] :
( ~ m_processor_v_reply_h_waiting(c_p0,X0)
| ~ node6(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_79) ).
fof(f92,axiom,
! [X0] :
( ~ m_processor_v_reply_h_waiting(c_p1,X0)
| ~ node6(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_80) ).
fof(f93,axiom,
! [X0] :
( ~ m_processor_v_reply_h_waiting(c_p2,X0)
| ~ node6(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_81) ).
fof(f94,axiom,
! [X0] :
( m_main_v_REPLY_h_WAITING(X0)
| node6(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_82) ).
fof(f95,axiom,
! [X0] :
( ~ m_main_v_REPLY_h_WAITING(X0)
| m_processor_v_reply_h_waiting(c_p0,X0)
| m_processor_v_reply_h_waiting(c_p1,X0)
| m_processor_v_reply_h_waiting(c_p2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_83) ).
fof(f96,axiom,
! [X0] :
( ~ m_processor_v_reply_h_stall(c_p0,X0)
| ~ node7(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_84) ).
fof(f97,axiom,
! [X0] :
( ~ m_processor_v_reply_h_stall(c_p1,X0)
| ~ node7(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_85) ).
fof(f98,axiom,
! [X0] :
( ~ m_processor_v_reply_h_stall(c_p2,X0)
| ~ node7(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_86) ).
fof(f99,axiom,
! [X0] :
( ~ m_memory_v_reply_h_stall(c_m,X0)
| ~ node7(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_87) ).
fof(f100,axiom,
! [X0] :
( m_main_v_REPLY_h_STALL(X0)
| node7(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_88) ).
fof(f101,axiom,
! [X0] :
( ~ m_main_v_REPLY_h_STALL(X0)
| m_processor_v_reply_h_stall(c_p0,X0)
| m_processor_v_reply_h_stall(c_p1,X0)
| m_processor_v_reply_h_stall(c_p2,X0)
| m_memory_v_reply_h_stall(c_m,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_89) ).
fof(f102,axiom,
! [X0,X1] :
( m_main_v_CMD(X0,X1)
| ~ m_processor_v_cmd(c_p0,X0,X1)
| ~ node8(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_90) ).
fof(f103,axiom,
! [X0,X1] :
( ~ m_main_v_CMD(X0,X1)
| m_processor_v_cmd(c_p0,X0,X1)
| ~ node8(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_91) ).
fof(f104,axiom,
! [X0] :
( m_processor_v_cmd(c_p1,X0,c_idle)
| ~ node9(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_92) ).
fof(f105,axiom,
! [X0] :
( m_processor_v_cmd(c_p2,X0,c_idle)
| ~ node9(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_93) ).
fof(f106,axiom,
! [X0] :
( m_memory_v_cmd(c_m,X0,c_idle)
| ~ node9(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_94) ).
fof(f107,axiom,
! [X0,X1] :
( m_main_v_CMD(X0,X1)
| ~ m_processor_v_cmd(c_p1,X0,X1)
| ~ node10(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_95) ).
fof(f108,axiom,
! [X0,X1] :
( ~ m_main_v_CMD(X0,X1)
| m_processor_v_cmd(c_p1,X0,X1)
| ~ node10(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_96) ).
fof(f109,axiom,
! [X0] :
( m_processor_v_cmd(c_p0,X0,c_idle)
| ~ node11(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_97) ).
fof(f110,axiom,
! [X0] :
( m_processor_v_cmd(c_p2,X0,c_idle)
| ~ node11(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_98) ).
fof(f111,axiom,
! [X0] :
( m_memory_v_cmd(c_m,X0,c_idle)
| ~ node11(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_99) ).
fof(f112,axiom,
! [X0,X1] :
( m_main_v_CMD(X0,X1)
| ~ m_processor_v_cmd(c_p0,X0,X1)
| ~ node12(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_100) ).
fof(f113,axiom,
! [X0,X1] :
( ~ m_main_v_CMD(X0,X1)
| m_processor_v_cmd(c_p0,X0,X1)
| ~ node12(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_101) ).
fof(f114,axiom,
! [X0] :
( m_processor_v_cmd(c_p0,X0,c_idle)
| ~ node13(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_102) ).
fof(f115,axiom,
! [X0] :
( m_processor_v_cmd(c_p1,X0,c_idle)
| ~ node13(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_103) ).
fof(f116,axiom,
! [X0] :
( m_memory_v_cmd(c_m,X0,c_idle)
| ~ node13(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_104) ).
fof(f117,axiom,
! [X0,X1] :
( m_main_v_CMD(X0,X1)
| ~ m_memory_v_cmd(c_m,X0,X1)
| ~ node14(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_105) ).
fof(f118,axiom,
! [X0,X1] :
( ~ m_main_v_CMD(X0,X1)
| m_memory_v_cmd(c_m,X0,X1)
| ~ node14(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_106) ).
fof(f119,axiom,
! [X0] :
( m_processor_v_cmd(c_p0,X0,c_idle)
| ~ node15(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_107) ).
fof(f120,axiom,
! [X0] :
( m_processor_v_cmd(c_p1,X0,c_idle)
| ~ node15(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_108) ).
fof(f121,axiom,
! [X0] :
( m_processor_v_cmd(c_p2,X0,c_idle)
| ~ node15(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_109) ).
fof(f122,axiom,
! [X0] :
( ~ m_processor_v_cmd(c_p1,X0,c_idle)
| ~ m_processor_v_cmd(c_p2,X0,c_idle)
| ~ m_memory_v_cmd(c_m,X0,c_idle)
| node8(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_110) ).
fof(f123,axiom,
! [X0] :
( node9(X0)
| ~ m_processor_v_cmd(c_p0,X0,c_idle)
| ~ m_processor_v_cmd(c_p2,X0,c_idle)
| ~ m_memory_v_cmd(c_m,X0,c_idle)
| node10(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_111) ).
fof(f124,axiom,
! [X0] :
( node9(X0)
| node11(X0)
| ~ m_processor_v_cmd(c_p0,X0,c_idle)
| ~ m_processor_v_cmd(c_p1,X0,c_idle)
| ~ m_memory_v_cmd(c_m,X0,c_idle)
| node12(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_112) ).
fof(f125,axiom,
! [X0] :
( node9(X0)
| node11(X0)
| node13(X0)
| ~ m_processor_v_cmd(c_p0,X0,c_idle)
| ~ m_processor_v_cmd(c_p1,X0,c_idle)
| ~ m_processor_v_cmd(c_p2,X0,c_idle)
| node14(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_113) ).
fof(f126,axiom,
! [X0] :
( m_main_v_CMD(X0,c_idle)
| m_main_v_CMD(X0,c_read_h_shared)
| m_main_v_CMD(X0,c_read_h_owned)
| m_main_v_CMD(X0,c_write_h_invalid)
| m_main_v_CMD(X0,c_write_h_shared)
| m_main_v_CMD(X0,c_write_h_resp_h_invalid)
| m_main_v_CMD(X0,c_write_h_resp_h_shared)
| m_main_v_CMD(X0,c_invalidate)
| m_main_v_CMD(X0,c_response)
| node9(X0)
| node11(X0)
| node13(X0)
| node15(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_114) ).
fof(f127,axiom,
! [X0] :
( ~ m_processor_v_master(c_p0,X0)
| m_processor_v_master(c_p0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_115) ).
fof(f128,axiom,
! [X0] :
( ~ m_processor_v_master(c_p0,X0)
| ~ m_processor_v_master(c_p1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_116) ).
fof(f129,axiom,
! [X0] :
( ~ m_processor_v_master(c_p1,X0)
| m_processor_v_master(c_p1,X0)
| m_processor_v_master(c_p0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_117) ).
fof(f130,axiom,
! [X0] :
( ~ m_processor_v_master(c_p0,X0)
| ~ node16(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_118) ).
fof(f131,axiom,
! [X0] :
( ~ m_processor_v_master(c_p1,X0)
| ~ node16(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_119) ).
fof(f132,axiom,
! [X0] :
( node16(X0)
| ~ m_processor_v_master(c_p2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_120) ).
fof(f133,axiom,
! [X0] :
( ~ m_processor_v_master(c_p2,X0)
| m_processor_v_master(c_p2,X0)
| m_processor_v_master(c_p0,X0)
| m_processor_v_master(c_p1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_121) ).
fof(f134,axiom,
! [X0] :
( ~ m_processor_v_master(c_p0,X0)
| ~ node17(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_122) ).
fof(f135,axiom,
! [X0] :
( ~ m_processor_v_master(c_p1,X0)
| ~ node17(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_123) ).
fof(f136,axiom,
! [X0] :
( ~ m_processor_v_master(c_p2,X0)
| ~ node17(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_124) ).
fof(f137,axiom,
! [X0] :
( node17(X0)
| ~ m_memory_v_master(c_m,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_125) ).
fof(f138,axiom,
! [X0] :
( ~ m_memory_v_master(c_m,X0)
| m_memory_v_master(c_m,X0)
| m_processor_v_master(c_p0,X0)
| m_processor_v_master(c_p1,X0)
| m_processor_v_master(c_p2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_126) ).
fof(f139,axiom,
! [X0,X1] :
( m_memory_v_cmd(X0,X1,c_idle)
| m_memory_v_cmd(X0,X1,c_read_h_shared)
| m_memory_v_cmd(X0,X1,c_read_h_owned)
| m_memory_v_cmd(X0,X1,c_write_h_invalid)
| m_memory_v_cmd(X0,X1,c_write_h_shared)
| m_memory_v_cmd(X0,X1,c_write_h_resp_h_invalid)
| m_memory_v_cmd(X0,X1,c_write_h_resp_h_shared)
| m_memory_v_cmd(X0,X1,c_invalidate)
| m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_1) ).
fof(f140,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_cmd(X0,X1,c_read_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_2) ).
fof(f141,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_cmd(X0,X1,c_read_h_owned) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_3) ).
fof(f142,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_cmd(X0,X1,c_write_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_4) ).
fof(f143,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_cmd(X0,X1,c_write_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_5) ).
fof(f144,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_6) ).
fof(f145,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_7) ).
fof(f146,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_8) ).
fof(f147,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_9) ).
fof(f148,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_read_h_owned) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_10) ).
fof(f149,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_write_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_11) ).
fof(f150,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_write_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_12) ).
fof(f151,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_13) ).
fof(f152,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_14) ).
fof(f153,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_15) ).
fof(f154,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_16) ).
fof(f155,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_owned)
| ~ m_memory_v_cmd(X0,X1,c_write_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_17) ).
fof(f156,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_owned)
| ~ m_memory_v_cmd(X0,X1,c_write_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_18) ).
fof(f157,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_owned)
| ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_19) ).
fof(f158,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_owned)
| ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_20) ).
fof(f159,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_owned)
| ~ m_memory_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_21) ).
fof(f160,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_owned)
| ~ m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_22) ).
fof(f161,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_invalid)
| ~ m_memory_v_cmd(X0,X1,c_write_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_23) ).
fof(f162,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_invalid)
| ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_24) ).
fof(f163,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_invalid)
| ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_25) ).
fof(f164,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_invalid)
| ~ m_memory_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_26) ).
fof(f165,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_invalid)
| ~ m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_27) ).
fof(f166,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_28) ).
fof(f167,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_29) ).
fof(f168,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_30) ).
fof(f169,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_31) ).
fof(f170,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_invalid)
| ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_32) ).
fof(f171,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_invalid)
| ~ m_memory_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_33) ).
fof(f172,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_invalid)
| ~ m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_34) ).
fof(f173,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_35) ).
fof(f174,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_resp_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_36) ).
fof(f175,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_invalidate)
| ~ m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_37) ).
fof(f176,axiom,
! [X0] : ~ m_memory_v_busy(X0,s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_38) ).
fof(f177,axiom,
! [X2,X0,X1] :
( m_memory_v_busy(X0,X1)
| ~ m_memory_v_busy(X0,X2)
| ~ node18(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_39) ).
fof(f178,axiom,
! [X2,X0,X1] :
( ~ m_memory_v_busy(X0,X1)
| m_memory_v_busy(X0,X2)
| ~ node18(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_40) ).
fof(f179,axiom,
! [X0,X1] :
( m_memory_v_master(X0,X1)
| ~ node19(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_41) ).
fof(f180,axiom,
! [X0,X1] :
( m_memory_v_CMD(X0,X1,c_response)
| ~ node19(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_42) ).
fof(f181,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_owned)
| ~ node20(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_43) ).
fof(f182,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_shared)
| ~ node20(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_44) ).
fof(f183,axiom,
! [X0,X1] :
( ~ m_memory_v_master(X0,X1)
| ~ node21(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_45) ).
fof(f184,axiom,
! [X0,X1] :
( m_memory_v_CMD(X0,X1,c_read_h_owned)
| m_memory_v_CMD(X0,X1,c_read_h_shared)
| ~ node21(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_46) ).
fof(f185,axiom,
! [X2,X0,X1] :
( m_memory_v_busy(X0,X1)
| ~ m_memory_v_busy(X0,X2)
| ~ node22(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_47) ).
fof(f186,axiom,
! [X2,X0,X1] :
( ~ m_memory_v_busy(X0,X1)
| m_memory_v_busy(X0,X2)
| ~ node22(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_48) ).
fof(f187,axiom,
! [X2,X0,X1] :
( ~ m_memory_v_abort(X0,X1)
| node18(X0,X1,X2)
| ~ node23(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_49) ).
fof(f188,axiom,
! [X2,X0,X1] :
( m_memory_v_abort(X0,X1)
| ~ m_memory_v_master(X0,X1)
| ~ m_memory_v_CMD(X0,X1,c_response)
| ~ m_memory_v_busy(X0,X2)
| ~ node23(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_50) ).
fof(f189,axiom,
! [X2,X0,X1] :
( m_memory_v_abort(X0,X1)
| node19(X0,X1)
| m_memory_v_master(X0,X1)
| node20(X0,X1)
| m_memory_v_busy(X0,X2)
| ~ node23(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_51) ).
fof(f190,axiom,
! [X2,X0,X1] :
( m_memory_v_abort(X0,X1)
| node19(X0,X1)
| node21(X0,X1)
| node22(X0,X1,X2)
| ~ node23(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_52) ).
fof(f191,axiom,
! [X2,X0,X1] :
( ~ trans(X0,X1)
| node23(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_53) ).
fof(f194,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_shared)
| ~ node24(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_56) ).
fof(f195,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_owned)
| ~ node24(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_57) ).
fof(f196,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_shared)
| ~ node25(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_58) ).
fof(f197,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_owned)
| ~ node25(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_59) ).
fof(f198,axiom,
! [X0,X1] :
( ~ m_memory_v_REPLY_h_STALL(X0,X1)
| ~ node26(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_60) ).
fof(f199,axiom,
! [X0,X1] :
( node24(X0,X1)
| ~ m_memory_v_REPLY_h_WAITING(X0,X1)
| ~ node26(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_61) ).
fof(f200,axiom,
! [X0,X1] :
( node25(X0,X1)
| ~ m_memory_v_REPLY_h_OWNED(X0,X1)
| ~ node26(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_62) ).
fof(f201,axiom,
! [X0,X1] :
( m_memory_v_CMD(X0,X1,c_read_h_shared)
| m_memory_v_CMD(X0,X1,c_read_h_owned)
| ~ node27(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_63) ).
fof(f202,axiom,
! [X0,X1] :
( m_memory_v_REPLY_h_WAITING(X0,X1)
| ~ node27(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_64) ).
fof(f203,axiom,
! [X0,X1] :
( m_memory_v_CMD(X0,X1,c_read_h_shared)
| m_memory_v_CMD(X0,X1,c_read_h_owned)
| ~ node28(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_65) ).
fof(f204,axiom,
! [X0,X1] :
( m_memory_v_REPLY_h_OWNED(X0,X1)
| ~ node28(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_66) ).
fof(f205,axiom,
! [X0,X1] :
( m_memory_v_abort(X0,X1)
| node26(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_67) ).
fof(f206,axiom,
! [X0,X1] :
( ~ m_memory_v_abort(X0,X1)
| m_memory_v_REPLY_h_STALL(X0,X1)
| node27(X0,X1)
| node28(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_68) ).
fof(f207,axiom,
! [X0,X1] :
( m_memory_v_master(X0,X1)
| ~ node29(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_69) ).
fof(f208,axiom,
! [X0,X1] :
( m_memory_v_busy(X0,X1)
| ~ node29(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_70) ).
fof(f209,axiom,
! [X0,X1] :
( m_memory_v_cmd(X0,X1,c_response)
| m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_master(X0,X1)
| ~ m_memory_v_busy(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_71) ).
fof(f210,axiom,
! [X0,X1] :
( node29(X0,X1)
| m_memory_v_cmd(X0,X1,c_idle) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_72) ).
fof(f211,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_shared)
| ~ node30(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_73) ).
fof(f212,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_owned)
| ~ node30(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_74) ).
fof(f213,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_write_h_invalid)
| ~ node30(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_75) ).
fof(f214,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_write_h_shared)
| ~ node30(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_76) ).
fof(f215,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_write_h_resp_h_invalid)
| ~ node30(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_77) ).
fof(f216,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_write_h_resp_h_shared)
| ~ node30(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_78) ).
fof(f217,axiom,
! [X0,X1] :
( m_memory_v_busy(X0,X1)
| ~ node31(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_79) ).
fof(f218,axiom,
! [X0,X1] :
( m_memory_v_CMD(X0,X1,c_read_h_shared)
| m_memory_v_CMD(X0,X1,c_read_h_owned)
| m_memory_v_CMD(X0,X1,c_write_h_invalid)
| m_memory_v_CMD(X0,X1,c_write_h_shared)
| m_memory_v_CMD(X0,X1,c_write_h_resp_h_invalid)
| m_memory_v_CMD(X0,X1,c_write_h_resp_h_shared)
| ~ node31(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_80) ).
fof(f219,axiom,
! [X0,X1] :
( ~ m_memory_v_busy(X0,X1)
| node30(X0,X1)
| m_memory_v_reply_h_stall(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_81) ).
fof(f220,axiom,
! [X0,X1] :
( ~ m_memory_v_reply_h_stall(X0,X1)
| m_memory_v_reply_h_stall(X0,X1)
| node31(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_memory_82) ).
fof(f221,axiom,
! [X0,X1] :
( m_processor_v_cmd(X0,X1,c_idle)
| m_processor_v_cmd(X0,X1,c_read_h_shared)
| m_processor_v_cmd(X0,X1,c_read_h_owned)
| m_processor_v_cmd(X0,X1,c_write_h_invalid)
| m_processor_v_cmd(X0,X1,c_write_h_shared)
| m_processor_v_cmd(X0,X1,c_write_h_resp_h_invalid)
| m_processor_v_cmd(X0,X1,c_write_h_resp_h_shared)
| m_processor_v_cmd(X0,X1,c_invalidate)
| m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_1) ).
fof(f222,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_idle)
| ~ m_processor_v_cmd(X0,X1,c_read_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_2) ).
fof(f223,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_idle)
| ~ m_processor_v_cmd(X0,X1,c_read_h_owned) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_3) ).
fof(f224,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_idle)
| ~ m_processor_v_cmd(X0,X1,c_write_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_4) ).
fof(f225,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_idle)
| ~ m_processor_v_cmd(X0,X1,c_write_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_5) ).
fof(f226,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_idle)
| ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_6) ).
fof(f227,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_idle)
| ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_7) ).
fof(f228,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_idle)
| ~ m_processor_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_8) ).
fof(f229,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_idle)
| ~ m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_9) ).
fof(f230,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_read_h_owned) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_10) ).
fof(f231,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_write_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_11) ).
fof(f232,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_write_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_12) ).
fof(f233,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_13) ).
fof(f234,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_14) ).
fof(f235,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_15) ).
fof(f236,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_16) ).
fof(f237,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_owned)
| ~ m_processor_v_cmd(X0,X1,c_write_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_17) ).
fof(f238,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_owned)
| ~ m_processor_v_cmd(X0,X1,c_write_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_18) ).
fof(f239,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_owned)
| ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_19) ).
fof(f240,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_owned)
| ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_20) ).
fof(f241,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_owned)
| ~ m_processor_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_21) ).
fof(f242,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_owned)
| ~ m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_22) ).
fof(f243,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_invalid)
| ~ m_processor_v_cmd(X0,X1,c_write_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_23) ).
fof(f244,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_invalid)
| ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_24) ).
fof(f245,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_invalid)
| ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_25) ).
fof(f246,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_invalid)
| ~ m_processor_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_26) ).
fof(f247,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_invalid)
| ~ m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_27) ).
fof(f248,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_28) ).
fof(f249,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_29) ).
fof(f250,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_30) ).
fof(f251,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_31) ).
fof(f252,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_invalid)
| ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_32) ).
fof(f253,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_invalid)
| ~ m_processor_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_33) ).
fof(f254,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_invalid)
| ~ m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_34) ).
fof(f255,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_35) ).
fof(f256,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_resp_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_36) ).
fof(f257,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_invalidate)
| ~ m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_37) ).
fof(f258,axiom,
! [X0,X1] :
( m_processor_v_snoop(X0,X1,c_invalid)
| m_processor_v_snoop(X0,X1,c_owned)
| m_processor_v_snoop(X0,X1,c_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_38) ).
fof(f259,axiom,
! [X0,X1] :
( ~ m_processor_v_snoop(X0,X1,c_invalid)
| ~ m_processor_v_snoop(X0,X1,c_owned) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_39) ).
fof(f260,axiom,
! [X0,X1] :
( ~ m_processor_v_snoop(X0,X1,c_invalid)
| ~ m_processor_v_snoop(X0,X1,c_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_40) ).
fof(f261,axiom,
! [X0,X1] :
( ~ m_processor_v_snoop(X0,X1,c_owned)
| ~ m_processor_v_snoop(X0,X1,c_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_41) ).
fof(f262,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_invalid)
| m_processor_v_state(X0,X1,c_shared)
| m_processor_v_state(X0,X1,c_owned) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_42) ).
fof(f263,axiom,
! [X0,X1] :
( ~ m_processor_v_state(X0,X1,c_invalid)
| ~ m_processor_v_state(X0,X1,c_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_43) ).
fof(f264,axiom,
! [X0,X1] :
( ~ m_processor_v_state(X0,X1,c_invalid)
| ~ m_processor_v_state(X0,X1,c_owned) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_44) ).
fof(f265,axiom,
! [X0,X1] :
( ~ m_processor_v_state(X0,X1,c_shared)
| ~ m_processor_v_state(X0,X1,c_owned) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_45) ).
fof(f266,axiom,
! [X0] : m_processor_v_state(X0,s0,c_invalid),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_46) ).
fof(f267,axiom,
! [X0] : m_processor_v_snoop(X0,s0,c_invalid),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_47) ).
fof(f268,axiom,
! [X0] : ~ m_processor_v_waiting(X0,s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_48) ).
fof(f269,axiom,
! [X2,X3,X0,X1] :
( m_processor_v_state(X0,X1,X2)
| ~ m_processor_v_state(X0,X3,X2)
| ~ node32(X0,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_49) ).
fof(f270,axiom,
! [X2,X3,X0,X1] :
( ~ m_processor_v_state(X0,X1,X2)
| m_processor_v_state(X0,X3,X2)
| ~ node32(X0,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_50) ).
fof(f271,axiom,
! [X2,X3,X0,X1] :
( m_processor_v_state(X0,X1,X2)
| ~ m_processor_v_state(X0,X3,X2)
| ~ node33(X0,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_51) ).
fof(f272,axiom,
! [X2,X3,X0,X1] :
( ~ m_processor_v_state(X0,X1,X2)
| m_processor_v_state(X0,X3,X2)
| ~ node33(X0,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_52) ).
fof(f273,axiom,
! [X2,X0,X1] :
( ~ m_processor_v_CMD(X0,X1,c_read_h_shared)
| m_processor_v_state(X0,X2,c_shared)
| ~ node34(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_53) ).
fof(f274,axiom,
! [X2,X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_shared)
| ~ m_processor_v_CMD(X0,X1,c_read_h_owned)
| m_processor_v_state(X0,X2,c_owned)
| ~ node34(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_54) ).
fof(f275,axiom,
! [X2,X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_shared)
| m_processor_v_CMD(X0,X1,c_read_h_owned)
| ~ m_processor_v_CMD(X0,X1,c_write_h_invalid)
| m_processor_v_state(X0,X2,c_invalid)
| ~ node34(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_55) ).
fof(f276,axiom,
! [X2,X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_shared)
| m_processor_v_CMD(X0,X1,c_read_h_owned)
| m_processor_v_CMD(X0,X1,c_write_h_invalid)
| ~ m_processor_v_CMD(X0,X1,c_write_h_resp_h_invalid)
| m_processor_v_state(X0,X2,c_invalid)
| ~ node34(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_56) ).
fof(f277,axiom,
! [X2,X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_shared)
| m_processor_v_CMD(X0,X1,c_read_h_owned)
| m_processor_v_CMD(X0,X1,c_write_h_invalid)
| m_processor_v_CMD(X0,X1,c_write_h_resp_h_invalid)
| ~ m_processor_v_CMD(X0,X1,c_write_h_shared)
| m_processor_v_state(X0,X2,c_shared)
| ~ node34(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_57) ).
fof(f278,axiom,
! [X2,X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_shared)
| m_processor_v_CMD(X0,X1,c_read_h_owned)
| m_processor_v_CMD(X0,X1,c_write_h_invalid)
| m_processor_v_CMD(X0,X1,c_write_h_resp_h_invalid)
| m_processor_v_CMD(X0,X1,c_write_h_shared)
| ~ m_processor_v_CMD(X0,X1,c_write_h_resp_h_shared)
| m_processor_v_state(X0,X2,c_shared)
| ~ node34(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_58) ).
fof(f279,axiom,
! [X2,X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_shared)
| m_processor_v_CMD(X0,X1,c_read_h_owned)
| m_processor_v_CMD(X0,X1,c_write_h_invalid)
| m_processor_v_CMD(X0,X1,c_write_h_resp_h_invalid)
| m_processor_v_CMD(X0,X1,c_write_h_shared)
| m_processor_v_CMD(X0,X1,c_write_h_resp_h_shared)
| node33(X0,X1,X2)
| ~ node34(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_59) ).
fof(f280,axiom,
! [X0,X1] :
( ~ m_processor_v_CMD(X0,X1,c_read_h_owned)
| ~ node35(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_60) ).
fof(f281,axiom,
! [X0,X1] :
( ~ m_processor_v_CMD(X0,X1,c_invalidate)
| ~ node35(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_61) ).
fof(f282,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node36(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_62) ).
fof(f283,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_shared)
| ~ node36(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_63) ).
fof(f284,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_owned)
| m_processor_v_CMD(X0,X1,c_invalidate)
| ~ node36(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_64) ).
fof(f285,axiom,
! [X2,X3,X0,X1] :
( m_processor_v_state(X0,X1,X2)
| ~ m_processor_v_state(X0,X3,X2)
| ~ node37(X0,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_65) ).
fof(f286,axiom,
! [X2,X3,X0,X1] :
( ~ m_processor_v_state(X0,X1,X2)
| m_processor_v_state(X0,X3,X2)
| ~ node37(X0,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_66) ).
fof(f287,axiom,
! [X2,X0,X1] :
( ~ m_processor_v_abort(X0,X1)
| node32(X0,X1,X2)
| ~ node38(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_67) ).
fof(f288,axiom,
! [X2,X0,X1] :
( m_processor_v_abort(X0,X1)
| ~ m_processor_v_master(X0,X1)
| node34(X0,X1,X2)
| ~ node38(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_68) ).
fof(f289,axiom,
! [X2,X0,X1] :
( m_processor_v_abort(X0,X1)
| m_processor_v_master(X0,X1)
| m_processor_v_master(X0,X1)
| ~ m_processor_v_state(X0,X1,c_shared)
| node35(X0,X1)
| m_processor_v_state(X0,X2,c_invalid)
| ~ node38(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_69) ).
fof(f290,axiom,
! [X2,X0,X1] :
( m_processor_v_state(X0,X1,c_shared)
| m_processor_v_state(X0,X1,c_invalid)
| m_processor_v_abort(X0,X2)
| m_processor_v_master(X0,X2)
| node36(X0,X2)
| ~ m_processor_v_state(X0,X2,c_shared)
| ~ node38(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_70) ).
fof(f291,axiom,
! [X2,X0,X1] :
( m_processor_v_abort(X0,X1)
| m_processor_v_master(X0,X1)
| node36(X0,X1)
| m_processor_v_state(X0,X1,c_shared)
| node37(X0,X1,X2)
| ~ node38(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_71) ).
fof(f292,axiom,
! [X2,X0,X1] :
( ~ trans(X0,X1)
| node38(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_72) ).
fof(f293,axiom,
! [X2,X3,X0,X1] :
( m_processor_v_snoop(X0,X1,X2)
| ~ m_processor_v_snoop(X0,X3,X2)
| ~ node39(X0,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_73) ).
fof(f294,axiom,
! [X2,X3,X0,X1] :
( ~ m_processor_v_snoop(X0,X1,X2)
| m_processor_v_snoop(X0,X3,X2)
| ~ node39(X0,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_74) ).
fof(f295,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node40(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_75) ).
fof(f296,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_owned)
| ~ node40(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_76) ).
fof(f297,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_shared)
| ~ node40(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_77) ).
fof(f298,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node41(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_78) ).
fof(f299,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_owned)
| ~ node41(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_79) ).
fof(f300,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_shared)
| ~ node41(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_80) ).
fof(f301,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node42(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_81) ).
fof(f302,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_write_h_resp_h_invalid)
| ~ node42(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_82) ).
fof(f303,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node43(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_83) ).
fof(f304,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_write_h_resp_h_shared)
| ~ node43(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_84) ).
fof(f305,axiom,
! [X2,X3,X0,X1] :
( m_processor_v_snoop(X0,X1,X2)
| ~ m_processor_v_snoop(X0,X3,X2)
| ~ node44(X0,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_85) ).
fof(f306,axiom,
! [X2,X3,X0,X1] :
( ~ m_processor_v_snoop(X0,X1,X2)
| m_processor_v_snoop(X0,X3,X2)
| ~ node44(X0,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_86) ).
fof(f307,axiom,
! [X2,X0,X1] :
( ~ m_processor_v_abort(X0,X1)
| node39(X0,X1,X2)
| ~ node45(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_87) ).
fof(f308,axiom,
! [X2,X0,X1] :
( m_processor_v_abort(X0,X1)
| m_processor_v_master(X0,X1)
| ~ m_processor_v_state(X0,X1,c_owned)
| ~ m_processor_v_CMD(X0,X1,c_read_h_shared)
| m_processor_v_snoop(X0,X2,c_shared)
| ~ node45(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_88) ).
fof(f309,axiom,
! [X2,X0,X1] :
( m_processor_v_abort(X0,X1)
| node40(X0,X1)
| m_processor_v_master(X0,X1)
| ~ m_processor_v_state(X0,X1,c_owned)
| ~ m_processor_v_CMD(X0,X1,c_read_h_shared)
| m_processor_v_snoop(X0,X2,c_owned)
| ~ node45(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_89) ).
fof(f310,axiom,
! [X2,X0,X1] :
( m_processor_v_abort(X0,X1)
| node40(X0,X1)
| node41(X0,X1)
| ~ m_processor_v_master(X0,X1)
| ~ m_processor_v_CMD(X0,X1,c_write_h_resp_h_invalid)
| m_processor_v_snoop(X0,X2,c_invalid)
| ~ node45(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_90) ).
fof(f311,axiom,
! [X2,X0,X1] :
( m_processor_v_abort(X0,X1)
| node40(X0,X1)
| node41(X0,X1)
| node42(X0,X1)
| ~ m_processor_v_master(X0,X1)
| ~ m_processor_v_CMD(X0,X1,c_write_h_resp_h_shared)
| m_processor_v_snoop(X0,X2,c_invalid)
| ~ node45(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_91) ).
fof(f312,axiom,
! [X2,X0,X1] :
( m_processor_v_abort(X0,X1)
| node40(X0,X1)
| node41(X0,X1)
| node42(X0,X1)
| node43(X0,X1)
| node44(X0,X1,X2)
| ~ node45(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_92) ).
fof(f313,axiom,
! [X2,X0,X1] :
( ~ trans(X0,X1)
| node45(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_93) ).
fof(f314,axiom,
! [X2,X0,X1] :
( m_processor_v_waiting(X0,X1)
| ~ m_processor_v_waiting(X0,X2)
| ~ node46(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_94) ).
fof(f315,axiom,
! [X2,X0,X1] :
( ~ m_processor_v_waiting(X0,X1)
| m_processor_v_waiting(X0,X2)
| ~ node46(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_95) ).
fof(f316,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node47(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_96) ).
fof(f317,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_shared)
| ~ node47(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_97) ).
fof(f318,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node48(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_98) ).
fof(f319,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_owned)
| ~ node48(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_99) ).
fof(f320,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node49(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_100) ).
fof(f321,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_response)
| ~ node49(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_101) ).
fof(f322,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node50(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_102) ).
fof(f323,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_write_h_resp_h_invalid)
| ~ node50(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_103) ).
fof(f324,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node51(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_104) ).
fof(f325,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_write_h_resp_h_shared)
| ~ node51(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_105) ).
fof(f326,axiom,
! [X2,X0,X1] :
( m_processor_v_waiting(X0,X1)
| ~ m_processor_v_waiting(X0,X2)
| ~ node52(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_106) ).
fof(f327,axiom,
! [X2,X0,X1] :
( ~ m_processor_v_waiting(X0,X1)
| m_processor_v_waiting(X0,X2)
| ~ node52(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_107) ).
fof(f328,axiom,
! [X2,X0,X1] :
( ~ m_processor_v_abort(X0,X1)
| node46(X0,X1,X2)
| ~ node53(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_108) ).
fof(f329,axiom,
! [X2,X0,X1] :
( m_processor_v_abort(X0,X1)
| ~ m_processor_v_master(X0,X1)
| ~ m_processor_v_CMD(X0,X1,c_read_h_shared)
| m_processor_v_waiting(X0,X2)
| ~ node53(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_109) ).
fof(f330,axiom,
! [X2,X0,X1] :
( m_processor_v_abort(X0,X1)
| node47(X0,X1)
| ~ m_processor_v_master(X0,X1)
| ~ m_processor_v_CMD(X0,X1,c_read_h_owned)
| m_processor_v_waiting(X0,X2)
| ~ node53(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_110) ).
fof(f331,axiom,
! [X2,X0,X1] :
( m_processor_v_abort(X0,X1)
| node47(X0,X1)
| node48(X0,X1)
| m_processor_v_master(X0,X1)
| ~ m_processor_v_CMD(X0,X1,c_response)
| ~ m_processor_v_waiting(X0,X2)
| ~ node53(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_111) ).
fof(f332,axiom,
! [X2,X0,X1] :
( m_processor_v_abort(X0,X1)
| node47(X0,X1)
| node48(X0,X1)
| node49(X0,X1)
| m_processor_v_master(X0,X1)
| ~ m_processor_v_CMD(X0,X1,c_write_h_resp_h_invalid)
| ~ m_processor_v_waiting(X0,X2)
| ~ node53(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_112) ).
fof(f333,axiom,
! [X2,X0,X1] :
( m_processor_v_abort(X0,X1)
| node47(X0,X1)
| node48(X0,X1)
| node49(X0,X1)
| node50(X0,X1)
| m_processor_v_master(X0,X1)
| ~ m_processor_v_CMD(X0,X1,c_write_h_resp_h_shared)
| ~ m_processor_v_waiting(X0,X2)
| ~ node53(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_113) ).
fof(f334,axiom,
! [X2,X0,X1] :
( m_processor_v_abort(X0,X1)
| node47(X0,X1)
| node48(X0,X1)
| node49(X0,X1)
| node50(X0,X1)
| node51(X0,X1)
| node52(X0,X1,X2)
| ~ node53(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_114) ).
fof(f335,axiom,
! [X2,X0,X1] :
( ~ trans(X0,X1)
| node53(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_115) ).
fof(f336,axiom,
! [X0,X1] :
( ~ m_processor_v_state(X0,X1,c_shared)
| ~ node54(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_116) ).
fof(f337,axiom,
! [X0,X1] :
( ~ m_processor_v_state(X0,X1,c_owned)
| ~ node54(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_117) ).
fof(f338,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_shared)
| m_processor_v_state(X0,X1,c_owned)
| ~ node55(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_118) ).
fof(f339,axiom,
! [X0,X1] :
( ~ m_processor_v_waiting(X0,X1)
| ~ node55(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_119) ).
fof(f340,axiom,
! [X0,X1] :
( m_processor_v_readable(X0,X1)
| node54(X0,X1)
| m_processor_v_waiting(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_120) ).
fof(f341,axiom,
! [X0,X1] :
( ~ m_processor_v_readable(X0,X1)
| node55(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_121) ).
fof(f342,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_owned)
| ~ node56(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_122) ).
fof(f343,axiom,
! [X0,X1] :
( ~ m_processor_v_waiting(X0,X1)
| ~ node56(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_123) ).
fof(f344,axiom,
! [X0,X1] :
( m_processor_v_writable(X0,X1)
| ~ m_processor_v_state(X0,X1,c_owned)
| m_processor_v_waiting(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_124) ).
fof(f345,axiom,
! [X0,X1] :
( ~ m_processor_v_writable(X0,X1)
| node56(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_125) ).
fof(f346,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node57(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_126) ).
fof(f347,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_owned)
| ~ node57(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_127) ).
fof(f348,axiom,
! [X0,X1] :
( m_processor_v_reply_h_owned(X0,X1)
| m_processor_v_master(X0,X1)
| ~ m_processor_v_state(X0,X1,c_owned) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_128) ).
fof(f349,axiom,
! [X0,X1] :
( ~ m_processor_v_reply_h_owned(X0,X1)
| node57(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_129) ).
fof(f350,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node58(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_130) ).
fof(f351,axiom,
! [X0,X1] :
( m_processor_v_waiting(X0,X1)
| ~ node58(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_131) ).
fof(f352,axiom,
! [X0,X1] :
( m_processor_v_reply_h_waiting(X0,X1)
| m_processor_v_master(X0,X1)
| ~ m_processor_v_waiting(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_132) ).
fof(f353,axiom,
! [X0,X1] :
( ~ m_processor_v_reply_h_waiting(X0,X1)
| node58(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_133) ).
fof(f354,axiom,
! [X0,X1] :
( ~ m_processor_v_CMD(X0,X1,c_read_h_shared)
| ~ node59(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_134) ).
fof(f355,axiom,
! [X0,X1] :
( ~ m_processor_v_CMD(X0,X1,c_read_h_owned)
| ~ node59(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_135) ).
fof(f356,axiom,
! [X0,X1] :
( ~ m_processor_v_REPLY_h_STALL(X0,X1)
| ~ node60(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_136) ).
fof(f357,axiom,
! [X0,X1] :
( node59(X0,X1)
| ~ m_processor_v_REPLY_h_WAITING(X0,X1)
| ~ node60(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_137) ).
fof(f358,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_shared)
| m_processor_v_CMD(X0,X1,c_read_h_owned)
| ~ node61(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_138) ).
fof(f359,axiom,
! [X0,X1] :
( m_processor_v_REPLY_h_WAITING(X0,X1)
| ~ node61(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_139) ).
fof(f360,axiom,
! [X0,X1] :
( m_processor_v_abort(X0,X1)
| node60(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_140) ).
fof(f361,axiom,
! [X0,X1] :
( ~ m_processor_v_abort(X0,X1)
| m_processor_v_REPLY_h_STALL(X0,X1)
| node61(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_141) ).
fof(f362,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node62(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_142) ).
fof(f363,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_invalid)
| ~ node62(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_143) ).
fof(f364,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node63(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_144) ).
fof(f365,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_shared)
| ~ node63(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_145) ).
fof(f366,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node64(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_146) ).
fof(f367,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_owned)
| ~ node64(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_147) ).
fof(f368,axiom,
! [X0,X1] :
( m_processor_v_snoop(X0,X1,c_owned)
| ~ node64(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_148) ).
fof(f369,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node65(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_149) ).
fof(f370,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_owned)
| ~ node65(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_150) ).
fof(f371,axiom,
! [X0,X1] :
( m_processor_v_snoop(X0,X1,c_shared)
| ~ node65(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_151) ).
fof(f372,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node66(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_152) ).
fof(f373,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_owned)
| ~ node66(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_153) ).
fof(f374,axiom,
! [X0,X1] :
( m_processor_v_snoop(X0,X1,c_invalid)
| ~ node66(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_154) ).
fof(f375,axiom,
! [X0,X1] :
( m_processor_v_cmd(X0,X1,c_read_h_shared)
| m_processor_v_cmd(X0,X1,c_read_h_owned)
| ~ m_processor_v_master(X0,X1)
| ~ m_processor_v_state(X0,X1,c_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_155) ).
fof(f376,axiom,
! [X0,X1] :
( node62(X0,X1)
| ~ m_processor_v_master(X0,X1)
| ~ m_processor_v_state(X0,X1,c_shared)
| m_processor_v_cmd(X0,X1,c_read_h_owned) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_156) ).
fof(f377,axiom,
! [X0,X1] :
( node62(X0,X1)
| node63(X0,X1)
| ~ m_processor_v_master(X0,X1)
| ~ m_processor_v_state(X0,X1,c_owned)
| ~ m_processor_v_snoop(X0,X1,c_owned)
| m_processor_v_cmd(X0,X1,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_157) ).
fof(f378,axiom,
! [X0,X1] :
( node62(X0,X1)
| node63(X0,X1)
| node64(X0,X1)
| ~ m_processor_v_master(X0,X1)
| ~ m_processor_v_state(X0,X1,c_owned)
| ~ m_processor_v_snoop(X0,X1,c_shared)
| m_processor_v_cmd(X0,X1,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_158) ).
fof(f379,axiom,
! [X0,X1] :
( node62(X0,X1)
| node63(X0,X1)
| node64(X0,X1)
| node65(X0,X1)
| ~ m_processor_v_master(X0,X1)
| ~ m_processor_v_state(X0,X1,c_owned)
| ~ m_processor_v_snoop(X0,X1,c_invalid)
| m_processor_v_cmd(X0,X1,c_write_h_invalid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_159) ).
fof(f380,axiom,
! [X0,X1] :
( node62(X0,X1)
| node63(X0,X1)
| node64(X0,X1)
| node65(X0,X1)
| node66(X0,X1)
| m_processor_v_cmd(X0,X1,c_idle) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_processor_160) ).
fof(f381,negated_conjecture,
! [X0] :
( m_processor_v_writable(c_p0,X0)
| ~ node67(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty1) ).
fof(f382,negated_conjecture,
! [X0] :
( m_processor_v_writable(c_p1,X0)
| ~ node67(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty2) ).
fof(f383,negated_conjecture,
! [X0] :
( node67(X0)
| xuntil69(X0)
| ~ until68(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty3) ).
fof(f384,negated_conjecture,
! [X0,X1] :
( until68(X0)
| ~ succ(X1,X0)
| ~ xuntil69(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty4) ).
fof(f385,negated_conjecture,
! [X0] :
( loop
| ~ last(X0)
| ~ xuntil69(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty5) ).
fof(f386,negated_conjecture,
! [X0,X1] :
( until2p70(X0)
| ~ trans(X1,X0)
| ~ last(X1)
| ~ xuntil69(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty6) ).
fof(f387,negated_conjecture,
! [X0] :
( node67(X0)
| xuntil2p71(X0)
| ~ until2p70(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty7) ).
fof(f388,negated_conjecture,
! [X0,X1] :
( until2p70(X0)
| ~ succ(X1,X0)
| ~ xuntil2p71(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty8) ).
fof(f389,negated_conjecture,
! [X0] :
( ~ last(X0)
| ~ xuntil2p71(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty9) ).
fof(f390,negated_conjecture,
until68(s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty10) ).
fof(f1244,plain,
$false,
inference(finite_model_not_found_(exhaustively_excluded_all_possible_domain_size_assignments),[],[f1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16,f17,f18,f19,f20,f21,f22,f23,f24,f25,f26,f27,f28,f29,f30,f31,f32,f33,f34,f35,f36,f37,f38,f39,f40,f41,f42,f43,f44,f45,f46,f47,f48,f49,f50,f51,f52,f53,f54,f55,f56,f57,f58,f59,f60,f61,f62,f63,f64,f65,f66,f67,f68,f69,f70,f71,f72,f73,f74,f75,f76,f77,f78,f79,f80,f81,f82,f83,f84,f85,f86,f87,f88,f89,f90,f91,f92,f93,f94,f95,f96,f97,f98,f99,f100,f101,f102,f103,f104,f105,f106,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,f194,f195,f196,f197,f198,f199,f200,f201,f202,f203,f204,f205,f206,f207,f208,f209,f210,f211,f212,f213,f214,f215,f216,f217,f218,f219,f220,f221,f222,f223,f224,f225,f226,f227,f228,f229,f230,f231,f232,f233,f234,f235,f236,f237,f238,f239,f240,f241,f242,f243,f244,f245,f246,f247,f248,f249,f250,f251,f252,f253,f254,f255,f256,f257,f258,f259,f260,f261,f262,f263,f264,f265,f266,f267,f268,f269,f270,f271,f272,f273,f274,f275,f276,f277,f278,f279,f280,f281,f282,f283,f284,f285,f286,f287,f288,f289,f290,f291,f292,f293,f294,f295,f296,f297,f298,f299,f300,f301,f302,f303,f304,f305,f306,f307,f308,f309,f310,f311,f312,f313,f314,f315,f316,f317,f318,f319,f320,f321,f322,f323,f324,f325,f326,f327,f328,f329,f330,f331,f332,f333,f334,f335,f336,f337,f338,f339,f340,f341,f342,f343,f344,f345,f346,f347,f348,f349,f350,f351,f352,f353,f354,f355,f356,f357,f358,f359,f360,f361,f362,f363,f364,f365,f366,f367,f368,f369,f370,f371,f372,f373,f374,f375,f376,f377,f378,f379,f380,f381,f382,f383,f384,f385,f386,f387,f388,f389,f390]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV420-1.010 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n003.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 10:58:27 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.22 Running first-order model finding
% 0.07/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.82/2.79 % (1512058)Will run a generic schedule for satisfiability detection.
% 16.82/2.79 % (1512067)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1253007529:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.82/2.79 % (1512064)% WARNING: option uhcvi not known.
% 16.82/2.79 % (1512063)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2725047265_2999 on theBenchmark for (2999ds/0Mi)
% 16.82/2.79 % (1512065)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4114452838:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.82/2.79 % (1512064)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2439793775:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.82/2.79 % (1512066)dis+10_1_sil=32000:sp=arity:random_seed=2511606627:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.82/2.79 % (1512068)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1091534656:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.82/2.79 % (1512069)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=540333668:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.82/2.79 % Detected minimum model sizes of [1]
% 16.82/2.79 % Detected maximum model sizes of [26]
% 16.82/2.79 % TRYING [1]
% 16.82/2.79 % TRYING [2]
% 16.82/2.79 % (1512067)Instruction limit reached!
% 16.82/2.79 % (1512067)------------------------------
% 16.82/2.79 % (1512067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.82/2.79 % (1512067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.82/2.79 % (1512067)CaDiCaL version: 2.1.3
% 16.82/2.79 % (1512067)Termination reason: Instruction limit
% 16.82/2.79 % (1512067)Termination phase: Saturation
% 16.82/2.79 % (1512067)Time elapsed: 0.029 s
% 16.82/2.79 % (1512067)Peak memory usage: 12 MB
% 16.82/2.79 % (1512067)Instructions burned: 117 (million)
% 16.82/2.79 % TRYING [3]
% 16.82/2.79 % (1512084)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3352889604:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.82/2.79 % Detected minimum model sizes of [1]
% 16.82/2.79 % Detected maximum model sizes of [26]
% 16.82/2.79 % TRYING [1]
% 16.82/2.79 % TRYING [2]
% 16.82/2.79 % TRYING [3]
% 16.82/2.79 % (1512066)Instruction limit reached!
% 16.82/2.79 % (1512066)------------------------------
% 16.82/2.79 % (1512066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.82/2.79 % (1512066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.82/2.79 % (1512066)CaDiCaL version: 2.1.3
% 16.82/2.79 % (1512066)Termination reason: Instruction limit
% 16.82/2.79 % (1512066)Termination phase: Saturation
% 16.82/2.79 % (1512066)Time elapsed: 0.078 s
% 16.82/2.79 % (1512066)Peak memory usage: 12 MB
% 16.82/2.79 % (1512066)Instructions burned: 104 (million)
% 16.82/2.79 % TRYING [4]
% 16.82/2.79 % TRYING [4]
% 16.82/2.79 % (1512068)Instruction limit reached!
% 16.82/2.79 % (1512068)------------------------------
% 16.82/2.79 % (1512068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.82/2.79 % (1512068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.82/2.79 % (1512068)CaDiCaL version: 2.1.3
% 16.82/2.79 % (1512068)Termination reason: Instruction limit
% 16.82/2.79 % (1512068)Termination phase: Saturation
% 16.82/2.79 % (1512068)Time elapsed: 0.098 s
% 16.82/2.79 % (1512068)Peak memory usage: 13 MB
% 16.82/2.79 % (1512068)Instructions burned: 132 (million)
% 16.82/2.79 % (1512087)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3104863122:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.82/2.79 % (1512069)Instruction limit reached!
% 16.82/2.79 % (1512069)------------------------------
% 16.82/2.79 % (1512069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.82/2.79 % (1512069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.82/2.79 % (1512069)CaDiCaL version: 2.1.3
% 16.82/2.79 % (1512069)Termination reason: Instruction limit
% 16.82/2.79 % (1512069)Termination phase: Saturation
% 16.82/2.79 % (1512069)Time elapsed: 0.104 s
% 16.82/2.79 % (1512069)Peak memory usage: 14 MB
% 16.82/2.79 % (1512069)Instructions burned: 160 (million)
% 16.82/2.79 % (1512088)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=1461479001:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.82/2.79 % (1512090)ott-21_1_sil=16000:fs=off:random_seed=3616063138:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.82/2.79 % (1512087)Instruction limit reached!
% 43.73/6.49 % (1512087)------------------------------
% 43.73/6.49 % (1512087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.73/6.49 % (1512087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.73/6.49 % (1512087)CaDiCaL version: 2.1.3
% 43.73/6.49 % (1512087)Termination reason: Instruction limit
% 43.73/6.49 % (1512087)Termination phase: Saturation
% 43.73/6.49 % (1512087)Time elapsed: 0.100 s
% 43.73/6.49 % (1512087)Peak memory usage: 14 MB
% 43.73/6.49 % (1512087)Instructions burned: 132 (million)
% 43.73/6.49 % TRYING [5]
% 43.73/6.49 % (1512090)Instruction limit reached!
% 43.73/6.49 % (1512090)------------------------------
% 43.73/6.49 % (1512090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.73/6.49 % (1512090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.73/6.49 % (1512090)CaDiCaL version: 2.1.3
% 43.73/6.49 % (1512090)Termination reason: Instruction limit
% 43.73/6.49 % (1512090)Termination phase: Saturation
% 43.73/6.49 % (1512090)Time elapsed: 0.104 s
% 43.73/6.49 % (1512090)Peak memory usage: 14 MB
% 43.73/6.49 % (1512090)Instructions burned: 181 (million)
% 43.73/6.49 % (1512095)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=914156351:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 43.73/6.49 % (1512097)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=937258265:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 43.73/6.49 % Detected minimum model sizes of [1]
% 43.73/6.49 % Detected maximum model sizes of [26]
% 43.73/6.49 % TRYING [1]
% 43.73/6.49 % TRYING [2]
% 43.73/6.49 % TRYING [3]
% 43.73/6.49 % TRYING [5]
% 43.73/6.49 % TRYING [4]
% 43.73/6.49 % (1512084)Instruction limit reached!
% 43.73/6.49 % (1512084)------------------------------
% 43.73/6.49 % (1512084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.73/6.49 % (1512084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.73/6.49 % (1512084)CaDiCaL version: 2.1.3
% 43.73/6.49 % (1512084)Termination reason: Instruction limit
% 43.73/6.49 % (1512084)Termination phase: Finite model building SAT solving
% 43.73/6.49 % (1512084)Time elapsed: 0.398 s
% 43.73/6.49 % (1512084)Peak memory usage: 18 MB
% 43.73/6.49 % (1512084)Instructions burned: 715 (million)
% 43.73/6.49 % (1512107)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2154974101:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 43.73/6.49 % TRYING [5]
% 43.73/6.49 % (1512095)Instruction limit reached!
% 43.73/6.49 % (1512095)------------------------------
% 43.73/6.49 % (1512095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.73/6.49 % (1512095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.73/6.49 % (1512095)CaDiCaL version: 2.1.3
% 43.73/6.49 % (1512095)Termination reason: Instruction limit
% 43.73/6.49 % (1512095)Termination phase: Saturation
% 43.73/6.49 % (1512095)Time elapsed: 0.274 s
% 43.73/6.49 % (1512095)Peak memory usage: 15 MB
% 43.73/6.49 % (1512095)Instructions burned: 477 (million)
% 43.73/6.49 % (1512109)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3289995604:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 43.73/6.49 % Detected minimum model sizes of [1]
% 43.73/6.49 % Detected maximum model sizes of [26]
% 43.73/6.49 % TRYING [14]
% 43.73/6.49 % (1512088)Instruction limit reached!
% 43.73/6.49 % (1512088)------------------------------
% 43.73/6.49 % (1512088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.73/6.49 % (1512088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.73/6.49 % (1512088)CaDiCaL version: 2.1.3
% 43.73/6.49 % (1512088)Termination reason: Instruction limit
% 43.73/6.49 % (1512088)Termination phase: Saturation
% 43.73/6.49 % (1512088)Time elapsed: 0.510 s
% 43.73/6.49 % (1512088)Peak memory usage: 17 MB
% 43.73/6.49 % (1512088)Instructions burned: 685 (million)
% 43.73/6.49 % (1512112)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=129288715: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)
% 43.73/6.49 % (1512109)Instruction limit reached!
% 43.73/6.49 % (1512109)------------------------------
% 43.73/6.49 % (1512109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.73/6.49 % (1512109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.73/6.49 % (1512109)CaDiCaL version: 2.1.3
% 43.73/6.49 % (1512109)Termination reason: Instruction limit
% 43.73/6.49 % (1512109)Termination phase: Finite model building SAT solving
% 43.73/6.49 % (1512109)Time elapsed: 0.307 s
% 110.93/15.94 % (1512109)Peak memory usage: 34 MB
% 110.93/15.94 % (1512109)Instructions burned: 894 (million)
% 110.93/15.94 % (1512097)Instruction limit reached!
% 110.93/15.94 % (1512097)------------------------------
% 110.93/15.94 % (1512097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 110.93/15.94 % (1512097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.93/15.94 % (1512097)CaDiCaL version: 2.1.3
% 110.93/15.94 % (1512097)Termination reason: Instruction limit
% 110.93/15.94 % (1512097)Termination phase: Finite model building SAT solving
% 110.93/15.94 % (1512097)Time elapsed: 0.590 s
% 110.93/15.94 % (1512097)Peak memory usage: 16 MB
% 110.93/15.94 % (1512097)Instructions burned: 865 (million)
% 110.93/15.94 % (1512117)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1561616808:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 110.93/15.94 % (1512119)fmb+10_1_sil=64000:random_seed=883410743:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 110.93/15.94 % Detected minimum model sizes of [1]
% 110.93/15.94 % Detected maximum model sizes of [26]
% 110.93/15.94 % TRYING [1]
% 110.93/15.94 % TRYING [2]
% 110.93/15.94 % TRYING [3]
% 110.93/15.94 % TRYING [4]
% 110.93/15.94 % TRYING [5]
% 110.93/15.94 % (1512117)Instruction limit reached!
% 110.93/15.94 % (1512117)------------------------------
% 110.93/15.94 % (1512117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 110.93/15.94 % (1512117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.93/15.94 % (1512117)CaDiCaL version: 2.1.3
% 110.93/15.94 % (1512117)Termination reason: Instruction limit
% 110.93/15.94 % (1512117)Termination phase: Saturation
% 110.93/15.94 % (1512117)Time elapsed: 0.350 s
% 110.93/15.94 % (1512117)Peak memory usage: 16 MB
% 110.93/15.94 % (1512117)Instructions burned: 881 (million)
% 110.93/15.94 % (1512127)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=516672180:i=9515:nm=5_2987 on theBenchmark for (2987ds/9515Mi)
% 110.93/15.94 % Detected minimum model sizes of [1]
% 110.93/15.94 % Detected maximum model sizes of [26]
% 110.93/15.94 % TRYING [20]
% 110.93/15.94 % (1512112)Instruction limit reached!
% 110.93/15.94 % (1512112)------------------------------
% 110.93/15.94 % (1512112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 110.93/15.94 % (1512112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.93/15.94 % (1512112)CaDiCaL version: 2.1.3
% 110.93/15.94 % (1512112)Termination reason: Instruction limit
% 110.93/15.94 % (1512112)Termination phase: Saturation
% 110.93/15.94 % (1512112)Time elapsed: 0.653 s
% 110.93/15.94 % (1512112)Peak memory usage: 19 MB
% 110.93/15.94 % (1512112)Instructions burned: 692 (million)
% 110.93/15.94 % (1512132)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=603635427:fmbsr=1.7:i=920_2986 on theBenchmark for (2986ds/920Mi)
% 110.93/15.94 % Detected minimum model sizes of [1]
% 110.93/15.94 % Detected maximum model sizes of [26]
% 110.93/15.94 % TRYING [8]
% 110.93/15.94 % (1512107)Instruction limit reached!
% 110.93/15.94 % (1512107)------------------------------
% 110.93/15.94 % (1512107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 110.93/15.94 % (1512107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.93/15.94 % (1512107)CaDiCaL version: 2.1.3
% 110.93/15.94 % (1512107)Termination reason: Instruction limit
% 110.93/15.94 % (1512107)Termination phase: Saturation
% 110.93/15.94 % (1512107)Time elapsed: 1.047 s
% 110.93/15.94 % (1512107)Peak memory usage: 21 MB
% 110.93/15.94 % (1512107)Instructions burned: 1179 (million)
% 110.93/15.94 % (1512137)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=603949254:i=5131_2984 on theBenchmark for (2984ds/5131Mi)
% 110.93/15.94 % TRYING [6]
% 110.93/15.94 % (1512132)Instruction limit reached!
% 110.93/15.94 % (1512132)------------------------------
% 110.93/15.94 % (1512132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 110.93/15.94 % (1512132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.93/15.94 % (1512132)CaDiCaL version: 2.1.3
% 110.93/15.94 % (1512132)Termination reason: Instruction limit
% 110.93/15.94 % (1512132)Termination phase: Finite model building SAT solving
% 110.93/15.94 % (1512132)Time elapsed: 0.425 s
% 110.93/15.94 % (1512132)Peak memory usage: 31 MB
% 110.93/15.94 % (1512132)Instructions burned: 921 (million)
% 110.93/15.94 % (1512143)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3589533940:i=1472:ins=7:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/1472Mi)
% 110.93/15.94 % TRYING [6]
% 110.93/15.94 % (1512143)Instruction limit reached!
% 110.93/15.94 % (1512143)------------------------------
% 110.93/15.94 % (1512143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.41/19.34 % (1512143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.41/19.34 % (1512143)CaDiCaL version: 2.1.3
% 135.41/19.34 % (1512143)Termination reason: Instruction limit
% 135.41/19.34 % (1512143)Termination phase: Saturation
% 135.41/19.34 % (1512143)Time elapsed: 0.691 s
% 135.41/19.34 % (1512143)Peak memory usage: 18 MB
% 135.41/19.34 % (1512143)Instructions burned: 1472 (million)
% 135.41/19.34 % (1512151)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2760658960:i=6324_2974 on theBenchmark for (2974ds/6324Mi)
% 135.41/19.34 % Detected minimum model sizes of [1]
% 135.41/19.34 % Detected maximum model sizes of [26]
% 135.41/19.34 % fmb_start_size (= 77) larger than a detected sort maximum size!
% 135.41/19.34 % (1512151)Refutation not found, incomplete strategy
% 135.41/19.34 % (1512151)------------------------------
% 135.41/19.34 % (1512151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.41/19.34 % (1512151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.41/19.34 % (1512151)CaDiCaL version: 2.1.3
% 135.41/19.34 % (1512151)Termination reason: Refutation not found, incomplete strategy
% 135.41/19.34 % (1512151)Time elapsed: 0.017 s
% 135.41/19.34 % (1512151)Peak memory usage: 11 MB
% 135.41/19.34 % (1512151)Instructions burned: 39 (million)
% 135.41/19.34 % (1512151)------------------------------
% 135.41/19.34 % (1512151)------------------------------
% 135.41/19.34 % (1512154)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=76763257:fmbsr=2.30978:i=2174_2973 on theBenchmark for (2973ds/2174Mi)
% 135.41/19.34 % Detected minimum model sizes of [1]
% 135.41/19.34 % Detected maximum model sizes of [26]
% 135.41/19.34 % TRYING [16]
% 135.41/19.34 % (1512154)Instruction limit reached!
% 135.41/19.34 % (1512154)------------------------------
% 135.41/19.34 % (1512154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.41/19.34 % (1512154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.41/19.34 % (1512154)CaDiCaL version: 2.1.3
% 135.41/19.34 % (1512154)Termination reason: Instruction limit
% 135.41/19.34 % (1512154)Termination phase: Finite model building SAT solving
% 135.41/19.34 % (1512154)Time elapsed: 1.038 s
% 135.41/19.34 % (1512154)Peak memory usage: 60 MB
% 135.41/19.34 % (1512154)Instructions burned: 2176 (million)
% 135.41/19.34 % (1512166)ott-2_1_sil=16000:newcnf=on:random_seed=2100245064:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2963 on theBenchmark for (2963ds/869Mi)
% 135.41/19.34 % (1512166)Instruction limit reached!
% 135.41/19.34 % (1512166)------------------------------
% 135.41/19.34 % (1512166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.41/19.34 % (1512166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.41/19.34 % (1512166)CaDiCaL version: 2.1.3
% 135.41/19.34 % (1512166)Termination reason: Instruction limit
% 135.41/19.34 % (1512166)Termination phase: Saturation
% 135.41/19.34 % (1512166)Time elapsed: 0.465 s
% 135.41/19.34 % (1512166)Peak memory usage: 19 MB
% 135.41/19.34 % (1512166)Instructions burned: 870 (million)
% 135.41/19.34 % (1512171)ott+10_1_sil=32000:tgt=ground:random_seed=1672726326:i=5114:av=off_2958 on theBenchmark for (2958ds/5114Mi)
% 135.41/19.34 % TRYING [7]
% 135.41/19.34 % TRYING [7]
% 135.41/19.34 % (1512171)Instruction limit reached!
% 135.41/19.34 % (1512171)------------------------------
% 135.41/19.34 % (1512171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.41/19.34 % (1512171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.41/19.34 % (1512171)CaDiCaL version: 2.1.3
% 135.41/19.34 % (1512171)Termination reason: Instruction limit
% 135.41/19.34 % (1512171)Termination phase: Saturation
% 135.41/19.34 % (1512171)Time elapsed: 1.983 s
% 135.41/19.34 % (1512171)Peak memory usage: 30 MB
% 135.41/19.34 % (1512171)Instructions burned: 5114 (million)
% 135.41/19.34 % (1512185)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2809068003:i=54282_2938 on theBenchmark for (2938ds/54282Mi)
% 135.41/19.34 % Detected minimum model sizes of [1]
% 135.41/19.34 % Detected maximum model sizes of [26]
% 135.41/19.34 % TRYING [1]
% 135.41/19.34 % TRYING [2]
% 135.41/19.34 % TRYING [3]
% 135.41/19.34 % (1512137)Instruction limit reached!
% 135.41/19.34 % (1512137)------------------------------
% 135.41/19.34 % (1512137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.41/19.34 % (1512137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.41/19.34 % (1512137)CaDiCaL version: 2.1.3
% 135.41/19.34 % (1512137)Termination reason: Instruction limit
% 135.41/19.34 % (1512137)Termination phase: Saturation
% 135.41/19.34 % (1512137)Time elapsed: 4.661 s
% 135.41/19.34 % (1512137)Peak memory usage: 36 MB
% 135.41/19.34 % (1512137)Instructions burned: 5131 (million)
% 135.41/19.34 % (1512188)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=951589161:i=3512:aac=none_2937 on theBenchmark for (2937ds/3512Mi)
% 135.41/19.34 % TRYING [4]
% 135.41/19.34 % TRYING [5]
% 135.41/19.34 % (1512188)Instruction limit reached!
% 135.41/19.34 % (1512188)------------------------------
% 135.41/19.34 % (1512188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.41/19.34 % (1512188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.41/19.34 % (1512188)CaDiCaL version: 2.1.3
% 135.41/19.34 % (1512188)Termination reason: Instruction limit
% 135.41/19.34 % (1512188)Termination phase: Saturation
% 135.41/19.34 % (1512188)Time elapsed: 1.483 s
% 135.41/19.34 % (1512188)Peak memory usage: 28 MB
% 135.41/19.34 % (1512188)Instructions burned: 3515 (million)
% 135.41/19.34 % (1512194)dis+21_1_sil=32000:sas=cadical:random_seed=4241088855:i=3773:amm=off_2922 on theBenchmark for (2922ds/3773Mi)
% 135.41/19.34 % TRYING [6]
% 135.41/19.34 % TRYING [8]
% 135.41/19.34 % TRYING [21]
% 135.41/19.34 % (1512127)Instruction limit reached!
% 135.41/19.34 % (1512127)------------------------------
% 135.41/19.34 % (1512127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.41/19.34 % (1512127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.41/19.34 % (1512127)CaDiCaL version: 2.1.3
% 135.41/19.34 % (1512127)Termination reason: Instruction limit
% 135.41/19.34 % (1512127)Termination phase: Finite model building SAT solving
% 135.41/19.34 % (1512127)Time elapsed: 7.898 s
% 135.41/19.34 % (1512127)Peak memory usage: 107 MB
% 135.41/19.34 % (1512127)Instructions burned: 9515 (million)
% 135.41/19.34 % (1512206)ott+11_1_sil=16000:gs=on:random_seed=1315372244:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2907 on theBenchmark for (2907ds/2251Mi)
% 135.41/19.34 % (1512194)Instruction limit reached!
% 135.41/19.34 % (1512194)------------------------------
% 135.41/19.34 % (1512194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.41/19.34 % (1512194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.41/19.34 % (1512194)CaDiCaL version: 2.1.3
% 135.41/19.34 % (1512194)Termination reason: Instruction limit
% 135.41/19.34 % (1512194)Termination phase: Saturation
% 135.41/19.34 % (1512194)Time elapsed: 1.658 s
% 135.41/19.34 % (1512194)Peak memory usage: 26 MB
% 135.41/19.34 % (1512194)Instructions burned: 3775 (million)
% 135.41/19.34 % (1512210)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2974388185:fmbsr=1.6:i=67534_2905 on theBenchmark for (2905ds/67534Mi)
% 135.41/19.34 % Detected minimum model sizes of [1]
% 135.41/19.34 % Detected maximum model sizes of [26]
% 135.41/19.34 % TRYING [7]
% 135.41/19.34 % TRYING [8]
% 135.41/19.34 % TRYING [9]
% 135.41/19.34 % (1512206)Instruction limit reached!
% 135.41/19.34 % (1512206)------------------------------
% 135.41/19.34 % (1512206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.41/19.34 % (1512206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.41/19.34 % (1512206)CaDiCaL version: 2.1.3
% 135.41/19.34 % (1512206)Termination reason: Instruction limit
% 135.41/19.34 % (1512206)Termination phase: Saturation
% 135.41/19.34 % (1512206)Time elapsed: 2.076 s
% 135.41/19.34 % (1512206)Peak memory usage: 26 MB
% 135.41/19.34 % (1512206)Instructions burned: 2252 (million)
% 135.41/19.34 % (1512215)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2123904233:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2886 on theBenchmark for (2886ds/4591Mi)
% 135.41/19.34 % TRYING [9]
% 135.41/19.34 % TRYING [7]
% 135.41/19.34 % TRYING [10]
% 135.41/19.34 % TRYING [8]
% 135.41/19.34 % (1512210)Cannot enumerate next child to try in an incomplete setup
% 135.41/19.34 % (1512210)Refutation not found, incomplete strategy
% 135.41/19.34 % (1512210)------------------------------
% 135.41/19.34 % (1512210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.41/19.34 % (1512210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.41/19.34 % (1512210)CaDiCaL version: 2.1.3
% 135.41/19.34 % (1512210)Termination reason: Refutation not found, incomplete strategy
% 135.41/19.34 % (1512210)Time elapsed: 5.921 s
% 135.41/19.34 % (1512210)Peak memory usage: 31 MB
% 135.41/19.34 % (1512210)Instructions burned: 12610 (million)
% 135.41/19.34 % (1512210)------------------------------
% 135.41/19.34 % (1512210)------------------------------
% 135.41/19.34 % (1512225)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2843693712:i=29340_2846 on theBenchmark for (2846ds/29340Mi)
% 135.41/19.34 % (1512215)Instruction limit reached!
% 135.41/19.34 % (1512215)------------------------------
% 135.41/19.34 % (1512215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.41/19.34 % (1512215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.41/19.34 % (1512215)CaDiCaL version: 2.1.3
% 135.41/19.34 % (1512215)Termination reason: Instruction limit
% 135.41/19.34 % (1512215)Termination phase: Saturation
% 135.41/19.34 % (1512215)Time elapsed: 4.367 s
% 135.41/19.34 % (1512215)Peak memory usage: 28 MB
% 135.41/19.34 % (1512215)Instructions burned: 4592 (million)
% 135.41/19.34 % (1512229)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=45770309:i=5211_2842 on theBenchmark for (2842ds/5211Mi)
% 135.41/19.34 % TRYING [10]
% 135.41/19.34 % (1512119) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1512058-1512119"...
% 135.41/19.34 % (1512119)...printing done.
% 135.41/19.34 % (1512119)Refutation found. Thanks to Tanya!
% 135.41/19.34 % SZS status Unsatisfiable for theBenchmark
% 135.41/19.34 % SZS output start Proof for theBenchmark
% See solution above
% 135.41/19.35 % (1512119)------------------------------
% 135.41/19.35 % (1512119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.41/19.35 % (1512119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.41/19.35 % (1512119)CaDiCaL version: 2.1.3
% 135.41/19.35 % (1512119)Termination reason: Refutation
% 135.41/19.35 % (1512119)Time elapsed: 18.146 s
% 135.41/19.35 % (1512119)Peak memory usage: 30 MB
% 135.41/19.35 % (1512119)Instructions burned: 21918 (million)
% 135.41/19.35 % (1512058)Success in time 19.116 s
% 135.41/19.35 % Vampire exiting
%------------------------------------------------------------------------------