%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ064-2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:31:26 PM UTC 2026
% Result : Unsatisfiable 16.93s 3.39s
% Output : Refutation 17.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 20
% Syntax : Number of formulae : 120 ( 114 unt; 0 def)
% Number of atoms : 135 ( 114 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 34 ( 19 ~; 15 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 7 con; 0-4 aty)
% Number of variables : 206 ( 206 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
c_in(v_a,v_A,tc_set(t_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f2,negated_conjecture,
c_inter(v_a,v_t,t_a) = c_emptyset,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f3,negated_conjecture,
c_in(v_u,c_Mutil_Otiling(v_A,t_a),tc_set(t_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f4,negated_conjecture,
c_inter(c_union(v_a,v_t,t_a),v_u,t_a) = c_emptyset,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f5,plain,
c_emptyset = c_inter(c_union(v_a,v_t,t_a),v_u,t_a),
inference(reorient_equations,[],[f4]) ).
fof(f6,negated_conjecture,
~ c_in(c_union(c_union(v_a,v_t,t_a),v_u,t_a),c_Mutil_Otiling(v_A,t_a),tc_set(t_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f7,negated_conjecture,
( c_in(c_union(v_t,v_u,t_a),c_Mutil_Otiling(v_A,t_a),tc_set(t_a))
| c_inter(v_t,v_u,t_a) != c_emptyset
| ~ c_in(v_u,c_Mutil_Otiling(v_A,t_a),tc_set(t_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f8,plain,
( c_in(c_union(v_t,v_u,t_a),c_Mutil_Otiling(v_A,t_a),tc_set(t_a))
| c_emptyset != c_inter(v_t,v_u,t_a)
| ~ c_in(v_u,c_Mutil_Otiling(v_A,t_a),tc_set(t_a)) ),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(X0,X1,tc_set(X2))
| ~ c_in(X3,c_Mutil_Otiling(X1,X2),tc_set(X2))
| c_inter(X0,X3,X2) != c_emptyset
| c_in(c_union(X0,X3,X2),c_Mutil_Otiling(X1,X2),tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Mutil_Otiling_OUn_0) ).
fof(f10,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,X1,tc_set(X2))
| ~ c_in(X3,c_Mutil_Otiling(X1,X2),tc_set(X2))
| c_emptyset != c_inter(X0,X3,X2)
| c_in(c_union(X0,X3,X2),c_Mutil_Otiling(X1,X2),tc_set(X2)) ),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X2,X0,X1] : c_Relation_OImage(c_Relation_Odiag(X0,X1),X2,X1,X1) = c_inter(X0,X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Relation_OImage__diag_0) ).
fof(f12,axiom,
! [X2,X0,X1] : c_uminus(c_minus(X0,X1,tc_set(X2)),tc_set(X2)) = c_union(c_uminus(X0,tc_set(X2)),X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OCompl__Diff__eq_0) ).
fof(f13,axiom,
! [X0] : c_uminus(c_UNIV,tc_set(X0)) = c_emptyset,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OCompl__UNIV__eq_0) ).
fof(f14,plain,
! [X0] : c_emptyset = c_uminus(c_UNIV,tc_set(X0)),
inference(reorient_equations,[],[f13]) ).
fof(f15,axiom,
! [X2,X0,X1] : c_minus(X0,c_uminus(X1,tc_set(X2)),tc_set(X2)) = c_inter(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_ODiff__Compl_0) ).
fof(f16,axiom,
! [X0,X1] : c_inter(c_UNIV,X0,X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OInt__UNIV__left_0) ).
fof(f18,axiom,
! [X2,X0,X1] : c_union(c_minus(X0,X1,tc_set(X2)),X1,X2) = c_union(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__Diff__cancel2_0) ).
fof(f19,axiom,
! [X2,X0,X1] : c_union(X0,c_minus(X1,X0,tc_set(X2)),X2) = c_union(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__Diff__cancel_0) ).
fof(f20,plain,
! [X2,X0,X1] : c_union(X0,X1,X2) = c_union(X0,c_minus(X1,X0,tc_set(X2)),X2),
inference(reorient_equations,[],[f19]) ).
fof(f21,axiom,
! [X0,X1] : c_union(c_UNIV,X0,X1) = c_UNIV,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__UNIV__left_0) ).
fof(f22,plain,
! [X0,X1] : c_UNIV = c_union(c_UNIV,X0,X1),
inference(reorient_equations,[],[f21]) ).
fof(f23,axiom,
! [X0,X1] : c_union(X0,X0,X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__absorb_0) ).
fof(f24,axiom,
! [X2,X3,X0,X1] : c_union(c_union(X0,X1,X2),X3,X2) = c_union(X0,c_union(X1,X3,X2),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__assoc_0) ).
fof(f25,axiom,
! [X0,X1] : c_union(c_emptyset,X0,X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__empty__left_0) ).
fof(f26,axiom,
! [X0,X1] : c_union(X0,c_emptyset,X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__empty__right_0) ).
fof(f30,axiom,
! [X0,X1] : c_uminus(c_uminus(X0,tc_set(X1)),tc_set(X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_Odouble__complement_0) ).
fof(f37,plain,
c_emptyset = c_Relation_OImage(c_Relation_Odiag(v_a,t_a),v_t,t_a,t_a),
inference(definition_unfolding,[],[f2,f11]) ).
fof(f38,plain,
c_emptyset = c_Relation_OImage(c_Relation_Odiag(c_union(v_a,v_t,t_a),t_a),v_u,t_a,t_a),
inference(definition_unfolding,[],[f5,f11]) ).
fof(f39,plain,
( c_emptyset != c_Relation_OImage(c_Relation_Odiag(v_t,t_a),v_u,t_a,t_a)
| c_in(c_union(v_t,v_u,t_a),c_Mutil_Otiling(v_A,t_a),tc_set(t_a))
| ~ c_in(v_u,c_Mutil_Otiling(v_A,t_a),tc_set(t_a)) ),
inference(definition_unfolding,[],[f8,f11]) ).
fof(f40,plain,
! [X2,X3,X0,X1] :
( c_emptyset != c_Relation_OImage(c_Relation_Odiag(X0,X2),X3,X2,X2)
| ~ c_in(X3,c_Mutil_Otiling(X1,X2),tc_set(X2))
| ~ c_in(X0,X1,tc_set(X2))
| c_in(c_union(X0,X3,X2),c_Mutil_Otiling(X1,X2),tc_set(X2)) ),
inference(definition_unfolding,[],[f10,f11]) ).
fof(f41,plain,
! [X2,X0,X1] : c_minus(X0,c_uminus(X1,tc_set(X2)),tc_set(X2)) = c_Relation_OImage(c_Relation_Odiag(X0,X2),X1,X2,X2),
inference(definition_unfolding,[],[f15,f11]) ).
fof(f42,plain,
! [X0,X1] : c_Relation_OImage(c_Relation_Odiag(c_UNIV,X1),X0,X1,X1) = X0,
inference(definition_unfolding,[],[f16,f11]) ).
fof(f44,plain,
~ c_in(c_union(v_a,c_union(v_t,v_u,t_a),t_a),c_Mutil_Otiling(v_A,t_a),tc_set(t_a)),
inference(forward_demodulation,[],[f6,f24]) ).
fof(f58,plain,
! [X2,X0,X1] : c_union(X0,X2,X1) = c_union(X0,c_union(X0,X2,X1),X1),
inference(superposition,[],[f24,f23]) ).
fof(f72,plain,
! [X2,X0,X1] : c_union(c_uminus(X0,tc_set(X1)),c_uminus(X2,tc_set(X1)),X1) = c_uminus(c_Relation_OImage(c_Relation_Odiag(X0,X1),X2,X1,X1),tc_set(X1)),
inference(superposition,[],[f12,f41]) ).
fof(f73,plain,
! [X2,X3,X0,X1] : c_Relation_OImage(c_Relation_Odiag(X3,X1),c_minus(X0,X2,tc_set(X1)),X1,X1) = c_minus(X3,c_union(c_uminus(X0,tc_set(X1)),X2,X1),tc_set(X1)),
inference(superposition,[],[f41,f12]) ).
fof(f109,plain,
! [X2,X0,X1] : c_union(c_uminus(X2,tc_set(X1)),X0,X1) = c_union(c_uminus(X2,tc_set(X1)),c_Relation_OImage(c_Relation_Odiag(X0,X1),X2,X1,X1),X1),
inference(superposition,[],[f20,f41]) ).
fof(f118,plain,
! [X0,X1] : c_union(c_emptyset,X0,X1) = c_minus(X0,c_emptyset,tc_set(X1)),
inference(superposition,[],[f25,f20]) ).
fof(f119,plain,
! [X0,X1] : c_minus(X0,c_emptyset,tc_set(X1)) = X0,
inference(forward_demodulation,[],[f118,f25]) ).
fof(f125,plain,
c_uminus(c_emptyset,tc_set(t_a)) = c_union(c_uminus(v_a,tc_set(t_a)),c_uminus(v_t,tc_set(t_a)),t_a),
inference(superposition,[],[f72,f37]) ).
fof(f134,plain,
! [X2,X0,X1] : c_minus(X0,X2,tc_set(X1)) = c_uminus(c_union(c_uminus(X0,tc_set(X1)),X2,X1),tc_set(X1)),
inference(superposition,[],[f30,f12]) ).
fof(f135,plain,
! [X0] : c_UNIV = c_uminus(c_emptyset,tc_set(X0)),
inference(superposition,[],[f30,f14]) ).
fof(f136,plain,
! [X2,X0,X1] : c_minus(X1,X0,tc_set(X2)) = c_Relation_OImage(c_Relation_Odiag(X1,X2),c_uminus(X0,tc_set(X2)),X2,X2),
inference(superposition,[],[f41,f30]) ).
fof(f152,plain,
! [X2,X0,X1] : c_union(X0,c_uminus(X2,tc_set(X1)),X1) = c_union(c_Relation_OImage(c_Relation_Odiag(X0,X1),X2,X1,X1),c_uminus(X2,tc_set(X1)),X1),
inference(superposition,[],[f18,f41]) ).
fof(f260,plain,
c_union(c_union(v_a,v_t,t_a),c_uminus(v_u,tc_set(t_a)),t_a) = c_union(c_emptyset,c_uminus(v_u,tc_set(t_a)),t_a),
inference(superposition,[],[f152,f38]) ).
fof(f287,plain,
c_uminus(v_u,tc_set(t_a)) = c_union(c_union(v_a,v_t,t_a),c_uminus(v_u,tc_set(t_a)),t_a),
inference(forward_demodulation,[],[f260,f25]) ).
fof(f289,plain,
c_uminus(v_u,tc_set(t_a)) = c_union(v_a,c_union(v_t,c_uminus(v_u,tc_set(t_a)),t_a),t_a),
inference(forward_demodulation,[],[f287,f24]) ).
fof(f336,plain,
c_union(c_uminus(v_u,tc_set(t_a)),c_union(v_a,v_t,t_a),t_a) = c_union(c_uminus(v_u,tc_set(t_a)),c_emptyset,t_a),
inference(superposition,[],[f109,f38]) ).
fof(f356,plain,
c_uminus(v_u,tc_set(t_a)) = c_union(c_uminus(v_u,tc_set(t_a)),c_union(v_a,v_t,t_a),t_a),
inference(forward_demodulation,[],[f336,f26]) ).
fof(f379,plain,
! [X0] : c_union(c_uminus(v_u,tc_set(t_a)),X0,t_a) = c_union(c_uminus(v_u,tc_set(t_a)),c_union(c_union(v_a,v_t,t_a),X0,t_a),t_a),
inference(superposition,[],[f24,f356]) ).
fof(f382,plain,
! [X0] : c_union(c_uminus(v_u,tc_set(t_a)),X0,t_a) = c_union(c_uminus(v_u,tc_set(t_a)),c_union(v_a,c_union(v_t,X0,t_a),t_a),t_a),
inference(forward_demodulation,[],[f379,f24]) ).
fof(f716,plain,
! [X0,X1] : c_minus(c_emptyset,X0,tc_set(X1)) = c_uminus(c_union(c_UNIV,X0,X1),tc_set(X1)),
inference(superposition,[],[f134,f135]) ).
fof(f718,plain,
! [X2,X3,X0,X1] : c_minus(c_Relation_OImage(c_Relation_Odiag(X0,X1),X2,X1,X1),X3,tc_set(X1)) = c_uminus(c_union(c_union(c_uminus(X0,tc_set(X1)),c_uminus(X2,tc_set(X1)),X1),X3,X1),tc_set(X1)),
inference(superposition,[],[f134,f72]) ).
fof(f719,plain,
! [X2,X3,X0,X1] : c_minus(c_minus(X0,X2,tc_set(X1)),X3,tc_set(X1)) = c_uminus(c_union(c_union(c_uminus(X0,tc_set(X1)),X2,X1),X3,X1),tc_set(X1)),
inference(superposition,[],[f134,f12]) ).
fof(f720,plain,
! [X2,X0,X1] : c_minus(c_uminus(X0,tc_set(X1)),X2,tc_set(X1)) = c_uminus(c_union(X0,X2,X1),tc_set(X1)),
inference(superposition,[],[f134,f30]) ).
fof(f724,plain,
! [X2,X0,X1] : c_uminus(c_union(c_uminus(X0,tc_set(X1)),X2,X1),tc_set(X1)) = c_minus(X0,c_Relation_OImage(c_Relation_Odiag(X2,X1),X0,X1,X1),tc_set(X1)),
inference(superposition,[],[f134,f109]) ).
fof(f752,plain,
! [X2,X0,X1] : c_minus(X0,X2,tc_set(X1)) = c_minus(X0,c_Relation_OImage(c_Relation_Odiag(X2,X1),X0,X1,X1),tc_set(X1)),
inference(forward_demodulation,[],[f724,f134]) ).
fof(f756,plain,
! [X2,X3,X0,X1] : c_minus(c_minus(X0,X2,tc_set(X1)),X3,tc_set(X1)) = c_uminus(c_union(c_uminus(X0,tc_set(X1)),c_union(X2,X3,X1),X1),tc_set(X1)),
inference(forward_demodulation,[],[f719,f24]) ).
fof(f757,plain,
! [X2,X3,X0,X1] : c_minus(c_Relation_OImage(c_Relation_Odiag(X0,X1),X2,X1,X1),X3,tc_set(X1)) = c_uminus(c_union(c_uminus(X0,tc_set(X1)),c_union(c_uminus(X2,tc_set(X1)),X3,X1),X1),tc_set(X1)),
inference(forward_demodulation,[],[f718,f24]) ).
fof(f758,plain,
! [X0,X1] : c_uminus(c_UNIV,tc_set(X1)) = c_minus(c_emptyset,X0,tc_set(X1)),
inference(forward_demodulation,[],[f716,f22]) ).
fof(f761,plain,
! [X2,X3,X0,X1] : c_minus(X0,c_union(X2,X3,X1),tc_set(X1)) = c_minus(c_minus(X0,X2,tc_set(X1)),X3,tc_set(X1)),
inference(forward_demodulation,[],[f756,f134]) ).
fof(f762,plain,
! [X2,X3,X0,X1] : c_minus(X0,c_union(c_uminus(X2,tc_set(X1)),X3,X1),tc_set(X1)) = c_minus(c_Relation_OImage(c_Relation_Odiag(X0,X1),X2,X1,X1),X3,tc_set(X1)),
inference(forward_demodulation,[],[f757,f134]) ).
fof(f763,plain,
! [X0,X1] : c_emptyset = c_minus(c_emptyset,X0,tc_set(X1)),
inference(forward_demodulation,[],[f758,f14]) ).
fof(f778,plain,
! [X2,X0,X1] : c_uminus(c_union(X0,c_uminus(X1,tc_set(X2)),X2),tc_set(X2)) = c_Relation_OImage(c_Relation_Odiag(c_uminus(X0,tc_set(X2)),X2),X1,X2,X2),
inference(superposition,[],[f41,f720]) ).
fof(f982,plain,
! [X0,X1] : c_union(X0,c_uminus(X0,tc_set(X1)),X1) = c_union(c_UNIV,c_uminus(X0,tc_set(X1)),X1),
inference(superposition,[],[f152,f42]) ).
fof(f1004,plain,
! [X0,X1] : c_UNIV = c_union(X0,c_uminus(X0,tc_set(X1)),X1),
inference(forward_demodulation,[],[f982,f22]) ).
fof(f1022,plain,
! [X0,X1] : c_uminus(c_UNIV,tc_set(X1)) = c_minus(X0,c_uminus(c_uminus(X0,tc_set(X1)),tc_set(X1)),tc_set(X1)),
inference(superposition,[],[f134,f1004]) ).
fof(f1029,plain,
! [X0,X1] : c_UNIV = c_union(X0,c_UNIV,X1),
inference(superposition,[],[f58,f1004]) ).
fof(f1038,plain,
! [X0,X1] : c_uminus(c_UNIV,tc_set(X1)) = c_minus(X0,X0,tc_set(X1)),
inference(forward_demodulation,[],[f1022,f30]) ).
fof(f1041,plain,
! [X0,X1] : c_emptyset = c_minus(X0,X0,tc_set(X1)),
inference(forward_demodulation,[],[f1038,f14]) ).
fof(f1056,plain,
! [X2,X0,X1] : c_minus(c_emptyset,X1,tc_set(X2)) = c_minus(X0,c_union(X0,X1,X2),tc_set(X2)),
inference(superposition,[],[f761,f1041]) ).
fof(f1058,plain,
! [X2,X0,X1] : c_emptyset = c_minus(X0,c_union(X1,c_minus(X0,X1,tc_set(X2)),X2),tc_set(X2)),
inference(superposition,[],[f761,f1041]) ).
fof(f1063,plain,
! [X2,X0,X1] : c_emptyset = c_minus(X0,c_union(X1,X0,X2),tc_set(X2)),
inference(forward_demodulation,[],[f1058,f20]) ).
fof(f1064,plain,
! [X2,X0,X1] : c_emptyset = c_minus(X0,c_union(X0,X1,X2),tc_set(X2)),
inference(forward_demodulation,[],[f1056,f763]) ).
fof(f1106,plain,
! [X0,X1] : c_uminus(c_UNIV,tc_set(X1)) = c_minus(X0,c_UNIV,tc_set(X1)),
inference(superposition,[],[f134,f1029]) ).
fof(f1122,plain,
! [X0,X1] : c_emptyset = c_minus(X0,c_UNIV,tc_set(X1)),
inference(forward_demodulation,[],[f1106,f14]) ).
fof(f1546,plain,
c_emptyset = c_minus(v_a,c_uminus(v_u,tc_set(t_a)),tc_set(t_a)),
inference(superposition,[],[f1064,f289]) ).
fof(f1572,plain,
! [X2,X0,X1] : c_union(c_union(X0,X1,X2),c_emptyset,X2) = c_union(c_union(X0,X1,X2),X0,X2),
inference(superposition,[],[f20,f1064]) ).
fof(f1589,plain,
! [X2,X0,X1] : c_union(c_union(X0,X1,X2),c_emptyset,X2) = c_union(X0,c_union(X1,X0,X2),X2),
inference(forward_demodulation,[],[f1572,f24]) ).
fof(f1602,plain,
c_emptyset = c_Relation_OImage(c_Relation_Odiag(v_a,t_a),v_u,t_a,t_a),
inference(forward_demodulation,[],[f1546,f41]) ).
fof(f1607,plain,
! [X2,X0,X1] : c_union(X0,X1,X2) = c_union(X0,c_union(X1,X0,X2),X2),
inference(forward_demodulation,[],[f1589,f26]) ).
fof(f1644,plain,
c_union(c_uminus(v_t,tc_set(t_a)),c_uminus(c_emptyset,tc_set(t_a)),t_a) = c_union(c_uminus(v_t,tc_set(t_a)),c_uminus(v_a,tc_set(t_a)),t_a),
inference(superposition,[],[f1607,f125]) ).
fof(f1657,plain,
! [X2,X0,X1] : c_uminus(c_union(c_uminus(X0,tc_set(X1)),X2,X1),tc_set(X1)) = c_minus(X0,c_union(X2,c_uminus(X0,tc_set(X1)),X1),tc_set(X1)),
inference(superposition,[],[f134,f1607]) ).
fof(f1679,plain,
! [X2,X0,X1] : c_minus(X0,X2,tc_set(X1)) = c_minus(X0,c_union(X2,c_uminus(X0,tc_set(X1)),X1),tc_set(X1)),
inference(forward_demodulation,[],[f1657,f134]) ).
fof(f1686,plain,
c_union(c_uminus(v_t,tc_set(t_a)),c_UNIV,t_a) = c_union(c_uminus(v_t,tc_set(t_a)),c_uminus(v_a,tc_set(t_a)),t_a),
inference(forward_demodulation,[],[f1644,f135]) ).
fof(f1710,plain,
c_UNIV = c_union(c_uminus(v_t,tc_set(t_a)),c_uminus(v_a,tc_set(t_a)),t_a),
inference(forward_demodulation,[],[f1686,f1029]) ).
fof(f1730,plain,
c_uminus(c_UNIV,tc_set(t_a)) = c_minus(v_t,c_uminus(v_a,tc_set(t_a)),tc_set(t_a)),
inference(superposition,[],[f134,f1710]) ).
fof(f1731,plain,
! [X0] : c_minus(X0,c_UNIV,tc_set(t_a)) = c_Relation_OImage(c_Relation_Odiag(X0,t_a),c_minus(v_t,c_uminus(v_a,tc_set(t_a)),tc_set(t_a)),t_a,t_a),
inference(superposition,[],[f73,f1710]) ).
fof(f1750,plain,
! [X0] : c_minus(X0,c_UNIV,tc_set(t_a)) = c_Relation_OImage(c_Relation_Odiag(X0,t_a),c_Relation_OImage(c_Relation_Odiag(v_t,t_a),v_a,t_a,t_a),t_a,t_a),
inference(forward_demodulation,[],[f1731,f41]) ).
fof(f1751,plain,
c_uminus(c_UNIV,tc_set(t_a)) = c_Relation_OImage(c_Relation_Odiag(v_t,t_a),v_a,t_a,t_a),
inference(forward_demodulation,[],[f1730,f41]) ).
fof(f1752,plain,
! [X0] : c_emptyset = c_Relation_OImage(c_Relation_Odiag(X0,t_a),c_Relation_OImage(c_Relation_Odiag(v_t,t_a),v_a,t_a,t_a),t_a,t_a),
inference(forward_demodulation,[],[f1750,f1122]) ).
fof(f1753,plain,
c_emptyset = c_Relation_OImage(c_Relation_Odiag(v_t,t_a),v_a,t_a,t_a),
inference(forward_demodulation,[],[f1751,f14]) ).
fof(f2154,plain,
c_union(c_uminus(v_u,tc_set(t_a)),c_union(v_a,v_t,t_a),t_a) = c_union(c_uminus(v_u,tc_set(t_a)),v_t,t_a),
inference(superposition,[],[f382,f23]) ).
fof(f2201,plain,
c_uminus(v_u,tc_set(t_a)) = c_union(c_uminus(v_u,tc_set(t_a)),v_t,t_a),
inference(forward_demodulation,[],[f2154,f356]) ).
fof(f2651,plain,
c_emptyset = c_minus(v_t,c_uminus(v_u,tc_set(t_a)),tc_set(t_a)),
inference(superposition,[],[f1063,f2201]) ).
fof(f2676,plain,
! [X2,X0,X1] : c_union(X0,c_union(X1,X0,X2),X2) = c_union(c_emptyset,c_union(X1,X0,X2),X2),
inference(superposition,[],[f18,f1063]) ).
fof(f2700,plain,
! [X2,X0,X1] : c_union(X1,X0,X2) = c_union(X0,c_union(X1,X0,X2),X2),
inference(forward_demodulation,[],[f2676,f25]) ).
fof(f2715,plain,
c_emptyset = c_Relation_OImage(c_Relation_Odiag(v_t,t_a),v_u,t_a,t_a),
inference(forward_demodulation,[],[f2651,f41]) ).
fof(f2733,plain,
c_in(c_union(v_t,v_u,t_a),c_Mutil_Otiling(v_A,t_a),tc_set(t_a)),
inference(unit_resulting_resolution,[],[f39,f3,f2715]) ).
fof(f2747,plain,
c_emptyset != c_Relation_OImage(c_Relation_Odiag(v_a,t_a),c_union(v_t,v_u,t_a),t_a,t_a),
inference(unit_resulting_resolution,[],[f40,f1,f44,f2733]) ).
fof(f2807,plain,
! [X2,X0,X1] : c_uminus(c_union(X0,c_uminus(X1,tc_set(X2)),X2),tc_set(X2)) = c_minus(X1,c_union(X0,c_uminus(X1,tc_set(X2)),X2),tc_set(X2)),
inference(superposition,[],[f134,f2700]) ).
fof(f2843,plain,
! [X2,X0,X1] : c_minus(X1,X0,tc_set(X2)) = c_uminus(c_union(X0,c_uminus(X1,tc_set(X2)),X2),tc_set(X2)),
inference(forward_demodulation,[],[f2807,f1679]) ).
fof(f4729,plain,
! [X0] : c_minus(c_Relation_OImage(c_Relation_Odiag(v_t,t_a),v_a,t_a,t_a),X0,tc_set(t_a)) = c_minus(c_Relation_OImage(c_Relation_Odiag(v_t,t_a),v_a,t_a,t_a),c_emptyset,tc_set(t_a)),
inference(superposition,[],[f752,f1752]) ).
fof(f4811,plain,
! [X0] : c_Relation_OImage(c_Relation_Odiag(v_t,t_a),v_a,t_a,t_a) = c_minus(c_Relation_OImage(c_Relation_Odiag(v_t,t_a),v_a,t_a,t_a),X0,tc_set(t_a)),
inference(forward_demodulation,[],[f4729,f119]) ).
fof(f4837,plain,
! [X0] : c_Relation_OImage(c_Relation_Odiag(v_t,t_a),v_a,t_a,t_a) = c_minus(v_t,c_union(c_uminus(v_a,tc_set(t_a)),X0,t_a),tc_set(t_a)),
inference(forward_demodulation,[],[f4811,f762]) ).
fof(f4856,plain,
! [X0] : c_Relation_OImage(c_Relation_Odiag(v_t,t_a),v_a,t_a,t_a) = c_Relation_OImage(c_Relation_Odiag(v_t,t_a),c_minus(v_a,X0,tc_set(t_a)),t_a,t_a),
inference(forward_demodulation,[],[f4837,f73]) ).
fof(f4870,plain,
! [X0] : c_emptyset = c_Relation_OImage(c_Relation_Odiag(v_t,t_a),c_minus(v_a,X0,tc_set(t_a)),t_a,t_a),
inference(forward_demodulation,[],[f4856,f1753]) ).
fof(f5086,plain,
! [X0] : c_minus(c_minus(v_a,X0,tc_set(t_a)),c_emptyset,tc_set(t_a)) = c_minus(c_minus(v_a,X0,tc_set(t_a)),v_t,tc_set(t_a)),
inference(superposition,[],[f752,f4870]) ).
fof(f5088,plain,
! [X0] : c_minus(c_minus(v_a,X0,tc_set(t_a)),c_emptyset,tc_set(t_a)) = c_minus(v_a,c_union(X0,v_t,t_a),tc_set(t_a)),
inference(forward_demodulation,[],[f5086,f761]) ).
fof(f5101,plain,
! [X0] : c_minus(v_a,X0,tc_set(t_a)) = c_minus(v_a,c_union(X0,v_t,t_a),tc_set(t_a)),
inference(forward_demodulation,[],[f5088,f119]) ).
fof(f23804,plain,
! [X0] : c_minus(v_a,c_union(X0,v_t,t_a),tc_set(t_a)) = c_minus(v_a,c_minus(X0,v_t,tc_set(t_a)),tc_set(t_a)),
inference(superposition,[],[f5101,f18]) ).
fof(f23851,plain,
! [X0] : c_minus(v_a,X0,tc_set(t_a)) = c_minus(v_a,c_minus(X0,v_t,tc_set(t_a)),tc_set(t_a)),
inference(forward_demodulation,[],[f23804,f5101]) ).
fof(f27091,plain,
! [X2,X0,X1] : c_minus(c_uminus(X0,tc_set(X2)),X1,tc_set(X2)) = c_uminus(c_union(X0,c_uminus(c_uminus(X1,tc_set(X2)),tc_set(X2)),X2),tc_set(X2)),
inference(superposition,[],[f136,f778]) ).
fof(f27104,plain,
! [X2,X0,X1] : c_minus(c_uminus(X0,tc_set(X2)),X1,tc_set(X2)) = c_minus(c_uminus(X1,tc_set(X2)),X0,tc_set(X2)),
inference(forward_demodulation,[],[f27091,f2843]) ).
fof(f27220,plain,
! [X2,X0,X1] : c_minus(c_uminus(X0,tc_set(X2)),X1,tc_set(X2)) = c_uminus(c_union(X1,X0,X2),tc_set(X2)),
inference(forward_demodulation,[],[f27104,f720]) ).
fof(f27456,plain,
! [X0] : c_minus(v_a,c_uminus(X0,tc_set(t_a)),tc_set(t_a)) = c_minus(v_a,c_uminus(c_union(v_t,X0,t_a),tc_set(t_a)),tc_set(t_a)),
inference(superposition,[],[f23851,f27220]) ).
fof(f27478,plain,
! [X0] : c_minus(v_a,c_uminus(X0,tc_set(t_a)),tc_set(t_a)) = c_Relation_OImage(c_Relation_Odiag(v_a,t_a),c_union(v_t,X0,t_a),t_a,t_a),
inference(forward_demodulation,[],[f27456,f41]) ).
fof(f27539,plain,
! [X0] : c_Relation_OImage(c_Relation_Odiag(v_a,t_a),X0,t_a,t_a) = c_Relation_OImage(c_Relation_Odiag(v_a,t_a),c_union(v_t,X0,t_a),t_a,t_a),
inference(forward_demodulation,[],[f27478,f41]) ).
fof(f27624,plain,
c_emptyset != c_Relation_OImage(c_Relation_Odiag(v_a,t_a),v_u,t_a,t_a),
inference(superposition,[],[f2747,f27539]) ).
fof(f27657,plain,
$false,
inference(forward_subsumption_resolution,[],[f27624,f1602]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ064-2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n019.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 22:38:48 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.76/2.51 % (3484987)Input is clausal, will run a generic CNF schedule.
% 10.76/2.51 % (3485013)lrs+10_1_sil=8000:sp=occurrence:random_seed=632327588:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.76/2.51 % (3485013)Instruction limit reached!
% 10.76/2.51 % (3485013)------------------------------
% 10.76/2.51 % (3485013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.76/2.51 % (3485013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.76/2.51 % (3485013)CaDiCaL version: 2.1.3
% 10.76/2.51 % (3485013)Termination reason: Instruction limit
% 10.76/2.51 % (3485013)Termination phase: Saturation
% 10.76/2.51 % (3485013)Time elapsed: 0.040 s
% 10.76/2.51 % (3485013)Peak memory usage: 89 MB
% 10.76/2.51 % (3485013)Instructions burned: 108 (million)
% 10.76/2.51 % (3485014)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4153076801:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.76/2.51 % (3485015)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1216975465:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.76/2.51 % (3485016)dis-21_1_sil=8000:lcm=predicate:random_seed=485045701:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.76/2.51 % (3485011)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3114124350:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.76/2.51 % (3485012)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4014251590:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.76/2.51 % (3485010)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2966660220:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.76/2.51 % (3485016)Instruction limit reached!
% 10.76/2.51 % (3485016)------------------------------
% 10.76/2.51 % (3485016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.76/2.51 % (3485016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.76/2.51 % (3485016)CaDiCaL version: 2.1.3
% 10.76/2.51 % (3485016)Termination reason: Instruction limit
% 10.76/2.51 % (3485016)Termination phase: Saturation
% 10.76/2.51 % (3485016)Time elapsed: 0.064 s
% 10.76/2.51 % (3485016)Peak memory usage: 88 MB
% 10.76/2.51 % (3485016)Instructions burned: 118 (million)
% 10.76/2.51 % (3485014)Instruction limit reached!
% 10.76/2.51 % (3485014)------------------------------
% 10.76/2.51 % (3485014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.76/2.51 % (3485014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.76/2.51 % (3485014)CaDiCaL version: 2.1.3
% 10.76/2.51 % (3485014)Termination reason: Instruction limit
% 10.76/2.51 % (3485014)Termination phase: Saturation
% 10.76/2.51 % (3485014)Time elapsed: 0.074 s
% 10.76/2.51 % (3485014)Peak memory usage: 88 MB
% 10.76/2.51 % (3485014)Instructions burned: 115 (million)
% 10.76/2.51 % (3485018)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2012525146:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 10.76/2.51 % (3485018)Refutation not found, incomplete strategy
% 10.76/2.51 % (3485018)------------------------------
% 10.76/2.51 % (3485018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.76/2.51 % (3485018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.76/2.51 % (3485018)CaDiCaL version: 2.1.3
% 10.76/2.51 % (3485018)Termination reason: Refutation not found, incomplete strategy
% 10.76/2.51 % (3485018)Time elapsed: 0.001 s
% 10.76/2.51 % (3485018)Peak memory usage: 88 MB
% 10.76/2.51 % (3485018)Instructions burned: 2 (million)
% 10.76/2.51 % (3485015)Instruction limit reached!
% 10.76/2.51 % (3485015)------------------------------
% 10.76/2.51 % (3485015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.76/2.51 % (3485015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.76/2.51 % (3485015)CaDiCaL version: 2.1.3
% 10.76/2.51 % (3485015)Termination reason: Instruction limit
% 10.76/2.51 % (3485015)Termination phase: Saturation
% 10.76/2.51 % (3485015)Time elapsed: 0.112 s
% 10.76/2.51 % (3485015)Peak memory usage: 90 MB
% 10.76/2.51 % (3485015)Instructions burned: 181 (million)
% 10.76/2.51 % (3485025)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2138434675:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 16.93/3.39 % (3485026)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1824309560:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 16.93/3.39 % (3485026)Refutation not found, incomplete strategy
% 16.93/3.39 % (3485026)------------------------------
% 16.93/3.39 % (3485026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485026)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485026)Termination reason: Refutation not found, incomplete strategy
% 16.93/3.39 % (3485026)Time elapsed: 0.002 s
% 16.93/3.39 % (3485026)Peak memory usage: 88 MB
% 16.93/3.39 % (3485026)Instructions burned: 1 (million)
% 16.93/3.39 % (3485018)------------------------------
% 16.93/3.39 % (3485018)------------------------------
% 16.93/3.39 % (3485028)lrs+10_64_to=lpo:sil=8000:random_seed=1859172758:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 16.93/3.39 % (3485025)Instruction limit reached!
% 16.93/3.39 % (3485025)------------------------------
% 16.93/3.39 % (3485025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485025)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485025)Termination reason: Instruction limit
% 16.93/3.39 % (3485025)Termination phase: Saturation
% 16.93/3.39 % (3485025)Time elapsed: 0.110 s
% 16.93/3.39 % (3485025)Peak memory usage: 91 MB
% 16.93/3.39 % (3485025)Instructions burned: 189 (million)
% 16.93/3.39 % (3485028)Instruction limit reached!
% 16.93/3.39 % (3485028)------------------------------
% 16.93/3.39 % (3485028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485028)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485028)Termination reason: Instruction limit
% 16.93/3.39 % (3485028)Termination phase: Saturation
% 16.93/3.39 % (3485028)Time elapsed: 0.077 s
% 16.93/3.39 % (3485028)Peak memory usage: 89 MB
% 16.93/3.39 % (3485028)Instructions burned: 127 (million)
% 16.93/3.39 % (3485031)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=195310868:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 16.93/3.39 % (3485031)Instruction limit reached!
% 16.93/3.39 % (3485031)------------------------------
% 16.93/3.39 % (3485031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485031)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485031)Termination reason: Instruction limit
% 16.93/3.39 % (3485031)Termination phase: Saturation
% 16.93/3.39 % (3485031)Time elapsed: 0.056 s
% 16.93/3.39 % (3485031)Peak memory usage: 90 MB
% 16.93/3.39 % (3485031)Instructions burned: 196 (million)
% 16.93/3.39 % (3485026)------------------------------
% 16.93/3.39 % (3485026)------------------------------
% 16.93/3.39 % (3485033)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1470698821:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 16.93/3.39 % (3485034)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1736980148:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 16.93/3.39 % (3485036)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2088995415:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 16.93/3.39 % (3485036)Instruction limit reached!
% 16.93/3.39 % (3485036)------------------------------
% 16.93/3.39 % (3485036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485036)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485036)Termination reason: Instruction limit
% 16.93/3.39 % (3485036)Termination phase: Saturation
% 16.93/3.39 % (3485036)Time elapsed: 0.031 s
% 16.93/3.39 % (3485036)Peak memory usage: 88 MB
% 16.93/3.39 % (3485036)Instructions burned: 107 (million)
% 16.93/3.39 % (3485033)Instruction limit reached!
% 16.93/3.39 % (3485033)------------------------------
% 16.93/3.39 % (3485033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485033)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485033)Termination reason: Instruction limit
% 16.93/3.39 % (3485033)Termination phase: Saturation
% 16.93/3.39 % (3485033)Time elapsed: 0.107 s
% 16.93/3.39 % (3485033)Peak memory usage: 90 MB
% 16.93/3.39 % (3485033)Instructions burned: 158 (million)
% 16.93/3.39 % (3485038)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3952620579:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 16.93/3.39 % (3485038)Refutation not found, incomplete strategy
% 16.93/3.39 % (3485038)------------------------------
% 16.93/3.39 % (3485038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485038)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485038)Termination reason: Refutation not found, incomplete strategy
% 16.93/3.39 % (3485038)Time elapsed: 0.002 s
% 16.93/3.39 % (3485038)Peak memory usage: 88 MB
% 16.93/3.39 % (3485038)Instructions burned: 2 (million)
% 16.93/3.39 % (3485041)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1330205136:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 16.93/3.39 % (3485042)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4260408388:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 16.93/3.39 % (3485041)Instruction limit reached!
% 16.93/3.39 % (3485041)------------------------------
% 16.93/3.39 % (3485041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485041)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485041)Termination reason: Instruction limit
% 16.93/3.39 % (3485041)Termination phase: Saturation
% 16.93/3.39 % (3485041)Time elapsed: 0.075 s
% 16.93/3.39 % (3485041)Peak memory usage: 88 MB
% 16.93/3.39 % (3485041)Instructions burned: 245 (million)
% 16.93/3.39 % (3485038)------------------------------
% 16.93/3.39 % (3485038)------------------------------
% 16.93/3.39 % (3485046)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=573215167:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 16.93/3.39 % (3485046)Instruction limit reached!
% 16.93/3.39 % (3485046)------------------------------
% 16.93/3.39 % (3485046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485046)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485046)Termination reason: Instruction limit
% 16.93/3.39 % (3485046)Termination phase: Saturation
% 16.93/3.39 % (3485046)Time elapsed: 0.045 s
% 16.93/3.39 % (3485046)Peak memory usage: 89 MB
% 16.93/3.39 % (3485046)Instructions burned: 137 (million)
% 16.93/3.39 % (3485048)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1051007455:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 16.93/3.39 % (3485050)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3634918818:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 16.93/3.39 % (3485050)Instruction limit reached!
% 16.93/3.39 % (3485050)------------------------------
% 16.93/3.39 % (3485050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485050)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485050)Termination reason: Instruction limit
% 16.93/3.39 % (3485050)Termination phase: Saturation
% 16.93/3.39 % (3485050)Time elapsed: 0.063 s
% 16.93/3.39 % (3485050)Peak memory usage: 91 MB
% 16.93/3.39 % (3485050)Instructions burned: 196 (million)
% 16.93/3.39 % (3485053)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3772363517:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 16.93/3.39 % (3485053)Instruction limit reached!
% 16.93/3.39 % (3485053)------------------------------
% 16.93/3.39 % (3485053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485053)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485053)Termination reason: Instruction limit
% 16.93/3.39 % (3485053)Termination phase: Saturation
% 16.93/3.39 % (3485053)Time elapsed: 0.081 s
% 16.93/3.39 % (3485053)Peak memory usage: 92 MB
% 16.93/3.39 % (3485053)Instructions burned: 267 (million)
% 16.93/3.39 % (3485048)Instruction limit reached!
% 16.93/3.39 % (3485048)------------------------------
% 16.93/3.39 % (3485048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485048)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485048)Termination reason: Instruction limit
% 16.93/3.39 % (3485048)Termination phase: Saturation
% 16.93/3.39 % (3485048)Time elapsed: 0.308 s
% 16.93/3.39 % (3485048)Peak memory usage: 92 MB
% 16.93/3.39 % (3485048)Instructions burned: 500 (million)
% 16.93/3.39 % (3485055)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3480718985:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 16.93/3.39 % (3485055)Instruction limit reached!
% 16.93/3.39 % (3485055)------------------------------
% 16.93/3.39 % (3485055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485055)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485055)Termination reason: Instruction limit
% 16.93/3.39 % (3485055)Termination phase: Saturation
% 16.93/3.39 % (3485055)Time elapsed: 0.052 s
% 16.93/3.39 % (3485055)Peak memory usage: 89 MB
% 16.93/3.39 % (3485055)Instructions burned: 158 (million)
% 16.93/3.39 % (3485056)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=272242861:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi)
% 16.93/3.39 % (3485058)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1653307659:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 16.93/3.39 % (3485058)Instruction limit reached!
% 16.93/3.39 % (3485058)------------------------------
% 16.93/3.39 % (3485058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485058)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485058)Termination reason: Instruction limit
% 16.93/3.39 % (3485058)Termination phase: Saturation
% 16.93/3.39 % (3485058)Time elapsed: 0.164 s
% 16.93/3.39 % (3485058)Peak memory usage: 91 MB
% 16.93/3.39 % (3485058)Instructions burned: 537 (million)
% 16.93/3.39 % (3485061)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1384358381:i=180:bd=preordered:av=off_2979 on theBenchmark for (2979ds/180Mi)
% 16.93/3.39 % (3485011)First to succeed.
% 16.93/3.39 % (3485011)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3484987"
% 16.93/3.39 % (3485061)Instruction limit reached!
% 16.93/3.39 % (3485061)------------------------------
% 16.93/3.39 % (3485061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.39 % (3485061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.39 % (3485061)CaDiCaL version: 2.1.3
% 16.93/3.39 % (3485061)Termination reason: Instruction limit
% 16.93/3.39 % (3485061)Termination phase: Saturation
% 16.93/3.39 % (3485061)Time elapsed: 0.053 s
% 16.93/3.39 % (3485061)Peak memory usage: 88 MB
% 16.93/3.39 % (3485061)Instructions burned: 183 (million)
% 16.93/3.39 % (3485063)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1058219582:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2978 on theBenchmark for (2978ds/10307Mi)
% 16.93/3.39 % (3485011)Refutation found. Thanks to Tanya!
% 16.93/3.39 % SZS status Unsatisfiable for theBenchmark
% 16.93/3.39 % SZS output start Proof for theBenchmark
% See solution above
% 17.81/3.59 % (3485011)------------------------------
% 17.81/3.59 % (3485011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.81/3.59 % (3485011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.81/3.59 % (3485011)CaDiCaL version: 2.1.3
% 17.81/3.59 % (3485011)Termination reason: Refutation
% 17.81/3.59 % (3485011)Time elapsed: 1.943 s
% 17.81/3.59 % (3485011)Peak memory usage: 143 MB
% 17.81/3.59 % (3485011)Instructions burned: 2995 (million)
% 17.81/3.59 % (3485011)------------------------------
% 17.81/3.59 % (3485011)------------------------------
% 17.81/3.59 % (3484987)Success in time 2.428 s
% 17.81/3.59 % Vampire exiting
%------------------------------------------------------------------------------