%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV420-1.005 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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 13.43s 2.17s
% Output : Refutation 13.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 1
% Number of leaves : 383
% Syntax : Number of formulae : 384 ( 15 unt; 0 def)
% Number of atoms : 1020 ( 0 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 1248 ( 612 ~; 636 |; 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 : 21 ( 21 usr; 21 con; 0-0 aty)
% Number of variables : 693 ( 693 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
succ(s0,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bound1) ).
fof(f2,axiom,
succ(s1,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bound2) ).
fof(f3,axiom,
succ(s2,s3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bound3) ).
fof(f4,axiom,
succ(s3,s4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bound4) ).
fof(f5,axiom,
last(s4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bound5) ).
fof(f6,axiom,
! [X0,X1] :
( ~ succ(X0,X1)
| trans(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bound6) ).
fof(f7,axiom,
( ~ loop
| trans(s4,s0)
| trans(s4,s1)
| trans(s4,s2)
| trans(s4,s3)
| trans(s4,s4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bound7) ).
fof(f8,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/sandbox2/benchmark/theBenchmark.p',m_main_1) ).
fof(f9,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_read_h_shared) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_2) ).
fof(f10,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_read_h_owned) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_3) ).
fof(f11,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_write_h_invalid) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_4) ).
fof(f12,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_write_h_shared) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_5) ).
fof(f13,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_write_h_resp_h_invalid) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_6) ).
fof(f14,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_write_h_resp_h_shared) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_7) ).
fof(f15,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_8) ).
fof(f16,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_idle)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_9) ).
fof(f17,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_shared)
| ~ m_main_v_CMD(X0,c_read_h_owned) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_10) ).
fof(f18,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_shared)
| ~ m_main_v_CMD(X0,c_write_h_invalid) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_11) ).
fof(f19,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_shared)
| ~ m_main_v_CMD(X0,c_write_h_shared) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_12) ).
fof(f20,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/sandbox2/benchmark/theBenchmark.p',m_main_13) ).
fof(f21,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/sandbox2/benchmark/theBenchmark.p',m_main_14) ).
fof(f22,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_shared)
| ~ m_main_v_CMD(X0,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_15) ).
fof(f23,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_shared)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_16) ).
fof(f24,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_owned)
| ~ m_main_v_CMD(X0,c_write_h_invalid) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_17) ).
fof(f25,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_owned)
| ~ m_main_v_CMD(X0,c_write_h_shared) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_18) ).
fof(f26,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/sandbox2/benchmark/theBenchmark.p',m_main_19) ).
fof(f27,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/sandbox2/benchmark/theBenchmark.p',m_main_20) ).
fof(f28,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_owned)
| ~ m_main_v_CMD(X0,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_21) ).
fof(f29,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_read_h_owned)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_22) ).
fof(f30,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_invalid)
| ~ m_main_v_CMD(X0,c_write_h_shared) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_23) ).
fof(f31,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/sandbox2/benchmark/theBenchmark.p',m_main_24) ).
fof(f32,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/sandbox2/benchmark/theBenchmark.p',m_main_25) ).
fof(f33,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_invalid)
| ~ m_main_v_CMD(X0,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_26) ).
fof(f34,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_invalid)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_27) ).
fof(f35,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/sandbox2/benchmark/theBenchmark.p',m_main_28) ).
fof(f36,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/sandbox2/benchmark/theBenchmark.p',m_main_29) ).
fof(f37,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_shared)
| ~ m_main_v_CMD(X0,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_30) ).
fof(f38,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_shared)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_31) ).
fof(f39,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/sandbox2/benchmark/theBenchmark.p',m_main_32) ).
fof(f40,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_resp_h_invalid)
| ~ m_main_v_CMD(X0,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_33) ).
fof(f41,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_resp_h_invalid)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_34) ).
fof(f42,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_resp_h_shared)
| ~ m_main_v_CMD(X0,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_35) ).
fof(f43,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_write_h_resp_h_shared)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_36) ).
fof(f44,axiom,
! [X0] :
( ~ m_main_v_CMD(X0,c_invalidate)
| ~ m_main_v_CMD(X0,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_37) ).
fof(f45,axiom,
! [X0,X1] :
( m_memory_v_CMD(c_m,X0,X1)
| ~ m_main_v_CMD(X0,X1)
| ~ node1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_38) ).
fof(f46,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(c_m,X0,X1)
| m_main_v_CMD(X0,X1)
| ~ node1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_39) ).
fof(f47,axiom,
! [X0] : node1(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_40) ).
fof(f48,axiom,
! [X0] :
( m_memory_v_REPLY_h_OWNED(c_m,X0)
| ~ m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_41) ).
fof(f49,axiom,
! [X0] :
( ~ m_memory_v_REPLY_h_OWNED(c_m,X0)
| m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_42) ).
fof(f50,axiom,
! [X0] :
( m_memory_v_REPLY_h_WAITING(c_m,X0)
| ~ m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_43) ).
fof(f51,axiom,
! [X0] :
( ~ m_memory_v_REPLY_h_WAITING(c_m,X0)
| m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_44) ).
fof(f52,axiom,
! [X0] :
( m_memory_v_REPLY_h_STALL(c_m,X0)
| ~ m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_45) ).
fof(f53,axiom,
! [X0] :
( ~ m_memory_v_REPLY_h_STALL(c_m,X0)
| m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_46) ).
fof(f54,axiom,
! [X0,X1] :
( m_processor_v_CMD(c_p0,X0,X1)
| ~ m_main_v_CMD(X0,X1)
| ~ node2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_47) ).
fof(f55,axiom,
! [X0,X1] :
( ~ m_processor_v_CMD(c_p0,X0,X1)
| m_main_v_CMD(X0,X1)
| ~ node2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_48) ).
fof(f56,axiom,
! [X0] : node2(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_49) ).
fof(f57,axiom,
! [X0] :
( m_processor_v_REPLY_h_OWNED(c_p0,X0)
| ~ m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_50) ).
fof(f58,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_OWNED(c_p0,X0)
| m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_51) ).
fof(f59,axiom,
! [X0] :
( m_processor_v_REPLY_h_WAITING(c_p0,X0)
| ~ m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_52) ).
fof(f60,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_WAITING(c_p0,X0)
| m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_53) ).
fof(f61,axiom,
! [X0] :
( m_processor_v_REPLY_h_STALL(c_p0,X0)
| ~ m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_54) ).
fof(f62,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_STALL(c_p0,X0)
| m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_55) ).
fof(f63,axiom,
! [X0,X1] :
( m_processor_v_CMD(c_p1,X0,X1)
| ~ m_main_v_CMD(X0,X1)
| ~ node3(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_56) ).
fof(f64,axiom,
! [X0,X1] :
( ~ m_processor_v_CMD(c_p1,X0,X1)
| m_main_v_CMD(X0,X1)
| ~ node3(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_57) ).
fof(f65,axiom,
! [X0] : node3(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_58) ).
fof(f66,axiom,
! [X0] :
( m_processor_v_REPLY_h_OWNED(c_p1,X0)
| ~ m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_59) ).
fof(f67,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_OWNED(c_p1,X0)
| m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_60) ).
fof(f68,axiom,
! [X0] :
( m_processor_v_REPLY_h_WAITING(c_p1,X0)
| ~ m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_61) ).
fof(f69,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_WAITING(c_p1,X0)
| m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_62) ).
fof(f70,axiom,
! [X0] :
( m_processor_v_REPLY_h_STALL(c_p1,X0)
| ~ m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_63) ).
fof(f71,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_STALL(c_p1,X0)
| m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_64) ).
fof(f72,axiom,
! [X0,X1] :
( m_processor_v_CMD(c_p2,X0,X1)
| ~ m_main_v_CMD(X0,X1)
| ~ node4(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_65) ).
fof(f73,axiom,
! [X0,X1] :
( ~ m_processor_v_CMD(c_p2,X0,X1)
| m_main_v_CMD(X0,X1)
| ~ node4(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_66) ).
fof(f74,axiom,
! [X0] : node4(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_67) ).
fof(f75,axiom,
! [X0] :
( m_processor_v_REPLY_h_OWNED(c_p2,X0)
| ~ m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_68) ).
fof(f76,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_OWNED(c_p2,X0)
| m_main_v_REPLY_h_OWNED(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_69) ).
fof(f77,axiom,
! [X0] :
( m_processor_v_REPLY_h_WAITING(c_p2,X0)
| ~ m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_70) ).
fof(f78,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_WAITING(c_p2,X0)
| m_main_v_REPLY_h_WAITING(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_71) ).
fof(f79,axiom,
! [X0] :
( m_processor_v_REPLY_h_STALL(c_p2,X0)
| ~ m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_72) ).
fof(f80,axiom,
! [X0] :
( ~ m_processor_v_REPLY_h_STALL(c_p2,X0)
| m_main_v_REPLY_h_STALL(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_73) ).
fof(f81,axiom,
! [X0] :
( ~ m_processor_v_reply_h_owned(c_p0,X0)
| ~ node5(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_74) ).
fof(f82,axiom,
! [X0] :
( ~ m_processor_v_reply_h_owned(c_p1,X0)
| ~ node5(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_75) ).
fof(f83,axiom,
! [X0] :
( ~ m_processor_v_reply_h_owned(c_p2,X0)
| ~ node5(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_76) ).
fof(f84,axiom,
! [X0] :
( m_main_v_REPLY_h_OWNED(X0)
| node5(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_77) ).
fof(f85,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/sandbox2/benchmark/theBenchmark.p',m_main_78) ).
fof(f86,axiom,
! [X0] :
( ~ m_processor_v_reply_h_waiting(c_p0,X0)
| ~ node6(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_79) ).
fof(f87,axiom,
! [X0] :
( ~ m_processor_v_reply_h_waiting(c_p1,X0)
| ~ node6(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_80) ).
fof(f88,axiom,
! [X0] :
( ~ m_processor_v_reply_h_waiting(c_p2,X0)
| ~ node6(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_81) ).
fof(f89,axiom,
! [X0] :
( m_main_v_REPLY_h_WAITING(X0)
| node6(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_82) ).
fof(f90,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/sandbox2/benchmark/theBenchmark.p',m_main_83) ).
fof(f91,axiom,
! [X0] :
( ~ m_processor_v_reply_h_stall(c_p0,X0)
| ~ node7(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_84) ).
fof(f92,axiom,
! [X0] :
( ~ m_processor_v_reply_h_stall(c_p1,X0)
| ~ node7(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_85) ).
fof(f93,axiom,
! [X0] :
( ~ m_processor_v_reply_h_stall(c_p2,X0)
| ~ node7(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_86) ).
fof(f94,axiom,
! [X0] :
( ~ m_memory_v_reply_h_stall(c_m,X0)
| ~ node7(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_87) ).
fof(f95,axiom,
! [X0] :
( m_main_v_REPLY_h_STALL(X0)
| node7(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_88) ).
fof(f96,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/sandbox2/benchmark/theBenchmark.p',m_main_89) ).
fof(f97,axiom,
! [X0,X1] :
( m_main_v_CMD(X0,X1)
| ~ m_processor_v_cmd(c_p0,X0,X1)
| ~ node8(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_90) ).
fof(f98,axiom,
! [X0,X1] :
( ~ m_main_v_CMD(X0,X1)
| m_processor_v_cmd(c_p0,X0,X1)
| ~ node8(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_91) ).
fof(f99,axiom,
! [X0] :
( m_processor_v_cmd(c_p1,X0,c_idle)
| ~ node9(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_92) ).
fof(f100,axiom,
! [X0] :
( m_processor_v_cmd(c_p2,X0,c_idle)
| ~ node9(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_93) ).
fof(f101,axiom,
! [X0] :
( m_memory_v_cmd(c_m,X0,c_idle)
| ~ node9(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_94) ).
fof(f102,axiom,
! [X0,X1] :
( m_main_v_CMD(X0,X1)
| ~ m_processor_v_cmd(c_p1,X0,X1)
| ~ node10(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_95) ).
fof(f103,axiom,
! [X0,X1] :
( ~ m_main_v_CMD(X0,X1)
| m_processor_v_cmd(c_p1,X0,X1)
| ~ node10(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_96) ).
fof(f104,axiom,
! [X0] :
( m_processor_v_cmd(c_p0,X0,c_idle)
| ~ node11(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_97) ).
fof(f105,axiom,
! [X0] :
( m_processor_v_cmd(c_p2,X0,c_idle)
| ~ node11(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_98) ).
fof(f106,axiom,
! [X0] :
( m_memory_v_cmd(c_m,X0,c_idle)
| ~ node11(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_99) ).
fof(f107,axiom,
! [X0,X1] :
( m_main_v_CMD(X0,X1)
| ~ m_processor_v_cmd(c_p0,X0,X1)
| ~ node12(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_100) ).
fof(f108,axiom,
! [X0,X1] :
( ~ m_main_v_CMD(X0,X1)
| m_processor_v_cmd(c_p0,X0,X1)
| ~ node12(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_101) ).
fof(f109,axiom,
! [X0] :
( m_processor_v_cmd(c_p0,X0,c_idle)
| ~ node13(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_102) ).
fof(f110,axiom,
! [X0] :
( m_processor_v_cmd(c_p1,X0,c_idle)
| ~ node13(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_103) ).
fof(f111,axiom,
! [X0] :
( m_memory_v_cmd(c_m,X0,c_idle)
| ~ node13(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_104) ).
fof(f112,axiom,
! [X0,X1] :
( m_main_v_CMD(X0,X1)
| ~ m_memory_v_cmd(c_m,X0,X1)
| ~ node14(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_105) ).
fof(f113,axiom,
! [X0,X1] :
( ~ m_main_v_CMD(X0,X1)
| m_memory_v_cmd(c_m,X0,X1)
| ~ node14(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_106) ).
fof(f114,axiom,
! [X0] :
( m_processor_v_cmd(c_p0,X0,c_idle)
| ~ node15(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_107) ).
fof(f115,axiom,
! [X0] :
( m_processor_v_cmd(c_p1,X0,c_idle)
| ~ node15(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_108) ).
fof(f116,axiom,
! [X0] :
( m_processor_v_cmd(c_p2,X0,c_idle)
| ~ node15(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_109) ).
fof(f117,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/sandbox2/benchmark/theBenchmark.p',m_main_110) ).
fof(f118,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/sandbox2/benchmark/theBenchmark.p',m_main_111) ).
fof(f119,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/sandbox2/benchmark/theBenchmark.p',m_main_112) ).
fof(f120,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/sandbox2/benchmark/theBenchmark.p',m_main_113) ).
fof(f121,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/sandbox2/benchmark/theBenchmark.p',m_main_114) ).
fof(f122,axiom,
! [X0] :
( ~ m_processor_v_master(c_p0,X0)
| m_processor_v_master(c_p0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_115) ).
fof(f123,axiom,
! [X0] :
( ~ m_processor_v_master(c_p0,X0)
| ~ m_processor_v_master(c_p1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_116) ).
fof(f124,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/sandbox2/benchmark/theBenchmark.p',m_main_117) ).
fof(f125,axiom,
! [X0] :
( ~ m_processor_v_master(c_p0,X0)
| ~ node16(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_118) ).
fof(f126,axiom,
! [X0] :
( ~ m_processor_v_master(c_p1,X0)
| ~ node16(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_119) ).
fof(f127,axiom,
! [X0] :
( node16(X0)
| ~ m_processor_v_master(c_p2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_120) ).
fof(f128,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/sandbox2/benchmark/theBenchmark.p',m_main_121) ).
fof(f129,axiom,
! [X0] :
( ~ m_processor_v_master(c_p0,X0)
| ~ node17(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_122) ).
fof(f130,axiom,
! [X0] :
( ~ m_processor_v_master(c_p1,X0)
| ~ node17(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_123) ).
fof(f131,axiom,
! [X0] :
( ~ m_processor_v_master(c_p2,X0)
| ~ node17(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_124) ).
fof(f132,axiom,
! [X0] :
( node17(X0)
| ~ m_memory_v_master(c_m,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_125) ).
fof(f133,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/sandbox2/benchmark/theBenchmark.p',m_main_126) ).
fof(f134,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/sandbox2/benchmark/theBenchmark.p',m_memory_1) ).
fof(f135,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_cmd(X0,X1,c_read_h_shared) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_2) ).
fof(f136,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_cmd(X0,X1,c_read_h_owned) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_3) ).
fof(f137,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_cmd(X0,X1,c_write_h_invalid) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_4) ).
fof(f138,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_cmd(X0,X1,c_write_h_shared) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_5) ).
fof(f139,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/sandbox2/benchmark/theBenchmark.p',m_memory_6) ).
fof(f140,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/sandbox2/benchmark/theBenchmark.p',m_memory_7) ).
fof(f141,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_8) ).
fof(f142,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_idle)
| ~ m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_9) ).
fof(f143,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/sandbox2/benchmark/theBenchmark.p',m_memory_10) ).
fof(f144,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/sandbox2/benchmark/theBenchmark.p',m_memory_11) ).
fof(f145,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/sandbox2/benchmark/theBenchmark.p',m_memory_12) ).
fof(f146,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/sandbox2/benchmark/theBenchmark.p',m_memory_13) ).
fof(f147,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/sandbox2/benchmark/theBenchmark.p',m_memory_14) ).
fof(f148,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_15) ).
fof(f149,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_16) ).
fof(f150,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/sandbox2/benchmark/theBenchmark.p',m_memory_17) ).
fof(f151,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/sandbox2/benchmark/theBenchmark.p',m_memory_18) ).
fof(f152,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/sandbox2/benchmark/theBenchmark.p',m_memory_19) ).
fof(f153,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/sandbox2/benchmark/theBenchmark.p',m_memory_20) ).
fof(f154,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_owned)
| ~ m_memory_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_21) ).
fof(f155,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_read_h_owned)
| ~ m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_22) ).
fof(f156,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/sandbox2/benchmark/theBenchmark.p',m_memory_23) ).
fof(f157,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/sandbox2/benchmark/theBenchmark.p',m_memory_24) ).
fof(f158,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/sandbox2/benchmark/theBenchmark.p',m_memory_25) ).
fof(f159,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_invalid)
| ~ m_memory_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_26) ).
fof(f160,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_invalid)
| ~ m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_27) ).
fof(f161,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/sandbox2/benchmark/theBenchmark.p',m_memory_28) ).
fof(f162,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/sandbox2/benchmark/theBenchmark.p',m_memory_29) ).
fof(f163,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_30) ).
fof(f164,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_write_h_shared)
| ~ m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_31) ).
fof(f165,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/sandbox2/benchmark/theBenchmark.p',m_memory_32) ).
fof(f166,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/sandbox2/benchmark/theBenchmark.p',m_memory_33) ).
fof(f167,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/sandbox2/benchmark/theBenchmark.p',m_memory_34) ).
fof(f168,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/sandbox2/benchmark/theBenchmark.p',m_memory_35) ).
fof(f169,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/sandbox2/benchmark/theBenchmark.p',m_memory_36) ).
fof(f170,axiom,
! [X0,X1] :
( ~ m_memory_v_cmd(X0,X1,c_invalidate)
| ~ m_memory_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_37) ).
fof(f171,axiom,
! [X0] : ~ m_memory_v_busy(X0,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_38) ).
fof(f172,axiom,
! [X2,X0,X1] :
( m_memory_v_busy(X0,X1)
| ~ m_memory_v_busy(X0,X2)
| ~ node18(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_39) ).
fof(f173,axiom,
! [X2,X0,X1] :
( ~ m_memory_v_busy(X0,X1)
| m_memory_v_busy(X0,X2)
| ~ node18(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_40) ).
fof(f174,axiom,
! [X0,X1] :
( m_memory_v_master(X0,X1)
| ~ node19(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_41) ).
fof(f175,axiom,
! [X0,X1] :
( m_memory_v_CMD(X0,X1,c_response)
| ~ node19(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_42) ).
fof(f176,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_owned)
| ~ node20(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_43) ).
fof(f177,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_shared)
| ~ node20(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_44) ).
fof(f178,axiom,
! [X0,X1] :
( ~ m_memory_v_master(X0,X1)
| ~ node21(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_45) ).
fof(f179,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/sandbox2/benchmark/theBenchmark.p',m_memory_46) ).
fof(f180,axiom,
! [X2,X0,X1] :
( m_memory_v_busy(X0,X1)
| ~ m_memory_v_busy(X0,X2)
| ~ node22(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_47) ).
fof(f181,axiom,
! [X2,X0,X1] :
( ~ m_memory_v_busy(X0,X1)
| m_memory_v_busy(X0,X2)
| ~ node22(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_48) ).
fof(f182,axiom,
! [X2,X0,X1] :
( ~ m_memory_v_abort(X0,X1)
| node18(X0,X1,X2)
| ~ node23(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_49) ).
fof(f183,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/sandbox2/benchmark/theBenchmark.p',m_memory_50) ).
fof(f184,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/sandbox2/benchmark/theBenchmark.p',m_memory_51) ).
fof(f185,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/sandbox2/benchmark/theBenchmark.p',m_memory_52) ).
fof(f186,axiom,
! [X2,X0,X1] :
( ~ trans(X0,X1)
| node23(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_53) ).
fof(f189,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_shared)
| ~ node24(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_56) ).
fof(f190,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_owned)
| ~ node24(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_57) ).
fof(f191,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_shared)
| ~ node25(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_58) ).
fof(f192,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_owned)
| ~ node25(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_59) ).
fof(f193,axiom,
! [X0,X1] :
( ~ m_memory_v_REPLY_h_STALL(X0,X1)
| ~ node26(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_60) ).
fof(f194,axiom,
! [X0,X1] :
( node24(X0,X1)
| ~ m_memory_v_REPLY_h_WAITING(X0,X1)
| ~ node26(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_61) ).
fof(f195,axiom,
! [X0,X1] :
( node25(X0,X1)
| ~ m_memory_v_REPLY_h_OWNED(X0,X1)
| ~ node26(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_62) ).
fof(f196,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/sandbox2/benchmark/theBenchmark.p',m_memory_63) ).
fof(f197,axiom,
! [X0,X1] :
( m_memory_v_REPLY_h_WAITING(X0,X1)
| ~ node27(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_64) ).
fof(f198,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/sandbox2/benchmark/theBenchmark.p',m_memory_65) ).
fof(f199,axiom,
! [X0,X1] :
( m_memory_v_REPLY_h_OWNED(X0,X1)
| ~ node28(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_66) ).
fof(f200,axiom,
! [X0,X1] :
( m_memory_v_abort(X0,X1)
| node26(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_67) ).
fof(f201,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/sandbox2/benchmark/theBenchmark.p',m_memory_68) ).
fof(f202,axiom,
! [X0,X1] :
( m_memory_v_master(X0,X1)
| ~ node29(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_69) ).
fof(f203,axiom,
! [X0,X1] :
( m_memory_v_busy(X0,X1)
| ~ node29(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_70) ).
fof(f204,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/sandbox2/benchmark/theBenchmark.p',m_memory_71) ).
fof(f205,axiom,
! [X0,X1] :
( node29(X0,X1)
| m_memory_v_cmd(X0,X1,c_idle) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_72) ).
fof(f206,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_shared)
| ~ node30(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_73) ).
fof(f207,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_read_h_owned)
| ~ node30(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_74) ).
fof(f208,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_write_h_invalid)
| ~ node30(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_75) ).
fof(f209,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_write_h_shared)
| ~ node30(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_76) ).
fof(f210,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_write_h_resp_h_invalid)
| ~ node30(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_77) ).
fof(f211,axiom,
! [X0,X1] :
( ~ m_memory_v_CMD(X0,X1,c_write_h_resp_h_shared)
| ~ node30(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_78) ).
fof(f212,axiom,
! [X0,X1] :
( m_memory_v_busy(X0,X1)
| ~ node31(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_79) ).
fof(f213,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/sandbox2/benchmark/theBenchmark.p',m_memory_80) ).
fof(f214,axiom,
! [X0,X1] :
( ~ m_memory_v_busy(X0,X1)
| node30(X0,X1)
| m_memory_v_reply_h_stall(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_memory_81) ).
fof(f215,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/sandbox2/benchmark/theBenchmark.p',m_memory_82) ).
fof(f216,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/sandbox2/benchmark/theBenchmark.p',m_processor_1) ).
fof(f217,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_idle)
| ~ m_processor_v_cmd(X0,X1,c_read_h_shared) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_2) ).
fof(f218,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_idle)
| ~ m_processor_v_cmd(X0,X1,c_read_h_owned) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_3) ).
fof(f219,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_idle)
| ~ m_processor_v_cmd(X0,X1,c_write_h_invalid) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_4) ).
fof(f220,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_idle)
| ~ m_processor_v_cmd(X0,X1,c_write_h_shared) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_5) ).
fof(f221,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/sandbox2/benchmark/theBenchmark.p',m_processor_6) ).
fof(f222,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/sandbox2/benchmark/theBenchmark.p',m_processor_7) ).
fof(f223,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_idle)
| ~ m_processor_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_8) ).
fof(f224,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_idle)
| ~ m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_9) ).
fof(f225,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/sandbox2/benchmark/theBenchmark.p',m_processor_10) ).
fof(f226,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/sandbox2/benchmark/theBenchmark.p',m_processor_11) ).
fof(f227,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/sandbox2/benchmark/theBenchmark.p',m_processor_12) ).
fof(f228,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/sandbox2/benchmark/theBenchmark.p',m_processor_13) ).
fof(f229,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/sandbox2/benchmark/theBenchmark.p',m_processor_14) ).
fof(f230,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_15) ).
fof(f231,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_16) ).
fof(f232,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/sandbox2/benchmark/theBenchmark.p',m_processor_17) ).
fof(f233,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/sandbox2/benchmark/theBenchmark.p',m_processor_18) ).
fof(f234,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/sandbox2/benchmark/theBenchmark.p',m_processor_19) ).
fof(f235,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/sandbox2/benchmark/theBenchmark.p',m_processor_20) ).
fof(f236,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_owned)
| ~ m_processor_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_21) ).
fof(f237,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_read_h_owned)
| ~ m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_22) ).
fof(f238,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/sandbox2/benchmark/theBenchmark.p',m_processor_23) ).
fof(f239,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/sandbox2/benchmark/theBenchmark.p',m_processor_24) ).
fof(f240,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/sandbox2/benchmark/theBenchmark.p',m_processor_25) ).
fof(f241,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_invalid)
| ~ m_processor_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_26) ).
fof(f242,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_invalid)
| ~ m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_27) ).
fof(f243,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/sandbox2/benchmark/theBenchmark.p',m_processor_28) ).
fof(f244,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/sandbox2/benchmark/theBenchmark.p',m_processor_29) ).
fof(f245,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_invalidate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_30) ).
fof(f246,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_write_h_shared)
| ~ m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_31) ).
fof(f247,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/sandbox2/benchmark/theBenchmark.p',m_processor_32) ).
fof(f248,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/sandbox2/benchmark/theBenchmark.p',m_processor_33) ).
fof(f249,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/sandbox2/benchmark/theBenchmark.p',m_processor_34) ).
fof(f250,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/sandbox2/benchmark/theBenchmark.p',m_processor_35) ).
fof(f251,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/sandbox2/benchmark/theBenchmark.p',m_processor_36) ).
fof(f252,axiom,
! [X0,X1] :
( ~ m_processor_v_cmd(X0,X1,c_invalidate)
| ~ m_processor_v_cmd(X0,X1,c_response) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_37) ).
fof(f253,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/sandbox2/benchmark/theBenchmark.p',m_processor_38) ).
fof(f254,axiom,
! [X0,X1] :
( ~ m_processor_v_snoop(X0,X1,c_invalid)
| ~ m_processor_v_snoop(X0,X1,c_owned) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_39) ).
fof(f255,axiom,
! [X0,X1] :
( ~ m_processor_v_snoop(X0,X1,c_invalid)
| ~ m_processor_v_snoop(X0,X1,c_shared) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_40) ).
fof(f256,axiom,
! [X0,X1] :
( ~ m_processor_v_snoop(X0,X1,c_owned)
| ~ m_processor_v_snoop(X0,X1,c_shared) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_41) ).
fof(f257,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/sandbox2/benchmark/theBenchmark.p',m_processor_42) ).
fof(f258,axiom,
! [X0,X1] :
( ~ m_processor_v_state(X0,X1,c_invalid)
| ~ m_processor_v_state(X0,X1,c_shared) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_43) ).
fof(f259,axiom,
! [X0,X1] :
( ~ m_processor_v_state(X0,X1,c_invalid)
| ~ m_processor_v_state(X0,X1,c_owned) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_44) ).
fof(f260,axiom,
! [X0,X1] :
( ~ m_processor_v_state(X0,X1,c_shared)
| ~ m_processor_v_state(X0,X1,c_owned) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_45) ).
fof(f261,axiom,
! [X0] : m_processor_v_state(X0,s0,c_invalid),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_46) ).
fof(f262,axiom,
! [X0] : m_processor_v_snoop(X0,s0,c_invalid),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_47) ).
fof(f263,axiom,
! [X0] : ~ m_processor_v_waiting(X0,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_48) ).
fof(f264,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/sandbox2/benchmark/theBenchmark.p',m_processor_49) ).
fof(f265,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/sandbox2/benchmark/theBenchmark.p',m_processor_50) ).
fof(f266,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/sandbox2/benchmark/theBenchmark.p',m_processor_51) ).
fof(f267,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/sandbox2/benchmark/theBenchmark.p',m_processor_52) ).
fof(f268,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/sandbox2/benchmark/theBenchmark.p',m_processor_53) ).
fof(f269,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/sandbox2/benchmark/theBenchmark.p',m_processor_54) ).
fof(f270,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/sandbox2/benchmark/theBenchmark.p',m_processor_55) ).
fof(f271,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/sandbox2/benchmark/theBenchmark.p',m_processor_56) ).
fof(f272,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/sandbox2/benchmark/theBenchmark.p',m_processor_57) ).
fof(f273,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/sandbox2/benchmark/theBenchmark.p',m_processor_58) ).
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_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/sandbox2/benchmark/theBenchmark.p',m_processor_59) ).
fof(f275,axiom,
! [X0,X1] :
( ~ m_processor_v_CMD(X0,X1,c_read_h_owned)
| ~ node35(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_60) ).
fof(f276,axiom,
! [X0,X1] :
( ~ m_processor_v_CMD(X0,X1,c_invalidate)
| ~ node35(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_61) ).
fof(f277,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node36(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_62) ).
fof(f278,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_shared)
| ~ node36(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_63) ).
fof(f279,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/sandbox2/benchmark/theBenchmark.p',m_processor_64) ).
fof(f280,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/sandbox2/benchmark/theBenchmark.p',m_processor_65) ).
fof(f281,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/sandbox2/benchmark/theBenchmark.p',m_processor_66) ).
fof(f282,axiom,
! [X2,X0,X1] :
( ~ m_processor_v_abort(X0,X1)
| node32(X0,X1,X2)
| ~ node38(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_67) ).
fof(f283,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/sandbox2/benchmark/theBenchmark.p',m_processor_68) ).
fof(f284,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/sandbox2/benchmark/theBenchmark.p',m_processor_69) ).
fof(f285,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/sandbox2/benchmark/theBenchmark.p',m_processor_70) ).
fof(f286,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/sandbox2/benchmark/theBenchmark.p',m_processor_71) ).
fof(f287,axiom,
! [X2,X0,X1] :
( ~ trans(X0,X1)
| node38(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_72) ).
fof(f288,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/sandbox2/benchmark/theBenchmark.p',m_processor_73) ).
fof(f289,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/sandbox2/benchmark/theBenchmark.p',m_processor_74) ).
fof(f290,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node40(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_75) ).
fof(f291,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_owned)
| ~ node40(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_76) ).
fof(f292,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_shared)
| ~ node40(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_77) ).
fof(f293,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node41(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_78) ).
fof(f294,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_owned)
| ~ node41(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_79) ).
fof(f295,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_shared)
| ~ node41(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_80) ).
fof(f296,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node42(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_81) ).
fof(f297,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_write_h_resp_h_invalid)
| ~ node42(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_82) ).
fof(f298,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node43(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_83) ).
fof(f299,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_write_h_resp_h_shared)
| ~ node43(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_84) ).
fof(f300,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/sandbox2/benchmark/theBenchmark.p',m_processor_85) ).
fof(f301,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/sandbox2/benchmark/theBenchmark.p',m_processor_86) ).
fof(f302,axiom,
! [X2,X0,X1] :
( ~ m_processor_v_abort(X0,X1)
| node39(X0,X1,X2)
| ~ node45(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_87) ).
fof(f303,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/sandbox2/benchmark/theBenchmark.p',m_processor_88) ).
fof(f304,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/sandbox2/benchmark/theBenchmark.p',m_processor_89) ).
fof(f305,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/sandbox2/benchmark/theBenchmark.p',m_processor_90) ).
fof(f306,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/sandbox2/benchmark/theBenchmark.p',m_processor_91) ).
fof(f307,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/sandbox2/benchmark/theBenchmark.p',m_processor_92) ).
fof(f308,axiom,
! [X2,X0,X1] :
( ~ trans(X0,X1)
| node45(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_93) ).
fof(f309,axiom,
! [X2,X0,X1] :
( m_processor_v_waiting(X0,X1)
| ~ m_processor_v_waiting(X0,X2)
| ~ node46(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_94) ).
fof(f310,axiom,
! [X2,X0,X1] :
( ~ m_processor_v_waiting(X0,X1)
| m_processor_v_waiting(X0,X2)
| ~ node46(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_95) ).
fof(f311,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node47(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_96) ).
fof(f312,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_shared)
| ~ node47(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_97) ).
fof(f313,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node48(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_98) ).
fof(f314,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_read_h_owned)
| ~ node48(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_99) ).
fof(f315,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node49(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_100) ).
fof(f316,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_response)
| ~ node49(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_101) ).
fof(f317,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node50(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_102) ).
fof(f318,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_write_h_resp_h_invalid)
| ~ node50(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_103) ).
fof(f319,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node51(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_104) ).
fof(f320,axiom,
! [X0,X1] :
( m_processor_v_CMD(X0,X1,c_write_h_resp_h_shared)
| ~ node51(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_105) ).
fof(f321,axiom,
! [X2,X0,X1] :
( m_processor_v_waiting(X0,X1)
| ~ m_processor_v_waiting(X0,X2)
| ~ node52(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_106) ).
fof(f322,axiom,
! [X2,X0,X1] :
( ~ m_processor_v_waiting(X0,X1)
| m_processor_v_waiting(X0,X2)
| ~ node52(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_107) ).
fof(f323,axiom,
! [X2,X0,X1] :
( ~ m_processor_v_abort(X0,X1)
| node46(X0,X1,X2)
| ~ node53(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_108) ).
fof(f324,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/sandbox2/benchmark/theBenchmark.p',m_processor_109) ).
fof(f325,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/sandbox2/benchmark/theBenchmark.p',m_processor_110) ).
fof(f326,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/sandbox2/benchmark/theBenchmark.p',m_processor_111) ).
fof(f327,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/sandbox2/benchmark/theBenchmark.p',m_processor_112) ).
fof(f328,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/sandbox2/benchmark/theBenchmark.p',m_processor_113) ).
fof(f329,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/sandbox2/benchmark/theBenchmark.p',m_processor_114) ).
fof(f330,axiom,
! [X2,X0,X1] :
( ~ trans(X0,X1)
| node53(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_115) ).
fof(f331,axiom,
! [X0,X1] :
( ~ m_processor_v_state(X0,X1,c_shared)
| ~ node54(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_116) ).
fof(f332,axiom,
! [X0,X1] :
( ~ m_processor_v_state(X0,X1,c_owned)
| ~ node54(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_117) ).
fof(f333,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/sandbox2/benchmark/theBenchmark.p',m_processor_118) ).
fof(f334,axiom,
! [X0,X1] :
( ~ m_processor_v_waiting(X0,X1)
| ~ node55(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_119) ).
fof(f335,axiom,
! [X0,X1] :
( m_processor_v_readable(X0,X1)
| node54(X0,X1)
| m_processor_v_waiting(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_120) ).
fof(f336,axiom,
! [X0,X1] :
( ~ m_processor_v_readable(X0,X1)
| node55(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_121) ).
fof(f337,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_owned)
| ~ node56(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_122) ).
fof(f338,axiom,
! [X0,X1] :
( ~ m_processor_v_waiting(X0,X1)
| ~ node56(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_123) ).
fof(f339,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/sandbox2/benchmark/theBenchmark.p',m_processor_124) ).
fof(f340,axiom,
! [X0,X1] :
( ~ m_processor_v_writable(X0,X1)
| node56(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_125) ).
fof(f341,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node57(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_126) ).
fof(f342,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_owned)
| ~ node57(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_127) ).
fof(f343,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/sandbox2/benchmark/theBenchmark.p',m_processor_128) ).
fof(f344,axiom,
! [X0,X1] :
( ~ m_processor_v_reply_h_owned(X0,X1)
| node57(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_129) ).
fof(f345,axiom,
! [X0,X1] :
( ~ m_processor_v_master(X0,X1)
| ~ node58(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_130) ).
fof(f346,axiom,
! [X0,X1] :
( m_processor_v_waiting(X0,X1)
| ~ node58(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_131) ).
fof(f347,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/sandbox2/benchmark/theBenchmark.p',m_processor_132) ).
fof(f348,axiom,
! [X0,X1] :
( ~ m_processor_v_reply_h_waiting(X0,X1)
| node58(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_133) ).
fof(f349,axiom,
! [X0,X1] :
( ~ m_processor_v_CMD(X0,X1,c_read_h_shared)
| ~ node59(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_134) ).
fof(f350,axiom,
! [X0,X1] :
( ~ m_processor_v_CMD(X0,X1,c_read_h_owned)
| ~ node59(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_135) ).
fof(f351,axiom,
! [X0,X1] :
( ~ m_processor_v_REPLY_h_STALL(X0,X1)
| ~ node60(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_136) ).
fof(f352,axiom,
! [X0,X1] :
( node59(X0,X1)
| ~ m_processor_v_REPLY_h_WAITING(X0,X1)
| ~ node60(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_137) ).
fof(f353,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/sandbox2/benchmark/theBenchmark.p',m_processor_138) ).
fof(f354,axiom,
! [X0,X1] :
( m_processor_v_REPLY_h_WAITING(X0,X1)
| ~ node61(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_139) ).
fof(f355,axiom,
! [X0,X1] :
( m_processor_v_abort(X0,X1)
| node60(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_140) ).
fof(f356,axiom,
! [X0,X1] :
( ~ m_processor_v_abort(X0,X1)
| m_processor_v_REPLY_h_STALL(X0,X1)
| node61(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_141) ).
fof(f357,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node62(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_142) ).
fof(f358,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_invalid)
| ~ node62(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_143) ).
fof(f359,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node63(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_144) ).
fof(f360,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_shared)
| ~ node63(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_145) ).
fof(f361,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node64(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_146) ).
fof(f362,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_owned)
| ~ node64(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_147) ).
fof(f363,axiom,
! [X0,X1] :
( m_processor_v_snoop(X0,X1,c_owned)
| ~ node64(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_148) ).
fof(f364,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node65(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_149) ).
fof(f365,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_owned)
| ~ node65(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_150) ).
fof(f366,axiom,
! [X0,X1] :
( m_processor_v_snoop(X0,X1,c_shared)
| ~ node65(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_151) ).
fof(f367,axiom,
! [X0,X1] :
( m_processor_v_master(X0,X1)
| ~ node66(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_152) ).
fof(f368,axiom,
! [X0,X1] :
( m_processor_v_state(X0,X1,c_owned)
| ~ node66(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_153) ).
fof(f369,axiom,
! [X0,X1] :
( m_processor_v_snoop(X0,X1,c_invalid)
| ~ node66(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_processor_154) ).
fof(f370,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/sandbox2/benchmark/theBenchmark.p',m_processor_155) ).
fof(f371,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/sandbox2/benchmark/theBenchmark.p',m_processor_156) ).
fof(f372,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/sandbox2/benchmark/theBenchmark.p',m_processor_157) ).
fof(f373,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/sandbox2/benchmark/theBenchmark.p',m_processor_158) ).
fof(f374,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/sandbox2/benchmark/theBenchmark.p',m_processor_159) ).
fof(f375,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/sandbox2/benchmark/theBenchmark.p',m_processor_160) ).
fof(f376,negated_conjecture,
! [X0] :
( m_processor_v_writable(c_p0,X0)
| ~ node67(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty1) ).
fof(f377,negated_conjecture,
! [X0] :
( m_processor_v_writable(c_p1,X0)
| ~ node67(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty2) ).
fof(f378,negated_conjecture,
! [X0] :
( node67(X0)
| xuntil69(X0)
| ~ until68(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty3) ).
fof(f379,negated_conjecture,
! [X0,X1] :
( until68(X0)
| ~ succ(X1,X0)
| ~ xuntil69(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty4) ).
fof(f380,negated_conjecture,
! [X0] :
( loop
| ~ last(X0)
| ~ xuntil69(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty5) ).
fof(f381,negated_conjecture,
! [X0,X1] :
( until2p70(X0)
| ~ trans(X1,X0)
| ~ last(X1)
| ~ xuntil69(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty6) ).
fof(f382,negated_conjecture,
! [X0] :
( node67(X0)
| xuntil2p71(X0)
| ~ until2p70(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty7) ).
fof(f383,negated_conjecture,
! [X0,X1] :
( until2p70(X0)
| ~ succ(X1,X0)
| ~ xuntil2p71(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty8) ).
fof(f384,negated_conjecture,
! [X0] :
( ~ last(X0)
| ~ xuntil2p71(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty9) ).
fof(f385,negated_conjecture,
until68(s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty10) ).
fof(f1214,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,f189,f190,f191,f192,f193,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]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV420-1.005 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n009.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 10:56:30 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.43/2.17 % (2954187)Will run a generic schedule for satisfiability detection.
% 13.43/2.17 % (2954203)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=143004449:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.43/2.17 % (2954202)% WARNING: option uhcvi not known.
% 13.43/2.17 % (2954201)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3530286350_2999 on theBenchmark for (2999ds/0Mi)
% 13.43/2.17 % (2954202)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4195454626:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.43/2.17 % (2954204)dis+10_1_sil=32000:sp=arity:random_seed=2355010548:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.43/2.17 % (2954208)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3900113570:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.43/2.17 % (2954205)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=912159797:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.43/2.17 % (2954206)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2845898858:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.43/2.17 % Detected minimum model sizes of [1]
% 13.43/2.17 % Detected maximum model sizes of [21]
% 13.43/2.17 % TRYING [1]
% 13.43/2.17 % TRYING [2]
% 13.43/2.17 % TRYING [3]
% 13.43/2.17 % TRYING [4]
% 13.43/2.17 % (2954205)Instruction limit reached!
% 13.43/2.17 % (2954205)------------------------------
% 13.43/2.17 % (2954205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.17 % (2954205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.17 % (2954205)CaDiCaL version: 2.1.3
% 13.43/2.17 % (2954205)Termination reason: Instruction limit
% 13.43/2.17 % (2954205)Termination phase: Saturation
% 13.43/2.17 % (2954205)Time elapsed: 0.049 s
% 13.43/2.17 % (2954205)Peak memory usage: 12 MB
% 13.43/2.17 % (2954205)Instructions burned: 117 (million)
% 13.43/2.17 % (2954204)Instruction limit reached!
% 13.43/2.17 % (2954204)------------------------------
% 13.43/2.17 % (2954204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.17 % (2954204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.17 % (2954204)CaDiCaL version: 2.1.3
% 13.43/2.17 % (2954204)Termination reason: Instruction limit
% 13.43/2.17 % (2954204)Termination phase: Saturation
% 13.43/2.17 % (2954204)Time elapsed: 0.059 s
% 13.43/2.17 % (2954204)Peak memory usage: 12 MB
% 13.43/2.17 % (2954204)Instructions burned: 103 (million)
% 13.43/2.17 % (2954206)Instruction limit reached!
% 13.43/2.17 % (2954206)------------------------------
% 13.43/2.17 % (2954206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.17 % (2954206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.17 % (2954206)CaDiCaL version: 2.1.3
% 13.43/2.17 % (2954206)Termination reason: Instruction limit
% 13.43/2.17 % (2954206)Termination phase: Saturation
% 13.43/2.17 % (2954206)Time elapsed: 0.065 s
% 13.43/2.17 % (2954206)Peak memory usage: 13 MB
% 13.43/2.17 % (2954206)Instructions burned: 132 (million)
% 13.43/2.17 % (2954245)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2344122959:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.43/2.17 % (2954254)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1724465977:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 13.43/2.17 % (2954258)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=3667561920:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.43/2.17 % Detected minimum model sizes of [1]
% 13.43/2.17 % Detected maximum model sizes of [21]
% 13.43/2.17 % TRYING [1]
% 13.43/2.17 % TRYING [2]
% 13.43/2.17 % TRYING [3]
% 13.43/2.17 % (2954208)Instruction limit reached!
% 13.43/2.17 % (2954208)------------------------------
% 13.43/2.17 % (2954208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.17 % (2954208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.17 % (2954208)CaDiCaL version: 2.1.3
% 13.43/2.17 % (2954208)Termination reason: Instruction limit
% 13.43/2.17 % (2954208)Termination phase: Saturation
% 13.43/2.17 % (2954208)Time elapsed: 0.099 s
% 13.43/2.17 % (2954208)Peak memory usage: 14 MB
% 13.43/2.17 % (2954208)Instructions burned: 159 (million)
% 13.43/2.17 % (2954268)ott-21_1_sil=16000:fs=off:random_seed=2354285426:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.43/2.17 % TRYING [5]
% 13.43/2.17 % TRYING [4]
% 13.43/2.17 % (2954254)Instruction limit reached!
% 13.43/2.17 % (2954254)------------------------------
% 13.43/2.17 % (2954254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.17 % (2954254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.17 % (2954254)CaDiCaL version: 2.1.3
% 13.43/2.17 % (2954254)Termination reason: Instruction limit
% 13.43/2.17 % (2954254)Termination phase: Saturation
% 13.43/2.17 % (2954254)Time elapsed: 0.076 s
% 13.43/2.17 % (2954254)Peak memory usage: 13 MB
% 13.43/2.17 % (2954254)Instructions burned: 132 (million)
% 13.43/2.17 % (2954282)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=625172203:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 13.43/2.17 % TRYING [5]
% 13.43/2.17 % (2954268)Instruction limit reached!
% 13.43/2.17 % (2954268)------------------------------
% 13.43/2.17 % (2954268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.17 % (2954268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.17 % (2954268)CaDiCaL version: 2.1.3
% 13.43/2.17 % (2954268)Termination reason: Instruction limit
% 13.43/2.17 % (2954268)Termination phase: Saturation
% 13.43/2.17 % (2954268)Time elapsed: 0.098 s
% 13.43/2.17 % (2954268)Peak memory usage: 13 MB
% 13.43/2.17 % (2954268)Instructions burned: 181 (million)
% 13.43/2.17 % (2954291)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4075958521:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 13.43/2.17 % TRYING [6]
% 13.43/2.17 % Detected minimum model sizes of [1]
% 13.43/2.17 % Detected maximum model sizes of [21]
% 13.43/2.17 % TRYING [1]
% 13.43/2.17 % TRYING [2]
% 13.43/2.17 % TRYING [3]
% 13.43/2.17 % TRYING [4]
% 13.43/2.17 % TRYING [6]
% 13.43/2.17 % TRYING [7]
% 13.43/2.17 % TRYING [5]
% 13.43/2.17 % (2954258)Instruction limit reached!
% 13.43/2.17 % (2954258)------------------------------
% 13.43/2.17 % (2954258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.17 % (2954258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.17 % (2954258)CaDiCaL version: 2.1.3
% 13.43/2.17 % (2954258)Termination reason: Instruction limit
% 13.43/2.17 % (2954258)Termination phase: Saturation
% 13.43/2.17 % (2954258)Time elapsed: 0.377 s
% 13.43/2.17 % (2954258)Peak memory usage: 17 MB
% 13.43/2.17 % (2954258)Instructions burned: 684 (million)
% 13.43/2.17 % (2954245)Instruction limit reached!
% 13.43/2.17 % (2954245)------------------------------
% 13.43/2.17 % (2954245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.17 % (2954245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.17 % (2954245)CaDiCaL version: 2.1.3
% 13.43/2.17 % (2954245)Termination reason: Instruction limit
% 13.43/2.17 % (2954245)Termination phase: Finite model building SAT solving
% 13.43/2.17 % (2954245)Time elapsed: 0.412 s
% 13.43/2.17 % (2954245)Peak memory usage: 19 MB
% 13.43/2.17 % (2954245)Instructions burned: 715 (million)
% 13.43/2.17 % (2954338)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1980811285:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 13.43/2.17 % TRYING [6]
% 13.43/2.17 % TRYING [8]
% 13.43/2.17 % (2954339)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2041583610:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 13.43/2.17 % (2954282)Instruction limit reached!
% 13.43/2.17 % (2954282)------------------------------
% 13.43/2.17 % (2954282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.17 % (2954282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.17 % (2954282)CaDiCaL version: 2.1.3
% 13.43/2.17 % (2954282)Termination reason: Instruction limit
% 13.43/2.17 % (2954282)Termination phase: Saturation
% 13.43/2.17 % (2954282)Time elapsed: 0.331 s
% 13.43/2.17 % (2954282)Peak memory usage: 15 MB
% 13.43/2.17 % (2954282)Instructions burned: 479 (million)
% 13.43/2.17 % Detected minimum model sizes of [1]
% 13.43/2.17 % Detected maximum model sizes of [21]
% 13.43/2.17 % (2954342)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=2871606762:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 13.43/2.17 % TRYING [14]
% 13.43/2.17 % TRYING [7]
% 13.43/2.17 % (2954291)Instruction limit reached!
% 13.43/2.17 % (2954291)------------------------------
% 13.43/2.17 % (2954291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.17 % (2954291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.17 % (2954291)CaDiCaL version: 2.1.3
% 13.43/2.17 % (2954291)Termination reason: Instruction limit
% 13.43/2.17 % (2954291)Termination phase: Finite model building SAT solving
% 13.43/2.17 % (2954291)Time elapsed: 0.383 s
% 13.43/2.17 % (2954291)Peak memory usage: 17 MB
% 13.43/2.17 % (2954291)Instructions burned: 867 (million)
% 13.43/2.17 % (2954344)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1141072949:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 13.43/2.17 % TRYING [9]
% 13.43/2.17 % (2954339)Cannot enumerate next child to try in an incomplete setup
% 13.43/2.17 % (2954339)Refutation not found, incomplete strategy
% 13.43/2.17 % (2954339)------------------------------
% 13.43/2.17 % (2954339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.17 % (2954339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.17 % (2954339)CaDiCaL version: 2.1.3
% 13.43/2.17 % (2954339)Termination reason: Refutation not found, incomplete strategy
% 13.43/2.17 % (2954339)Time elapsed: 0.204 s
% 13.43/2.17 % (2954339)Peak memory usage: 28 MB
% 13.43/2.17 % (2954339)Instructions burned: 462 (million)
% 13.43/2.17 % (2954339)------------------------------
% 13.43/2.17 % (2954339)------------------------------
% 13.43/2.17 % (2954346)fmb+10_1_sil=64000:random_seed=2413816932:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 13.43/2.17 % Detected minimum model sizes of [1]
% 13.43/2.17 % Detected maximum model sizes of [21]
% 13.43/2.17 % TRYING [1]
% 13.43/2.17 % TRYING [2]
% 13.43/2.17 % TRYING [3]
% 13.43/2.17 % TRYING [4]
% 13.43/2.17 % TRYING [10]
% 13.43/2.17 % TRYING [5]
% 13.43/2.17 % TRYING [11]
% 13.43/2.17 % (2954342)Instruction limit reached!
% 13.43/2.17 % (2954342)------------------------------
% 13.43/2.17 % (2954342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.17 % (2954342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.17 % (2954342)CaDiCaL version: 2.1.3
% 13.43/2.17 % (2954342)Termination reason: Instruction limit
% 13.43/2.17 % (2954342)Termination phase: Saturation
% 13.43/2.17 % (2954342)Time elapsed: 0.456 s
% 13.43/2.17 % (2954342)Peak memory usage: 18 MB
% 13.43/2.17 % (2954342)Instructions burned: 692 (million)
% 13.43/2.17 % TRYING [6]
% 13.43/2.17 % (2954356)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1279887996:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 13.43/2.17 % Detected minimum model sizes of [1]
% 13.43/2.17 % Detected maximum model sizes of [21]
% 13.43/2.17 % TRYING [20]
% 13.43/2.17 % TRYING [12]
% 13.43/2.17 % TRYING [7]
% 13.43/2.17 % (2954338)Instruction limit reached!
% 13.43/2.17 % (2954338)------------------------------
% 13.43/2.17 % (2954338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.17 % (2954338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.17 % (2954338)CaDiCaL version: 2.1.3
% 13.43/2.17 % (2954338)Termination reason: Instruction limit
% 13.43/2.17 % (2954338)Termination phase: Saturation
% 13.43/2.17 % (2954338)Time elapsed: 0.802 s
% 13.43/2.17 % (2954338)Peak memory usage: 19 MB
% 13.43/2.17 % (2954338)Instructions burned: 1181 (million)
% 13.43/2.17 % (2954344)Instruction limit reached!
% 13.43/2.17 % (2954344)------------------------------
% 13.43/2.17 % (2954344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.17 % (2954344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.17 % (2954344)CaDiCaL version: 2.1.3
% 13.43/2.17 % (2954344)Termination reason: Instruction limit
% 13.43/2.17 % (2954344)Termination phase: Saturation
% 13.43/2.17 % (2954344)Time elapsed: 0.648 s
% 13.43/2.17 % (2954344)Peak memory usage: 16 MB
% 13.43/2.17 % (2954344)Instructions burned: 879 (million)
% 13.43/2.17 % (2954368)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2759207362:fmbsr=1.7:i=920_2986 on theBenchmark for (2986ds/920Mi)
% 13.43/2.17 % (2954369)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=667156264:i=5131_2986 on theBenchmark for (2986ds/5131Mi)
% 13.43/2.17 % Detected minimum model sizes of [1]
% 13.43/2.17 % Detected maximum model sizes of [21]
% 13.43/2.17 % TRYING [8]
% 13.43/2.17 % TRYING [8]
% 13.43/2.17 % TRYING [13]
% 13.43/2.17 % TRYING [21]
% 13.43/2.17 % TRYING [9]
% 13.43/2.17 % TRYING [9]
% 13.43/2.17 % TRYING [14]
% 13.43/2.17 % (2954346) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2954187-2954346"...
% 13.43/2.17 % (2954346)...printing done.
% 13.43/2.17 % (2954346)Refutation found. Thanks to Tanya!
% 13.43/2.17 % SZS status Unsatisfiable for theBenchmark
% 13.43/2.17 % SZS output start Proof for theBenchmark
% See solution above
% 13.43/2.18 % (2954346)------------------------------
% 13.43/2.18 % (2954346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.43/2.18 % (2954346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.43/2.18 % (2954346)CaDiCaL version: 2.1.3
% 13.43/2.18 % (2954346)Termination reason: Refutation
% 13.43/2.18 % (2954346)Time elapsed: 1.126 s
% 13.43/2.18 % (2954346)Peak memory usage: 22 MB
% 13.43/2.18 % (2954346)Instructions burned: 1695 (million)
% 13.43/2.18 % (2954187)Success in time 1.933 s
% 13.43/2.18 % Vampire exiting
%------------------------------------------------------------------------------