%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : TOP050-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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 02:34:30 PM UTC 2026
% Result : Unsatisfiable 3.03s 1.05s
% Output : Refutation 3.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 77
% Number of leaves : 35
% Syntax : Number of formulae : 244 ( 244 unt; 0 def)
% Number of atoms : 244 ( 243 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 32 ( 32 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 34 ( 34 usr; 32 con; 0-31 aty)
% Number of variables : 18 ( 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : product(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',involutory_quandle) ).
fof(f2,axiom,
! [X0,X1] : product(product(X0,X1),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',involutory_quandle_01) ).
fof(f3,axiom,
! [X2,X0,X1] : product(product(X0,X1),X2) = product(product(X0,X2),product(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',involutory_quandle_02) ).
fof(f4,axiom,
product(a1,a31) = a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot) ).
fof(f5,axiom,
product(a2,a25) = a3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_03) ).
fof(f6,axiom,
product(a3,a29) = a4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_04) ).
fof(f7,axiom,
product(a4,a11) = a5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_05) ).
fof(f8,axiom,
product(a5,a15) = a6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_06) ).
fof(f9,axiom,
product(a7,a19) = a8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_07) ).
fof(f10,axiom,
product(a8,a5) = a9,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_08) ).
fof(f11,axiom,
product(a9,a17) = a10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_09) ).
fof(f12,axiom,
product(a10,a7) = a11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_10) ).
fof(f13,plain,
a11 = product(a10,a7),
inference(reorient_equations,[],[f12]) ).
fof(f14,axiom,
product(a11,a5) = a12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_11) ).
fof(f15,axiom,
product(a12,a19) = a13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_12) ).
fof(f16,axiom,
product(a13,a7) = a14,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_13) ).
fof(f17,axiom,
product(a14,a17) = a15,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_14) ).
fof(f18,plain,
a15 = product(a14,a17),
inference(reorient_equations,[],[f17]) ).
fof(f19,axiom,
product(a15,a5) = a16,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_15) ).
fof(f20,axiom,
product(a16,a19) = a17,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_16) ).
fof(f21,plain,
a17 = product(a16,a19),
inference(reorient_equations,[],[f20]) ).
fof(f22,axiom,
product(a17,a9) = a18,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_17) ).
fof(f23,axiom,
product(a18,a15) = a19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_18) ).
fof(f24,plain,
a19 = product(a18,a15),
inference(reorient_equations,[],[f23]) ).
fof(f25,axiom,
product(a19,a11) = a20,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_19) ).
fof(f26,axiom,
product(a20,a29) = a21,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_20) ).
fof(f27,axiom,
product(a21,a25) = a22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_21) ).
fof(f28,axiom,
product(a22,a31) = a23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_22) ).
fof(f29,axiom,
product(a23,a21) = a24,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_23) ).
fof(f30,axiom,
product(a24,a3) = a25,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_24) ).
fof(f31,plain,
a25 = product(a24,a3),
inference(reorient_equations,[],[f30]) ).
fof(f32,axiom,
product(a25,a23) = a26,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_25) ).
fof(f33,axiom,
product(a26,a1) = a27,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_26) ).
fof(f34,axiom,
product(a27,a21) = a28,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_27) ).
fof(f35,axiom,
product(a28,a3) = a29,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_28) ).
fof(f36,plain,
a29 = product(a28,a3),
inference(reorient_equations,[],[f35]) ).
fof(f37,axiom,
product(a29,a1) = a30,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_29) ).
fof(f38,axiom,
product(a30,a23) = a31,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_30) ).
fof(f39,plain,
a31 = product(a30,a23),
inference(reorient_equations,[],[f38]) ).
fof(f40,axiom,
product(a31,a3) = a32,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_31) ).
fof(f41,axiom,
product(a32,a21) = a1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knot_32) ).
fof(f42,plain,
a1 = product(a32,a21),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
tuple(a1,a30,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27) != tuple(a2,a31,a32,a3,a25,a26,a4,a29,a30,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f45,plain,
a1 = product(a2,a31),
inference(superposition,[],[f2,f4]) ).
fof(f46,plain,
a31 = product(a32,a3),
inference(superposition,[],[f2,f40]) ).
fof(f47,plain,
a2 = product(a3,a25),
inference(superposition,[],[f2,f5]) ).
fof(f48,plain,
a25 = product(a26,a23),
inference(superposition,[],[f2,f32]) ).
fof(f50,plain,
a29 = product(a30,a1),
inference(superposition,[],[f2,f37]) ).
fof(f52,plain,
a11 = product(a12,a5),
inference(superposition,[],[f2,f14]) ).
fof(f53,plain,
a5 = product(a6,a15),
inference(superposition,[],[f2,f8]) ).
fof(f54,plain,
a15 = product(a16,a5),
inference(superposition,[],[f2,f19]) ).
fof(f56,plain,
a19 = product(a20,a11),
inference(superposition,[],[f2,f25]) ).
fof(f60,plain,
a10 = product(a11,a7),
inference(superposition,[],[f2,f13]) ).
fof(f63,plain,
a14 = product(a15,a17),
inference(superposition,[],[f2,f18]) ).
fof(f65,plain,
a18 = product(a19,a15),
inference(superposition,[],[f2,f24]) ).
fof(f67,plain,
a21 = product(a22,a25),
inference(superposition,[],[f2,f27]) ).
fof(f71,plain,
a26 = product(a27,a1),
inference(superposition,[],[f2,f33]) ).
fof(f73,plain,
a28 = product(a29,a3),
inference(superposition,[],[f2,f36]) ).
fof(f74,plain,
a30 = product(a31,a23),
inference(superposition,[],[f2,f39]) ).
fof(f75,plain,
a32 = product(a1,a21),
inference(superposition,[],[f2,f42]) ).
fof(f78,plain,
! [X0,X1] : product(product(X0,X1),X0) = product(X0,product(X1,X0)),
inference(superposition,[],[f3,f1]) ).
fof(f85,plain,
! [X0] : product(product(a25,X0),a23) = product(a26,product(X0,a23)),
inference(superposition,[],[f3,f32]) ).
fof(f108,plain,
! [X0] : product(product(a26,X0),a1) = product(a27,product(X0,a1)),
inference(superposition,[],[f3,f33]) ).
fof(f109,plain,
! [X0] : product(product(a27,X0),a21) = product(a28,product(X0,a21)),
inference(superposition,[],[f3,f34]) ).
fof(f110,plain,
! [X0] : product(product(a28,X0),a3) = product(a29,product(X0,a3)),
inference(superposition,[],[f3,f36]) ).
fof(f119,plain,
! [X0] : product(product(X0,a2),a31) = product(product(X0,a31),a1),
inference(superposition,[],[f3,f45]) ).
fof(f140,plain,
! [X0] : product(product(X0,a22),a31) = product(product(X0,a31),a23),
inference(superposition,[],[f3,f28]) ).
fof(f141,plain,
! [X0] : product(product(X0,a23),a21) = product(product(X0,a21),a24),
inference(superposition,[],[f3,f29]) ).
fof(f142,plain,
! [X0] : product(product(X0,a24),a3) = product(product(X0,a3),a25),
inference(superposition,[],[f3,f31]) ).
fof(f153,plain,
! [X0] : product(product(X0,a3),a25) = product(product(X0,a25),a2),
inference(superposition,[],[f3,f47]) ).
fof(f1570,plain,
product(a28,product(a1,a21)) = product(a26,a21),
inference(superposition,[],[f109,f71]) ).
fof(f1586,plain,
product(a26,a21) = product(a28,a32),
inference(forward_demodulation,[],[f1570,f75]) ).
fof(f1611,plain,
product(a29,product(a32,a3)) = product(product(a26,a21),a3),
inference(superposition,[],[f110,f1586]) ).
fof(f1622,plain,
product(product(a26,a21),a3) = product(a29,a31),
inference(forward_demodulation,[],[f1611,f46]) ).
fof(f2880,plain,
product(a26,a21) = product(product(a25,a21),a24),
inference(superposition,[],[f141,f32]) ).
fof(f7453,plain,
! [X0] : product(product(X0,a24),a3) = product(product(X0,a25),a2),
inference(backward_demodulation,[],[f142,f153]) ).
fof(f7591,plain,
product(product(a26,a21),a3) = product(product(product(a25,a21),a25),a2),
inference(superposition,[],[f7453,f2880]) ).
fof(f7641,plain,
product(product(a26,a21),a3) = product(product(a25,product(a21,a25)),a2),
inference(forward_demodulation,[],[f7591,f78]) ).
fof(f7655,plain,
product(product(a26,a21),a3) = product(product(a25,a22),a2),
inference(forward_demodulation,[],[f7641,f27]) ).
fof(f7663,plain,
product(a29,a31) = product(product(a25,a22),a2),
inference(forward_demodulation,[],[f7655,f1622]) ).
fof(f7686,plain,
product(product(a29,a31),a31) = product(product(product(a25,a22),a31),a1),
inference(superposition,[],[f119,f7663]) ).
fof(f7698,plain,
product(product(a29,a31),a31) = product(product(product(a25,a31),a23),a1),
inference(forward_demodulation,[],[f7686,f140]) ).
fof(f7700,plain,
product(product(a29,a31),a31) = product(product(a26,product(a31,a23)),a1),
inference(forward_demodulation,[],[f7698,f85]) ).
fof(f7702,plain,
product(product(a29,a31),a31) = product(a27,product(product(a31,a23),a1)),
inference(forward_demodulation,[],[f7700,f108]) ).
fof(f7703,plain,
product(product(a29,a31),a31) = product(a27,product(a30,a1)),
inference(forward_demodulation,[],[f7702,f74]) ).
fof(f7704,plain,
product(product(a29,a31),a31) = product(a27,a29),
inference(forward_demodulation,[],[f7703,f50]) ).
fof(f7705,plain,
a29 = product(a27,a29),
inference(forward_demodulation,[],[f7704,f2]) ).
fof(f7751,plain,
a27 = product(a29,a29),
inference(superposition,[],[f2,f7705]) ).
fof(f7767,plain,
a29 = a27,
inference(forward_demodulation,[],[f7751,f1]) ).
fof(f7773,plain,
a28 = product(a29,a21),
inference(backward_demodulation,[],[f34,f7767]) ).
fof(f7774,plain,
tuple(a1,a30,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29) != tuple(a2,a31,a32,a3,a25,a26,a4,a29,a30,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a28),
inference(backward_demodulation,[],[f43,f7767]) ).
fof(f7775,plain,
a26 = product(a29,a1),
inference(backward_demodulation,[],[f71,f7767]) ).
fof(f7818,plain,
a26 = a30,
inference(backward_demodulation,[],[f37,f7775]) ).
fof(f7834,plain,
a31 = product(a26,a23),
inference(backward_demodulation,[],[f39,f7818]) ).
fof(f7858,plain,
tuple(a1,a26,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29) != tuple(a2,a31,a32,a3,a25,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a28),
inference(backward_demodulation,[],[f7774,f7818]) ).
fof(f7862,plain,
a31 = a25,
inference(backward_demodulation,[],[f48,f7834]) ).
fof(f7875,plain,
a3 = product(a2,a31),
inference(backward_demodulation,[],[f5,f7862]) ).
fof(f7876,plain,
a22 = product(a21,a31),
inference(backward_demodulation,[],[f27,f7862]) ).
fof(f7877,plain,
a31 = product(a24,a3),
inference(backward_demodulation,[],[f31,f7862]) ).
fof(f7878,plain,
a26 = product(a31,a23),
inference(backward_demodulation,[],[f32,f7862]) ).
fof(f7880,plain,
a21 = product(a22,a31),
inference(backward_demodulation,[],[f67,f7862]) ).
fof(f7955,plain,
a1 = a3,
inference(forward_demodulation,[],[f7875,f45]) ).
fof(f7968,plain,
a4 = product(a1,a29),
inference(backward_demodulation,[],[f6,f7955]) ).
fof(f7970,plain,
a32 = product(a31,a1),
inference(backward_demodulation,[],[f40,f7955]) ).
fof(f7973,plain,
a28 = product(a29,a1),
inference(backward_demodulation,[],[f73,f7955]) ).
fof(f8001,plain,
a26 = a28,
inference(forward_demodulation,[],[f7973,f7775]) ).
fof(f8005,plain,
a26 = product(a29,a21),
inference(backward_demodulation,[],[f7773,f8001]) ).
fof(f8018,plain,
a31 = product(a24,a1),
inference(forward_demodulation,[],[f7877,f7955]) ).
fof(f8056,plain,
a29 = product(a26,a21),
inference(superposition,[],[f2,f8005]) ).
fof(f8077,plain,
tuple(a1,a26,a31,a2,a24,a25,a3,a26,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29) != tuple(a2,a31,a32,a3,a25,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a26),
inference(forward_demodulation,[],[f7858,f8001]) ).
fof(f8078,plain,
tuple(a1,a26,a31,a2,a24,a31,a3,a26,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29) != tuple(a2,a31,a32,a3,a31,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a26),
inference(forward_demodulation,[],[f8077,f7862]) ).
fof(f8079,plain,
tuple(a1,a26,a31,a2,a24,a31,a1,a26,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29) != tuple(a2,a31,a32,a1,a31,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a26),
inference(forward_demodulation,[],[f8078,f7955]) ).
fof(f8083,plain,
a21 = a23,
inference(backward_demodulation,[],[f28,f7880]) ).
fof(f8102,plain,
a24 = product(a21,a21),
inference(backward_demodulation,[],[f29,f8083]) ).
fof(f8114,plain,
a31 = product(a26,a21),
inference(backward_demodulation,[],[f7834,f8083]) ).
fof(f8115,plain,
a26 = product(a31,a21),
inference(backward_demodulation,[],[f7878,f8083]) ).
fof(f8116,plain,
tuple(a1,a26,a31,a2,a24,a31,a1,a26,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a21,a26,a29) != tuple(a2,a31,a32,a1,a31,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a21,a24,a29,a26),
inference(backward_demodulation,[],[f8079,f8083]) ).
fof(f8121,plain,
a21 = a24,
inference(forward_demodulation,[],[f8102,f1]) ).
fof(f8125,plain,
a31 = product(a21,a1),
inference(backward_demodulation,[],[f8018,f8121]) ).
fof(f8148,plain,
a21 = product(a31,a1),
inference(superposition,[],[f2,f8125]) ).
fof(f8163,plain,
tuple(a1,a26,a31,a2,a21,a31,a1,a26,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a21,a26,a29) != tuple(a2,a31,a32,a1,a31,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a21,a21,a29,a26),
inference(forward_demodulation,[],[f8116,f8121]) ).
fof(f8188,plain,
a31 = a29,
inference(forward_demodulation,[],[f8056,f8114]) ).
fof(f8189,plain,
a21 = product(a20,a31),
inference(backward_demodulation,[],[f26,f8188]) ).
fof(f8199,plain,
product(a1,a31) = a4,
inference(backward_demodulation,[],[f7968,f8188]) ).
fof(f8202,plain,
tuple(a1,a26,a31,a2,a21,a31,a1,a26,a31,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a21,a26,a31) != tuple(a2,a31,a32,a1,a31,a26,a4,a31,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a21,a21,a31,a26),
inference(backward_demodulation,[],[f8163,f8188]) ).
fof(f8203,plain,
a2 = a4,
inference(forward_demodulation,[],[f8199,f4]) ).
fof(f8205,plain,
a5 = product(a2,a11),
inference(backward_demodulation,[],[f7,f8203]) ).
fof(f8263,plain,
tuple(a1,a26,a31,a2,a21,a31,a1,a26,a31,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a21,a26,a31) != tuple(a2,a31,a32,a1,a31,a26,a2,a31,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a21,a21,a31,a26),
inference(forward_demodulation,[],[f8202,f8203]) ).
fof(f8267,plain,
a21 = a32,
inference(backward_demodulation,[],[f7970,f8148]) ).
fof(f8280,plain,
a1 = product(a21,a21),
inference(backward_demodulation,[],[f42,f8267]) ).
fof(f8286,plain,
tuple(a1,a26,a31,a2,a21,a31,a1,a26,a31,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a21,a26,a31) != tuple(a2,a31,a21,a1,a31,a26,a2,a31,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a21,a21,a31,a26),
inference(backward_demodulation,[],[f8263,f8267]) ).
fof(f8290,plain,
a1 = a21,
inference(forward_demodulation,[],[f8280,f1]) ).
fof(f8292,plain,
product(a1,a31) = a22,
inference(backward_demodulation,[],[f7876,f8290]) ).
fof(f8296,plain,
a26 = product(a31,a1),
inference(backward_demodulation,[],[f8115,f8290]) ).
fof(f8298,plain,
a31 = product(a1,a1),
inference(backward_demodulation,[],[f8125,f8290]) ).
fof(f8300,plain,
a1 = product(a20,a31),
inference(backward_demodulation,[],[f8189,f8290]) ).
fof(f8302,plain,
a1 = a31,
inference(forward_demodulation,[],[f8298,f1]) ).
fof(f8303,plain,
a2 = a22,
inference(forward_demodulation,[],[f8292,f4]) ).
fof(f8304,plain,
a2 = product(a1,a1),
inference(backward_demodulation,[],[f4,f8302]) ).
fof(f8318,plain,
a1 = a2,
inference(forward_demodulation,[],[f8304,f1]) ).
fof(f8320,plain,
a5 = product(a1,a11),
inference(backward_demodulation,[],[f8205,f8318]) ).
fof(f8321,plain,
a1 = a22,
inference(backward_demodulation,[],[f8303,f8318]) ).
fof(f8322,plain,
a26 = product(a1,a1),
inference(forward_demodulation,[],[f8296,f8302]) ).
fof(f8323,plain,
a1 = a26,
inference(forward_demodulation,[],[f8322,f1]) ).
fof(f8326,plain,
a1 = product(a20,a1),
inference(forward_demodulation,[],[f8300,f8302]) ).
fof(f8338,plain,
a20 = product(a1,a1),
inference(superposition,[],[f2,f8326]) ).
fof(f8354,plain,
a1 = a20,
inference(forward_demodulation,[],[f8338,f1]) ).
fof(f8357,plain,
a1 = product(a19,a11),
inference(backward_demodulation,[],[f25,f8354]) ).
fof(f8358,plain,
a19 = product(a1,a11),
inference(backward_demodulation,[],[f56,f8354]) ).
fof(f8369,plain,
a5 = a19,
inference(forward_demodulation,[],[f8358,f8320]) ).
fof(f8370,plain,
a8 = product(a7,a5),
inference(backward_demodulation,[],[f9,f8369]) ).
fof(f8371,plain,
a13 = product(a12,a5),
inference(backward_demodulation,[],[f15,f8369]) ).
fof(f8372,plain,
a17 = product(a16,a5),
inference(backward_demodulation,[],[f21,f8369]) ).
fof(f8377,plain,
product(a5,a15) = a18,
inference(backward_demodulation,[],[f65,f8369]) ).
fof(f8419,plain,
a6 = a18,
inference(forward_demodulation,[],[f8377,f8]) ).
fof(f8420,plain,
a15 = a17,
inference(forward_demodulation,[],[f8372,f54]) ).
fof(f8421,plain,
a11 = a13,
inference(forward_demodulation,[],[f8371,f52]) ).
fof(f8429,plain,
a10 = product(a9,a15),
inference(backward_demodulation,[],[f11,f8420]) ).
fof(f8431,plain,
a18 = product(a15,a9),
inference(backward_demodulation,[],[f22,f8420]) ).
fof(f8434,plain,
a14 = product(a15,a15),
inference(backward_demodulation,[],[f63,f8420]) ).
fof(f8456,plain,
a15 = a14,
inference(forward_demodulation,[],[f8434,f1]) ).
fof(f8459,plain,
a14 = product(a11,a7),
inference(backward_demodulation,[],[f16,f8421]) ).
fof(f8466,plain,
a10 = a14,
inference(forward_demodulation,[],[f8459,f60]) ).
fof(f8477,plain,
a15 = a10,
inference(backward_demodulation,[],[f8466,f8456]) ).
fof(f8478,plain,
a11 = product(a15,a7),
inference(backward_demodulation,[],[f13,f8477]) ).
fof(f8486,plain,
a1 = product(a5,a11),
inference(forward_demodulation,[],[f8357,f8369]) ).
fof(f8498,plain,
a15 = product(a9,a15),
inference(forward_demodulation,[],[f8429,f8477]) ).
fof(f8500,plain,
a6 = product(a15,a9),
inference(forward_demodulation,[],[f8431,f8419]) ).
fof(f8528,plain,
a9 = product(a15,a15),
inference(superposition,[],[f2,f8498]) ).
fof(f8544,plain,
a15 = a9,
inference(forward_demodulation,[],[f8528,f1]) ).
fof(f8566,plain,
a15 = product(a8,a5),
inference(backward_demodulation,[],[f10,f8544]) ).
fof(f8574,plain,
a6 = product(a15,a15),
inference(backward_demodulation,[],[f8500,f8544]) ).
fof(f8575,plain,
a15 = a6,
inference(forward_demodulation,[],[f8574,f1]) ).
fof(f8580,plain,
a5 = product(a15,a15),
inference(backward_demodulation,[],[f53,f8575]) ).
fof(f8586,plain,
a15 = a18,
inference(backward_demodulation,[],[f8419,f8575]) ).
fof(f8591,plain,
a5 = a15,
inference(forward_demodulation,[],[f8580,f1]) ).
fof(f8593,plain,
a16 = product(a5,a5),
inference(backward_demodulation,[],[f19,f8591]) ).
fof(f8599,plain,
a5 = a17,
inference(backward_demodulation,[],[f8420,f8591]) ).
fof(f8600,plain,
a5 = a14,
inference(backward_demodulation,[],[f8456,f8591]) ).
fof(f8601,plain,
a5 = a10,
inference(backward_demodulation,[],[f8477,f8591]) ).
fof(f8602,plain,
a11 = product(a5,a7),
inference(backward_demodulation,[],[f8478,f8591]) ).
fof(f8603,plain,
a5 = a9,
inference(backward_demodulation,[],[f8544,f8591]) ).
fof(f8604,plain,
a5 = a6,
inference(backward_demodulation,[],[f8575,f8591]) ).
fof(f8605,plain,
a5 = a18,
inference(backward_demodulation,[],[f8586,f8591]) ).
fof(f8609,plain,
a5 = a16,
inference(forward_demodulation,[],[f8593,f1]) ).
fof(f8610,plain,
a5 = product(a8,a5),
inference(forward_demodulation,[],[f8566,f8591]) ).
fof(f8624,plain,
a8 = product(a5,a5),
inference(superposition,[],[f2,f8610]) ).
fof(f8640,plain,
a5 = a8,
inference(forward_demodulation,[],[f8624,f1]) ).
fof(f8643,plain,
a5 = product(a7,a5),
inference(backward_demodulation,[],[f8370,f8640]) ).
fof(f8645,plain,
a7 = product(a5,a5),
inference(superposition,[],[f2,f8643]) ).
fof(f8662,plain,
a5 = a7,
inference(forward_demodulation,[],[f8645,f1]) ).
fof(f8666,plain,
a11 = product(a5,a5),
inference(backward_demodulation,[],[f8602,f8662]) ).
fof(f8667,plain,
a11 = a5,
inference(forward_demodulation,[],[f8666,f1]) ).
fof(f8668,plain,
a12 = product(a11,a11),
inference(backward_demodulation,[],[f14,f8667]) ).
fof(f8672,plain,
a11 = a19,
inference(backward_demodulation,[],[f8369,f8667]) ).
fof(f8673,plain,
a1 = product(a11,a11),
inference(backward_demodulation,[],[f8486,f8667]) ).
fof(f8674,plain,
a11 = a15,
inference(backward_demodulation,[],[f8591,f8667]) ).
fof(f8675,plain,
a11 = a17,
inference(backward_demodulation,[],[f8599,f8667]) ).
fof(f8676,plain,
a11 = a14,
inference(backward_demodulation,[],[f8600,f8667]) ).
fof(f8677,plain,
a11 = a10,
inference(backward_demodulation,[],[f8601,f8667]) ).
fof(f8678,plain,
a11 = a9,
inference(backward_demodulation,[],[f8603,f8667]) ).
fof(f8679,plain,
a11 = a6,
inference(backward_demodulation,[],[f8604,f8667]) ).
fof(f8680,plain,
a11 = a18,
inference(backward_demodulation,[],[f8605,f8667]) ).
fof(f8681,plain,
a11 = a16,
inference(backward_demodulation,[],[f8609,f8667]) ).
fof(f8682,plain,
a11 = a8,
inference(backward_demodulation,[],[f8640,f8667]) ).
fof(f8683,plain,
a11 = a7,
inference(backward_demodulation,[],[f8662,f8667]) ).
fof(f8684,plain,
a1 = a11,
inference(forward_demodulation,[],[f8673,f1]) ).
fof(f8686,plain,
a11 = a12,
inference(forward_demodulation,[],[f8668,f1]) ).
fof(f8687,plain,
a1 = a13,
inference(backward_demodulation,[],[f8421,f8684]) ).
fof(f8688,plain,
a1 = a5,
inference(backward_demodulation,[],[f8667,f8684]) ).
fof(f8689,plain,
a1 = a17,
inference(backward_demodulation,[],[f8675,f8684]) ).
fof(f8690,plain,
a1 = a10,
inference(backward_demodulation,[],[f8677,f8684]) ).
fof(f8691,plain,
a1 = a6,
inference(backward_demodulation,[],[f8679,f8684]) ).
fof(f8692,plain,
a1 = a16,
inference(backward_demodulation,[],[f8681,f8684]) ).
fof(f8693,plain,
a1 = a12,
inference(forward_demodulation,[],[f8686,f8684]) ).
fof(f8694,plain,
a1 = a19,
inference(forward_demodulation,[],[f8672,f8684]) ).
fof(f8696,plain,
a1 = a15,
inference(forward_demodulation,[],[f8674,f8684]) ).
fof(f8697,plain,
a1 = a14,
inference(forward_demodulation,[],[f8676,f8684]) ).
fof(f8698,plain,
a1 = a9,
inference(forward_demodulation,[],[f8678,f8684]) ).
fof(f8699,plain,
a1 = a18,
inference(forward_demodulation,[],[f8680,f8684]) ).
fof(f8700,plain,
tuple(a1,a1,a31,a2,a21,a31,a1,a1,a31,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a21,a1,a31) != tuple(a2,a31,a21,a1,a31,a1,a2,a31,a1,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a21,a21,a31,a1),
inference(forward_demodulation,[],[f8286,f8323]) ).
fof(f8701,plain,
tuple(a1,a1,a1,a2,a21,a1,a1,a1,a1,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a21,a1,a1) != tuple(a2,a1,a21,a1,a1,a1,a2,a1,a1,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a21,a21,a1,a1),
inference(forward_demodulation,[],[f8700,f8302]) ).
fof(f8702,plain,
tuple(a1,a1,a1,a2,a1,a1,a1,a1,a1,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a1,a22,a1,a1,a1) != tuple(a2,a1,a1,a1,a1,a1,a2,a1,a1,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a1,a22,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8701,f8290]) ).
fof(f8703,plain,
tuple(a1,a1,a1,a2,a1,a1,a1,a1,a1,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a1,a1,a1,a1,a1) != tuple(a2,a1,a1,a1,a1,a1,a2,a1,a1,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8702,f8321]) ).
fof(f8704,plain,
tuple(a1,a1,a1,a2,a1,a1,a1,a1,a1,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a1,a20,a1,a1,a1,a1,a1) != tuple(a2,a1,a1,a1,a1,a1,a2,a1,a1,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a1,a14,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8703,f8687]) ).
fof(f8705,plain,
tuple(a1,a1,a1,a2,a1,a1,a1,a1,a1,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a1,a12,a1,a20,a1,a1,a1,a1,a1) != tuple(a2,a1,a1,a1,a1,a1,a2,a1,a1,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a1,a18,a1,a14,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8704,f8689]) ).
fof(f8706,plain,
tuple(a1,a1,a1,a2,a1,a1,a1,a1,a1,a2,a1,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a1,a12,a1,a20,a1,a1,a1,a1,a1) != tuple(a2,a1,a1,a1,a1,a1,a2,a1,a1,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a1,a1,a18,a1,a14,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8705,f8690]) ).
fof(f8707,plain,
tuple(a1,a1,a1,a2,a1,a1,a1,a1,a1,a2,a1,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a1,a12,a1,a1,a1,a1,a1,a1,a1) != tuple(a2,a1,a1,a1,a1,a1,a2,a1,a1,a5,a11,a12,a6,a15,a16,a7,a8,a19,a1,a9,a1,a1,a18,a1,a14,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8706,f8354]) ).
fof(f8708,plain,
tuple(a1,a1,a1,a2,a1,a1,a1,a1,a1,a2,a1,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a1,a1,a12,a1,a1,a1,a1,a1,a1,a1) != tuple(a2,a1,a1,a1,a1,a1,a2,a1,a1,a5,a11,a12,a6,a15,a1,a7,a8,a19,a1,a9,a1,a1,a18,a1,a14,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8707,f8692]) ).
fof(f8709,plain,
tuple(a1,a1,a1,a2,a1,a1,a1,a1,a1,a2,a1,a11,a5,a14,a15,a1,a7,a18,a19,a8,a9,a1,a1,a12,a1,a1,a1,a1,a1,a1,a1) != tuple(a2,a1,a1,a1,a1,a1,a2,a1,a1,a5,a11,a12,a1,a15,a1,a7,a8,a19,a1,a9,a1,a1,a18,a1,a14,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8708,f8691]) ).
fof(f8710,plain,
tuple(a1,a1,a1,a2,a1,a1,a1,a1,a1,a2,a1,a11,a5,a14,a15,a1,a7,a18,a19,a8,a9,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1) != tuple(a2,a1,a1,a1,a1,a1,a2,a1,a1,a5,a11,a1,a1,a15,a1,a7,a8,a19,a1,a9,a1,a1,a18,a1,a14,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8709,f8693]) ).
fof(f8711,plain,
tuple(a1,a1,a1,a2,a1,a1,a1,a1,a1,a2,a1,a1,a5,a14,a15,a1,a7,a18,a19,a8,a9,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1) != tuple(a2,a1,a1,a1,a1,a1,a2,a1,a1,a5,a1,a1,a1,a15,a1,a7,a8,a19,a1,a9,a1,a1,a18,a1,a14,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8710,f8684]) ).
fof(f8712,plain,
tuple(a1,a1,a1,a2,a1,a1,a1,a1,a1,a2,a1,a1,a1,a14,a15,a1,a7,a18,a19,a8,a9,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1) != tuple(a2,a1,a1,a1,a1,a1,a2,a1,a1,a1,a1,a1,a1,a15,a1,a7,a8,a19,a1,a9,a1,a1,a18,a1,a14,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8711,f8688]) ).
fof(f8713,plain,
tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a14,a15,a1,a7,a18,a19,a8,a9,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1) != tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a15,a1,a7,a8,a19,a1,a9,a1,a1,a18,a1,a14,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8712,f8318]) ).
fof(f8714,plain,
a1 = a8,
inference(forward_demodulation,[],[f8682,f8684]) ).
fof(f8715,plain,
a1 = a7,
inference(forward_demodulation,[],[f8683,f8684]) ).
fof(f8716,plain,
tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a14,a15,a1,a7,a18,a1,a8,a9,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1) != tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a15,a1,a7,a8,a1,a1,a9,a1,a1,a18,a1,a14,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8713,f8694]) ).
fof(f8717,plain,
tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a14,a1,a1,a7,a18,a1,a8,a9,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1) != tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a7,a8,a1,a1,a9,a1,a1,a18,a1,a14,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8716,f8696]) ).
fof(f8718,plain,
tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a7,a18,a1,a8,a9,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1) != tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a7,a8,a1,a1,a9,a1,a1,a18,a1,a1,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8717,f8697]) ).
fof(f8719,plain,
tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a7,a1,a1,a8,a9,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1) != tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a7,a8,a1,a1,a9,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8718,f8699]) ).
fof(f8720,plain,
tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a7,a1,a1,a8,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1) != tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a7,a8,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8719,f8698]) ).
fof(f8721,plain,
tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a7,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1) != tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a7,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8720,f8714]) ).
fof(f8729,plain,
tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1) != tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[],[f8721,f8715]) ).
fof(f8730,plain,
$false,
inference(trivial_inequality_removal,[],[f8729]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : TOP050-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.26/0.33 % Computer : n007.cluster.edu
% 0.26/0.33 % Model : x86_64 x86_64
% 0.26/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.26/0.33 % Memory : 8046.5625MB
% 0.26/0.33 % OS : Linux 6.8.0-71-generic
% 0.26/0.33 % CPULimit : 300
% 0.26/0.33 % WCLimit : 300
% 0.26/0.33 % DateTime : Mon Sep 28 19:05:26 UTC 2026
% 0.26/0.33 % CPUTime :
% 0.26/0.33 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.26/0.39 Running first-order model finding
% 0.26/0.39 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
% 3.03/1.05 % (2718352)Will run a generic schedule for satisfiability detection.
% 3.03/1.05 % (2718362)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2053636973:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.03/1.05 % (2718358)% WARNING: option uhcvi not known.
% 3.03/1.05 % (2718359)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1951494200:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.03/1.05 % (2718358)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=535668778:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.03/1.05 % (2718360)dis+10_1_sil=32000:sp=arity:random_seed=2692822459:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.03/1.05 % (2718357)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=356650457_2999 on theBenchmark for (2999ds/0Mi)
% 3.03/1.05 % (2718361)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2584473074:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.03/1.05 % (2718363)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3601688302:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.03/1.05 % TRYING [1]
% 3.03/1.05 % (2718357)Cannot represent all propositional literals internally
% 3.03/1.05 % (2718357)Refutation not found, incomplete strategy
% 3.03/1.05 % (2718357)------------------------------
% 3.03/1.05 % (2718357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.03/1.05 % (2718357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.03/1.05 % (2718357)CaDiCaL version: 2.1.3
% 3.03/1.05 % (2718357)Termination reason: Refutation not found, incomplete strategy
% 3.03/1.05 % (2718357)Time elapsed: 0.007 s
% 3.03/1.05 % (2718357)Peak memory usage: 11 MB
% 3.03/1.05 % (2718357)Instructions burned: 7 (million)
% 3.03/1.05 % (2718357)------------------------------
% 3.03/1.05 % (2718357)------------------------------
% 3.03/1.05 % (2718362)Instruction limit reached!
% 3.03/1.05 % (2718362)------------------------------
% 3.03/1.05 % (2718362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.03/1.05 % (2718362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.03/1.05 % (2718362)CaDiCaL version: 2.1.3
% 3.03/1.05 % (2718362)Termination reason: Instruction limit
% 3.03/1.05 % (2718362)Termination phase: Saturation
% 3.03/1.05 % (2718362)Time elapsed: 0.049 s
% 3.03/1.05 % (2718362)Peak memory usage: 12 MB
% 3.03/1.05 % (2718362)Instructions burned: 133 (million)
% 3.03/1.05 % (2718371)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=877592078:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.03/1.05 % TRYING [1]
% 3.03/1.05 % (2718371)Cannot represent all propositional literals internally
% 3.03/1.05 % (2718371)Refutation not found, incomplete strategy
% 3.03/1.05 % (2718371)------------------------------
% 3.03/1.05 % (2718371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.03/1.05 % (2718371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.03/1.05 % (2718371)CaDiCaL version: 2.1.3
% 3.03/1.05 % (2718371)Termination reason: Refutation not found, incomplete strategy
% 3.03/1.05 % (2718371)Time elapsed: 0.007 s
% 3.03/1.05 % (2718371)Peak memory usage: 11 MB
% 3.03/1.05 % (2718371)Instructions burned: 7 (million)
% 3.03/1.05 % (2718371)------------------------------
% 3.03/1.05 % (2718371)------------------------------
% 3.03/1.05 % (2718372)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1258461013:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.03/1.05 % (2718360)Instruction limit reached!
% 3.03/1.05 % (2718360)------------------------------
% 3.03/1.05 % (2718360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.03/1.05 % (2718360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.03/1.05 % (2718360)CaDiCaL version: 2.1.3
% 3.03/1.05 % (2718360)Termination reason: Instruction limit
% 3.03/1.05 % (2718360)Termination phase: Saturation
% 3.03/1.05 % (2718360)Time elapsed: 0.096 s
% 3.03/1.05 % (2718360)Peak memory usage: 12 MB
% 3.03/1.05 % (2718360)Instructions burned: 103 (million)
% 3.03/1.05 % (2718361)Instruction limit reached!
% 3.03/1.05 % (2718361)------------------------------
% 3.03/1.05 % (2718361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.03/1.05 % (2718361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.03/1.05 % (2718361)CaDiCaL version: 2.1.3
% 3.03/1.05 % (2718361)Termination reason: Instruction limit
% 3.03/1.05 % (2718361)Termination phase: Saturation
% 3.03/1.05 % (2718361)Time elapsed: 0.113 s
% 3.03/1.05 % (2718361)Peak memory usage: 12 MB
% 3.03/1.05 % (2718361)Instructions burned: 116 (million)
% 3.03/1.05 % (2718374)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=2878983372:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 3.03/1.05 % (2718376)ott-21_1_sil=16000:fs=off:random_seed=3791580799:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 3.03/1.05 % (2718372)Instruction limit reached!
% 3.03/1.05 % (2718372)------------------------------
% 3.03/1.05 % (2718372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.03/1.05 % (2718372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.03/1.05 % (2718372)CaDiCaL version: 2.1.3
% 3.03/1.05 % (2718372)Termination reason: Instruction limit
% 3.03/1.05 % (2718372)Termination phase: Saturation
% 3.03/1.05 % (2718372)Time elapsed: 0.078 s
% 3.03/1.05 % (2718372)Peak memory usage: 13 MB
% 3.03/1.05 % (2718372)Instructions burned: 131 (million)
% 3.03/1.05 % (2718363)Instruction limit reached!
% 3.03/1.05 % (2718363)------------------------------
% 3.03/1.05 % (2718363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.03/1.05 % (2718363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.03/1.05 % (2718363)CaDiCaL version: 2.1.3
% 3.03/1.05 % (2718363)Termination reason: Instruction limit
% 3.03/1.05 % (2718363)Termination phase: Saturation
% 3.03/1.05 % (2718363)Time elapsed: 0.164 s
% 3.03/1.05 % (2718363)Peak memory usage: 13 MB
% 3.03/1.05 % (2718363)Instructions burned: 159 (million)
% 3.03/1.05 % (2718378)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=804075769:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 3.03/1.05 % (2718380)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1192531836:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 3.03/1.05 % TRYING [1]
% 3.03/1.05 % (2718380)Cannot represent all propositional literals internally
% 3.03/1.05 % (2718380)Refutation not found, incomplete strategy
% 3.03/1.05 % (2718380)------------------------------
% 3.03/1.05 % (2718380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.03/1.05 % (2718380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.03/1.05 % (2718380)CaDiCaL version: 2.1.3
% 3.03/1.05 % (2718380)Termination reason: Refutation not found, incomplete strategy
% 3.03/1.05 % (2718380)Time elapsed: 0.004 s
% 3.03/1.05 % (2718380)Peak memory usage: 10 MB
% 3.03/1.05 % (2718380)Instructions burned: 7 (million)
% 3.03/1.05 % (2718380)------------------------------
% 3.03/1.05 % (2718380)------------------------------
% 3.03/1.05 % (2718381)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3098577311:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 3.03/1.05 % (2718384)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2085027645:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 3.03/1.05 % (2718384)Cannot represent all propositional literals internally
% 3.03/1.05 % (2718384)Refutation not found, incomplete strategy
% 3.03/1.05 % (2718384)------------------------------
% 3.03/1.05 % (2718384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.03/1.05 % (2718384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.03/1.05 % (2718384)CaDiCaL version: 2.1.3
% 3.03/1.05 % (2718384)Termination reason: Refutation not found, incomplete strategy
% 3.03/1.05 % (2718384)Time elapsed: 0.003 s
% 3.03/1.05 % (2718384)Peak memory usage: 10 MB
% 3.03/1.05 % (2718384)Instructions burned: 6 (million)
% 3.03/1.05 % (2718384)------------------------------
% 3.03/1.05 % (2718384)------------------------------
% 3.03/1.05 % (2718387)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=2318593209:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 3.03/1.05 % (2718376)Instruction limit reached!
% 3.03/1.05 % (2718376)------------------------------
% 3.03/1.05 % (2718376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.03/1.05 % (2718376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.03/1.05 % (2718376)CaDiCaL version: 2.1.3
% 3.03/1.05 % (2718376)Termination reason: Instruction limit
% 3.03/1.05 % (2718376)Termination phase: Saturation
% 3.03/1.05 % (2718376)Time elapsed: 0.162 s
% 3.03/1.05 % (2718376)Peak memory usage: 13 MB
% 3.03/1.05 % (2718376)Instructions burned: 180 (million)
% 3.03/1.05 % (2718389)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=827928711:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 3.03/1.05 % (2718378) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2718352-2718378"...
% 3.03/1.05 % (2718378)...printing done.
% 3.03/1.05 % (2718378)Refutation found. Thanks to Tanya!
% 3.03/1.05 % SZS status Unsatisfiable for theBenchmark
% 3.03/1.05 % SZS output start Proof for theBenchmark
% See solution above
% 3.03/1.06 % (2718378)------------------------------
% 3.03/1.06 % (2718378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.03/1.06 % (2718378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.03/1.06 % (2718378)CaDiCaL version: 2.1.3
% 3.03/1.06 % (2718378)Termination reason: Refutation
% 3.03/1.06 % (2718378)Time elapsed: 0.408 s
% 3.03/1.06 % (2718378)Peak memory usage: 15 MB
% 3.03/1.06 % (2718378)Instructions burned: 428 (million)
% 3.03/1.06 % (2718352)Success in time 0.648 s
% 3.03/1.06 % Vampire exiting
%------------------------------------------------------------------------------