%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU427+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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 12:53:15 PM UTC 2026
% Result : Theorem 14.61s 5.41s
% Output : Refutation 14.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 22
% Syntax : Number of formulae : 125 ( 64 unt; 9 def)
% Number of atoms : 230 ( 95 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 178 ( 73 ~; 67 |; 18 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 15 con; 0-4 aty)
% Number of variables : 171 ( 161 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X0))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ( k4_relset_2(k1_zfmisc_1(X0),X1,k6_relset_2(X1,X0,X4),k3_pua2mss1(X2)) = k1_xboole_0
=> k8_relset_2(X0,X1,k4_subset_1(X0,X2,X3),X4) = k8_relset_2(X0,X1,X3,X4) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t26_relset_2) ).
fof(f2,negated_conjecture,
~ ! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X0))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ( k4_relset_2(k1_zfmisc_1(X0),X1,k6_relset_2(X1,X0,X4),k3_pua2mss1(X2)) = k1_xboole_0
=> k8_relset_2(X0,X1,k4_subset_1(X0,X2,X3),X4) = k8_relset_2(X0,X1,X3,X4) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f5,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f6,axiom,
! [X0,X1] : k2_xboole_0(X0,X1) = k2_xboole_0(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_xboole_0) ).
fof(f8,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> k7_relset_2(X0,X1,X2,X3) = k8_setfam_1(X1,k4_relset_2(k1_zfmisc_1(X0),X1,k6_relset_2(X1,X0,X3),k3_pua2mss1(X2))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_relset_2) ).
fof(f15,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_subset_1) ).
fof(f17,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X0)))
=> ( v1_funct_1(k6_relset_2(X0,X1,X2))
& v1_funct_2(k6_relset_2(X0,X1,X2),k1_zfmisc_1(X1),k1_zfmisc_1(X0))
& m2_relset_1(k6_relset_2(X0,X1,X2),k1_zfmisc_1(X1),k1_zfmisc_1(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_relset_2) ).
fof(f25,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f44,axiom,
! [X0,X1,X2,X3] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,k1_zfmisc_1(X1))))
=> k4_relset_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_relset_2) ).
fof(f45,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_subset_1) ).
fof(f47,axiom,
! [X0,X1,X2,X3] :
( ( m1_subset_1(X2,k1_zfmisc_1(X0))
& m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
=> k8_relset_2(X0,X1,X2,X3) = k7_relset_2(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k8_relset_2) ).
fof(f50,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> k9_relat_1(X2,k2_xboole_0(X0,X1)) = k2_xboole_0(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t153_relat_1) ).
fof(f51,axiom,
! [X0] : k2_xboole_0(X0,k1_xboole_0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_boole) ).
fof(f54,axiom,
! [X0,X1] : k3_pua2mss1(k2_xboole_0(X0,X1)) = k2_xboole_0(k3_pua2mss1(X0),k3_pua2mss1(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_relset_2) ).
fof(f66,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X0)))
=> ( v1_funct_1(k6_relset_2(X0,X1,X2))
& m2_relset_1(k6_relset_2(X0,X1,X2),k1_zfmisc_1(X1),k1_zfmisc_1(X0)) ) ),
inference(pure_predicate_removal,[],[f17]) ).
fof(f68,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X0)))
=> m2_relset_1(k6_relset_2(X0,X1,X2),k1_zfmisc_1(X1),k1_zfmisc_1(X0)) ),
inference(pure_predicate_removal,[],[f66]) ).
fof(f70,plain,
? [X0,X1,X2] :
( ? [X3] :
( ? [X4] :
( k8_relset_2(X0,X1,k4_subset_1(X0,X2,X3),X4) != k8_relset_2(X0,X1,X3,X4)
& k4_relset_2(k1_zfmisc_1(X0),X1,k6_relset_2(X1,X0,X4),k3_pua2mss1(X2)) = k1_xboole_0
& m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
& m1_subset_1(X3,k1_zfmisc_1(X0)) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f2]) ).
fof(f71,plain,
? [X0,X1,X2] :
( ? [X3] :
( ? [X4] :
( k8_relset_2(X0,X1,k4_subset_1(X0,X2,X3),X4) != k8_relset_2(X0,X1,X3,X4)
& k4_relset_2(k1_zfmisc_1(X0),X1,k6_relset_2(X1,X0,X4),k3_pua2mss1(X2)) = k1_xboole_0
& m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
& m1_subset_1(X3,k1_zfmisc_1(X0)) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f70]) ).
fof(f74,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f5]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ! [X3] :
( k7_relset_2(X0,X1,X2,X3) = k8_setfam_1(X1,k4_relset_2(k1_zfmisc_1(X0),X1,k6_relset_2(X1,X0,X3),k3_pua2mss1(X2)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f8]) ).
fof(f79,plain,
! [X0,X1,X2] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f15]) ).
fof(f80,plain,
! [X0,X1,X2] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f79]) ).
fof(f82,plain,
! [X0,X1,X2] :
( m2_relset_1(k6_relset_2(X0,X1,X2),k1_zfmisc_1(X1),k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X0))) ),
inference(ennf_transformation,[],[f68]) ).
fof(f87,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f95,plain,
! [X0,X1,X2,X3] :
( k4_relset_2(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,k1_zfmisc_1(X1)))) ),
inference(ennf_transformation,[],[f44]) ).
fof(f96,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f45]) ).
fof(f97,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f96]) ).
fof(f99,plain,
! [X0,X1,X2,X3] :
( k8_relset_2(X0,X1,X2,X3) = k7_relset_2(X0,X1,X2,X3)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f47]) ).
fof(f100,plain,
! [X0,X1,X2,X3] :
( k8_relset_2(X0,X1,X2,X3) = k7_relset_2(X0,X1,X2,X3)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(flattening,[],[f99]) ).
fof(f101,plain,
! [X0,X1,X2] :
( k9_relat_1(X2,k2_xboole_0(X0,X1)) = k2_xboole_0(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f50]) ).
fof(f112,plain,
( k8_relset_2(sK0,sK1,k4_subset_1(sK0,sK2,sK3),sK4) != k8_relset_2(sK0,sK1,sK3,sK4)
& k1_xboole_0 = k4_relset_2(k1_zfmisc_1(sK0),sK1,k6_relset_2(sK1,sK0,sK4),k3_pua2mss1(sK2))
& m1_subset_1(sK4,k1_zfmisc_1(k2_zfmisc_1(sK0,sK1)))
& m1_subset_1(sK3,k1_zfmisc_1(sK0))
& m1_subset_1(sK2,k1_zfmisc_1(sK0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4)],[f71]) ).
fof(f124,plain,
m1_subset_1(sK2,k1_zfmisc_1(sK0)),
inference(cnf_transformation,[],[f112]) ).
fof(f125,plain,
m1_subset_1(sK3,k1_zfmisc_1(sK0)),
inference(cnf_transformation,[],[f112]) ).
fof(f126,plain,
m1_subset_1(sK4,k1_zfmisc_1(k2_zfmisc_1(sK0,sK1))),
inference(cnf_transformation,[],[f112]) ).
fof(f127,plain,
k1_xboole_0 = k4_relset_2(k1_zfmisc_1(sK0),sK1,k6_relset_2(sK1,sK0,sK4),k3_pua2mss1(sK2)),
inference(cnf_transformation,[],[f112]) ).
fof(f128,plain,
k8_relset_2(sK0,sK1,k4_subset_1(sK0,sK2,sK3),sK4) != k8_relset_2(sK0,sK1,sK3,sK4),
inference(cnf_transformation,[],[f112]) ).
fof(f131,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f74]) ).
fof(f132,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k2_xboole_0(X1,X0),
inference(cnf_transformation,[],[f6]) ).
fof(f134,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| k7_relset_2(X0,X1,X2,X3) = k8_setfam_1(X1,k4_relset_2(k1_zfmisc_1(X0),X1,k6_relset_2(X1,X0,X3),k3_pua2mss1(X2)))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f77]) ).
fof(f137,plain,
! [X2,X0,X1] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f80]) ).
fof(f139,plain,
! [X2,X0,X1] :
( m2_relset_1(k6_relset_2(X0,X1,X2),k1_zfmisc_1(X1),k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X0))) ),
inference(cnf_transformation,[],[f82]) ).
fof(f143,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f87]) ).
fof(f169,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,k1_zfmisc_1(X1))))
| k4_relset_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(cnf_transformation,[],[f95]) ).
fof(f170,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2) ),
inference(cnf_transformation,[],[f97]) ).
fof(f172,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| k7_relset_2(X0,X1,X2,X3) = k8_relset_2(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f100]) ).
fof(f176,plain,
! [X2,X0,X1] :
( ~ v1_relat_1(X2)
| k9_relat_1(X2,k2_xboole_0(X0,X1)) = k2_xboole_0(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ),
inference(cnf_transformation,[],[f101]) ).
fof(f177,plain,
! [X0] : k2_xboole_0(X0,k1_xboole_0) = X0,
inference(cnf_transformation,[],[f51]) ).
fof(f180,plain,
! [X0,X1] : k3_pua2mss1(k2_xboole_0(X0,X1)) = k2_xboole_0(k3_pua2mss1(X0),k3_pua2mss1(X1)),
inference(cnf_transformation,[],[f54]) ).
fof(f187,definition,
sF15 = k4_subset_1(sK0,sK2,sK3),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f188,plain,
k4_subset_1(sK0,sK2,sK3) = sF15,
inference(reorient_equations,[],[f187]) ).
fof(f189,definition,
sF16 = k8_relset_2(sK0,sK1,sF15,sK4),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f190,plain,
k8_relset_2(sK0,sK1,sF15,sK4) = sF16,
inference(reorient_equations,[],[f189]) ).
fof(f191,definition,
sF17 = k8_relset_2(sK0,sK1,sK3,sK4),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f192,plain,
k8_relset_2(sK0,sK1,sK3,sK4) = sF17,
inference(reorient_equations,[],[f191]) ).
fof(f193,plain,
sF16 != sF17,
inference(definition_folding,[],[f128,f192,f190,f188]) ).
fof(f194,definition,
sF18 = k1_zfmisc_1(sK0),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f195,plain,
k1_zfmisc_1(sK0) = sF18,
inference(reorient_equations,[],[f194]) ).
fof(f196,definition,
sF19 = k6_relset_2(sK1,sK0,sK4),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f197,plain,
k6_relset_2(sK1,sK0,sK4) = sF19,
inference(reorient_equations,[],[f196]) ).
fof(f198,definition,
sF20 = k3_pua2mss1(sK2),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f199,plain,
k3_pua2mss1(sK2) = sF20,
inference(reorient_equations,[],[f198]) ).
fof(f200,definition,
sF21 = k4_relset_2(sF18,sK1,sF19,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f201,plain,
k4_relset_2(sF18,sK1,sF19,sF20) = sF21,
inference(reorient_equations,[],[f200]) ).
fof(f202,plain,
k1_xboole_0 = sF21,
inference(definition_folding,[],[f127,f201,f199,f197,f195]) ).
fof(f203,definition,
sF22 = k2_zfmisc_1(sK0,sK1),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f204,plain,
k2_zfmisc_1(sK0,sK1) = sF22,
inference(reorient_equations,[],[f203]) ).
fof(f205,definition,
sF23 = k1_zfmisc_1(sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f206,plain,
k1_zfmisc_1(sF22) = sF23,
inference(reorient_equations,[],[f205]) ).
fof(f207,plain,
m1_subset_1(sK4,sF23),
inference(definition_folding,[],[f126,f206,f204]) ).
fof(f208,plain,
m1_subset_1(sK3,sF18),
inference(definition_folding,[],[f125,f195]) ).
fof(f209,plain,
m1_subset_1(sK2,sF18),
inference(definition_folding,[],[f124,f195]) ).
fof(f210,plain,
k1_xboole_0 = k4_relset_2(sF18,sK1,sF19,sF20),
inference(forward_demodulation,[],[f201,f202]) ).
fof(f235,plain,
! [X0] : k2_xboole_0(k1_xboole_0,X0) = X0,
inference(superposition,[],[f177,f132]) ).
fof(f327,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f143,f131]) ).
fof(f336,plain,
! [X0] : k3_pua2mss1(k2_xboole_0(sK2,X0)) = k2_xboole_0(sF20,k3_pua2mss1(X0)),
inference(superposition,[],[f180,f199]) ).
fof(f395,plain,
( m1_subset_1(sF15,k1_zfmisc_1(sK0))
| ~ m1_subset_1(sK2,k1_zfmisc_1(sK0))
| ~ m1_subset_1(sK3,k1_zfmisc_1(sK0)) ),
inference(superposition,[],[f137,f188]) ).
fof(f398,plain,
( m1_subset_1(sF15,sF18)
| ~ m1_subset_1(sK2,k1_zfmisc_1(sK0))
| ~ m1_subset_1(sK3,k1_zfmisc_1(sK0)) ),
inference(forward_demodulation,[],[f395,f195]) ).
fof(f400,plain,
( ~ m1_subset_1(sK2,sF18)
| m1_subset_1(sF15,sF18)
| ~ m1_subset_1(sK3,k1_zfmisc_1(sK0)) ),
inference(forward_demodulation,[],[f398,f195]) ).
fof(f401,plain,
( m1_subset_1(sF15,sF18)
| ~ m1_subset_1(sK3,k1_zfmisc_1(sK0)) ),
inference(forward_subsumption_resolution,[],[f400,f209]) ).
fof(f402,plain,
( ~ m1_subset_1(sK3,sF18)
| m1_subset_1(sF15,sF18) ),
inference(forward_demodulation,[],[f401,f195]) ).
fof(f403,plain,
m1_subset_1(sF15,sF18),
inference(forward_subsumption_resolution,[],[f402,f208]) ).
fof(f407,plain,
( m2_relset_1(sF19,k1_zfmisc_1(sK0),k1_zfmisc_1(sK1))
| ~ m1_subset_1(sK4,k1_zfmisc_1(k2_zfmisc_1(sK0,sK1))) ),
inference(superposition,[],[f139,f197]) ).
fof(f412,plain,
( m2_relset_1(sF19,sF18,k1_zfmisc_1(sK1))
| ~ m1_subset_1(sK4,k1_zfmisc_1(k2_zfmisc_1(sK0,sK1))) ),
inference(forward_demodulation,[],[f407,f195]) ).
fof(f413,plain,
( ~ m1_subset_1(sK4,k1_zfmisc_1(sF22))
| m2_relset_1(sF19,sF18,k1_zfmisc_1(sK1)) ),
inference(forward_demodulation,[],[f412,f204]) ).
fof(f414,plain,
( ~ m1_subset_1(sK4,sF23)
| m2_relset_1(sF19,sF18,k1_zfmisc_1(sK1)) ),
inference(forward_demodulation,[],[f413,f206]) ).
fof(f415,plain,
m2_relset_1(sF19,sF18,k1_zfmisc_1(sK1)),
inference(forward_subsumption_resolution,[],[f414,f207]) ).
fof(f443,plain,
! [X2,X3,X0,X1] :
( ~ m2_relset_1(X2,X0,k1_zfmisc_1(X1))
| k4_relset_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(resolution,[],[f169,f143]) ).
fof(f465,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF18)
| ~ m1_subset_1(X0,sF18)
| k2_xboole_0(X1,X0) = k4_subset_1(sK0,X1,X0) ),
inference(superposition,[],[f170,f195]) ).
fof(f539,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF22))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK0))
| k7_relset_2(sK0,sK1,X1,X0) = k8_relset_2(sK0,sK1,X1,X0) ),
inference(superposition,[],[f172,f204]) ).
fof(f540,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF23)
| ~ m1_subset_1(X1,k1_zfmisc_1(sK0))
| k7_relset_2(sK0,sK1,X1,X0) = k8_relset_2(sK0,sK1,X1,X0) ),
inference(forward_demodulation,[],[f539,f206]) ).
fof(f542,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF18)
| ~ m1_subset_1(X0,sF23)
| k7_relset_2(sK0,sK1,X1,X0) = k8_relset_2(sK0,sK1,X1,X0) ),
inference(forward_demodulation,[],[f540,f195]) ).
fof(f559,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF22))
| k7_relset_2(sK0,sK1,X1,X0) = k8_setfam_1(sK1,k4_relset_2(k1_zfmisc_1(sK0),sK1,k6_relset_2(sK1,sK0,X0),k3_pua2mss1(X1)))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK0)) ),
inference(superposition,[],[f134,f204]) ).
fof(f560,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF23)
| k7_relset_2(sK0,sK1,X1,X0) = k8_setfam_1(sK1,k4_relset_2(k1_zfmisc_1(sK0),sK1,k6_relset_2(sK1,sK0,X0),k3_pua2mss1(X1)))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK0)) ),
inference(forward_demodulation,[],[f559,f206]) ).
fof(f564,plain,
! [X0,X1] :
( k7_relset_2(sK0,sK1,X1,X0) = k8_setfam_1(sK1,k4_relset_2(sF18,sK1,k6_relset_2(sK1,sK0,X0),k3_pua2mss1(X1)))
| ~ m1_subset_1(X0,sF23)
| ~ m1_subset_1(X1,k1_zfmisc_1(sK0)) ),
inference(forward_demodulation,[],[f560,f195]) ).
fof(f566,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF18)
| k7_relset_2(sK0,sK1,X1,X0) = k8_setfam_1(sK1,k4_relset_2(sF18,sK1,k6_relset_2(sK1,sK0,X0),k3_pua2mss1(X1)))
| ~ m1_subset_1(X0,sF23) ),
inference(forward_demodulation,[],[f564,f195]) ).
fof(f588,plain,
v1_relat_1(sF19),
inference(resolution,[],[f327,f415]) ).
fof(f589,plain,
! [X0,X1] : k9_relat_1(sF19,k2_xboole_0(X0,X1)) = k2_xboole_0(k9_relat_1(sF19,X0),k9_relat_1(sF19,X1)),
inference(resolution,[],[f588,f176]) ).
fof(f1019,plain,
! [X0] : k9_relat_1(sF19,X0) = k4_relset_2(sF18,sK1,sF19,X0),
inference(resolution,[],[f443,f415]) ).
fof(f1023,plain,
k1_xboole_0 = k9_relat_1(sF19,sF20),
inference(superposition,[],[f210,f1019]) ).
fof(f1029,plain,
! [X0] :
( ~ m1_subset_1(X0,sF18)
| k2_xboole_0(sK2,X0) = k4_subset_1(sK0,sK2,X0) ),
inference(resolution,[],[f465,f209]) ).
fof(f1431,plain,
! [X0] :
( ~ m1_subset_1(X0,sF23)
| k7_relset_2(sK0,sK1,sK3,X0) = k8_relset_2(sK0,sK1,sK3,X0) ),
inference(resolution,[],[f542,f208]) ).
fof(f1435,plain,
! [X0] :
( ~ m1_subset_1(X0,sF23)
| k7_relset_2(sK0,sK1,sF15,X0) = k8_relset_2(sK0,sK1,sF15,X0) ),
inference(resolution,[],[f542,f403]) ).
fof(f1483,plain,
k4_subset_1(sK0,sK2,sK3) = k2_xboole_0(sK2,sK3),
inference(resolution,[],[f1029,f208]) ).
fof(f1489,plain,
sF15 = k2_xboole_0(sK2,sK3),
inference(forward_demodulation,[],[f1483,f188]) ).
fof(f1502,plain,
k2_xboole_0(sF20,k3_pua2mss1(sK3)) = k3_pua2mss1(sF15),
inference(superposition,[],[f336,f1489]) ).
fof(f1806,plain,
! [X0] :
( ~ m1_subset_1(X0,sF23)
| k7_relset_2(sK0,sK1,sK3,X0) = k8_setfam_1(sK1,k4_relset_2(sF18,sK1,k6_relset_2(sK1,sK0,X0),k3_pua2mss1(sK3))) ),
inference(resolution,[],[f566,f208]) ).
fof(f1810,plain,
! [X0] :
( ~ m1_subset_1(X0,sF23)
| k7_relset_2(sK0,sK1,sF15,X0) = k8_setfam_1(sK1,k4_relset_2(sF18,sK1,k6_relset_2(sK1,sK0,X0),k3_pua2mss1(sF15))) ),
inference(resolution,[],[f566,f403]) ).
fof(f2663,plain,
k8_relset_2(sK0,sK1,sK3,sK4) = k7_relset_2(sK0,sK1,sK3,sK4),
inference(resolution,[],[f1431,f207]) ).
fof(f2669,plain,
sF17 = k7_relset_2(sK0,sK1,sK3,sK4),
inference(forward_demodulation,[],[f2663,f192]) ).
fof(f2689,plain,
k8_relset_2(sK0,sK1,sF15,sK4) = k7_relset_2(sK0,sK1,sF15,sK4),
inference(resolution,[],[f1435,f207]) ).
fof(f2695,plain,
sF16 = k7_relset_2(sK0,sK1,sF15,sK4),
inference(forward_demodulation,[],[f2689,f190]) ).
fof(f2740,plain,
k7_relset_2(sK0,sK1,sK3,sK4) = k8_setfam_1(sK1,k4_relset_2(sF18,sK1,k6_relset_2(sK1,sK0,sK4),k3_pua2mss1(sK3))),
inference(resolution,[],[f1806,f207]) ).
fof(f2748,plain,
k7_relset_2(sK0,sK1,sK3,sK4) = k8_setfam_1(sK1,k4_relset_2(sF18,sK1,sF19,k3_pua2mss1(sK3))),
inference(forward_demodulation,[],[f2740,f197]) ).
fof(f2753,plain,
k7_relset_2(sK0,sK1,sK3,sK4) = k8_setfam_1(sK1,k9_relat_1(sF19,k3_pua2mss1(sK3))),
inference(forward_demodulation,[],[f2748,f1019]) ).
fof(f2756,plain,
sF17 = k8_setfam_1(sK1,k9_relat_1(sF19,k3_pua2mss1(sK3))),
inference(forward_demodulation,[],[f2753,f2669]) ).
fof(f2764,plain,
k7_relset_2(sK0,sK1,sF15,sK4) = k8_setfam_1(sK1,k4_relset_2(sF18,sK1,k6_relset_2(sK1,sK0,sK4),k3_pua2mss1(sF15))),
inference(resolution,[],[f1810,f207]) ).
fof(f2772,plain,
k7_relset_2(sK0,sK1,sF15,sK4) = k8_setfam_1(sK1,k4_relset_2(sF18,sK1,sF19,k3_pua2mss1(sF15))),
inference(forward_demodulation,[],[f2764,f197]) ).
fof(f2777,plain,
k7_relset_2(sK0,sK1,sF15,sK4) = k8_setfam_1(sK1,k9_relat_1(sF19,k3_pua2mss1(sF15))),
inference(forward_demodulation,[],[f2772,f1019]) ).
fof(f2780,plain,
sF16 = k8_setfam_1(sK1,k9_relat_1(sF19,k3_pua2mss1(sF15))),
inference(forward_demodulation,[],[f2777,f2695]) ).
fof(f22615,plain,
! [X0] : k9_relat_1(sF19,k2_xboole_0(sF20,X0)) = k2_xboole_0(k1_xboole_0,k9_relat_1(sF19,X0)),
inference(superposition,[],[f589,f1023]) ).
fof(f22645,plain,
! [X0] : k9_relat_1(sF19,X0) = k9_relat_1(sF19,k2_xboole_0(sF20,X0)),
inference(forward_demodulation,[],[f22615,f235]) ).
fof(f22756,plain,
k9_relat_1(sF19,k3_pua2mss1(sK3)) = k9_relat_1(sF19,k3_pua2mss1(sF15)),
inference(superposition,[],[f22645,f1502]) ).
fof(f22837,plain,
sF16 = k8_setfam_1(sK1,k9_relat_1(sF19,k3_pua2mss1(sK3))),
inference(superposition,[],[f2780,f22756]) ).
fof(f22859,plain,
sF16 = sF17,
inference(superposition,[],[f2756,f22837]) ).
fof(f22866,plain,
$false,
inference(forward_subsumption_resolution,[],[f22859,f193]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU427+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.15/0.42 % Computer : n009.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 28 05:22:15 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.21/0.48 Running first-order model finding
% 0.21/0.48 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 24.12/4.02 % (2692925)Will run a generic schedule for satisfiability detection.
% 24.12/4.02 % (2692933)dis+10_1_sil=32000:sp=arity:random_seed=487709795:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 24.12/4.02 % (2692931)% WARNING: option uhcvi not known.
% 24.12/4.02 % (2692935)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=634018620:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 24.12/4.02 % (2692932)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1976805528:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 24.12/4.02 % (2692931)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1836166900:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 24.12/4.02 % (2692934)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2493467730:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 24.12/4.02 % (2692930)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2854706836_2999 on theBenchmark for (2999ds/0Mi)
% 24.12/4.02 % (2692936)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1674570493:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 24.12/4.02 % TRYING [1]
% 24.12/4.02 % TRYING [2]
% 24.12/4.02 % TRYING [3]
% 24.12/4.02 % TRYING [4]
% 24.12/4.02 % (2692933)Instruction limit reached!
% 24.12/4.02 % (2692933)------------------------------
% 24.12/4.02 % (2692933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.12/4.02 % (2692933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.12/4.02 % (2692933)CaDiCaL version: 2.1.3
% 24.12/4.02 % (2692933)Termination reason: Instruction limit
% 24.12/4.02 % (2692933)Termination phase: Saturation
% 24.12/4.02 % (2692933)Time elapsed: 0.059 s
% 24.12/4.02 % (2692933)Peak memory usage: 13 MB
% 24.12/4.02 % (2692933)Instructions burned: 103 (million)
% 24.12/4.02 % (2692944)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4208298451:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 24.12/4.02 % TRYING [1]
% 24.12/4.02 % TRYING [2]
% 24.12/4.02 % TRYING [3]
% 24.12/4.02 % TRYING [4]
% 24.12/4.02 % (2692934)Instruction limit reached!
% 24.12/4.02 % (2692934)------------------------------
% 24.12/4.02 % (2692934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.12/4.02 % (2692934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.12/4.02 % (2692934)CaDiCaL version: 2.1.3
% 24.12/4.02 % (2692934)Termination reason: Instruction limit
% 24.12/4.02 % (2692934)Termination phase: Saturation
% 24.12/4.02 % (2692934)Time elapsed: 0.117 s
% 24.12/4.02 % (2692934)Peak memory usage: 13 MB
% 24.12/4.02 % (2692934)Instructions burned: 116 (million)
% 24.12/4.02 % (2692935)Instruction limit reached!
% 24.12/4.02 % (2692935)------------------------------
% 24.12/4.02 % (2692935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.12/4.02 % (2692935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.12/4.02 % (2692935)CaDiCaL version: 2.1.3
% 24.12/4.02 % (2692935)Termination reason: Instruction limit
% 24.12/4.02 % (2692935)Termination phase: Saturation
% 24.12/4.02 % (2692935)Time elapsed: 0.136 s
% 24.12/4.02 % (2692935)Peak memory usage: 13 MB
% 24.12/4.02 % (2692935)Instructions burned: 132 (million)
% 24.12/4.02 % (2692946)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2652369989:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 24.12/4.02 % TRYING [5]
% 24.12/4.02 % TRYING [5]
% 24.12/4.02 % (2692936)Instruction limit reached!
% 24.12/4.02 % (2692936)------------------------------
% 24.12/4.02 % (2692936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.12/4.02 % (2692936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.12/4.02 % (2692936)CaDiCaL version: 2.1.3
% 24.12/4.02 % (2692936)Termination reason: Instruction limit
% 24.12/4.02 % (2692936)Termination phase: Saturation
% 24.12/4.02 % (2692936)Time elapsed: 0.172 s
% 24.12/4.02 % (2692936)Peak memory usage: 13 MB
% 24.12/4.02 % (2692936)Instructions burned: 160 (million)
% 24.12/4.02 % (2692947)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=1615956705:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 24.12/4.02 % (2692949)ott-21_1_sil=16000:fs=off:random_seed=1166124858:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 24.12/4.02 % (2692946)Instruction limit reached!
% 24.12/4.02 % (2692946)------------------------------
% 24.12/4.02 % (2692946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692946)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692946)Termination reason: Instruction limit
% 14.61/5.41 % (2692946)Termination phase: Saturation
% 14.61/5.41 % (2692946)Time elapsed: 0.120 s
% 14.61/5.41 % (2692946)Peak memory usage: 13 MB
% 14.61/5.41 % (2692946)Instructions burned: 131 (million)
% 14.61/5.41 % (2692952)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=14367939:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 14.61/5.41 % (2692949)Instruction limit reached!
% 14.61/5.41 % (2692949)------------------------------
% 14.61/5.41 % (2692949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692949)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692949)Termination reason: Instruction limit
% 14.61/5.41 % (2692949)Termination phase: Saturation
% 14.61/5.41 % (2692949)Time elapsed: 0.125 s
% 14.61/5.41 % (2692949)Peak memory usage: 13 MB
% 14.61/5.41 % (2692949)Instructions burned: 180 (million)
% 14.61/5.41 % (2692944)Instruction limit reached!
% 14.61/5.41 % (2692944)------------------------------
% 14.61/5.41 % (2692944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692944)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692944)Termination reason: Instruction limit
% 14.61/5.41 % (2692944)Termination phase: Finite model building constraint generation
% 14.61/5.41 % (2692944)Time elapsed: 0.294 s
% 14.61/5.41 % (2692944)Peak memory usage: 41 MB
% 14.61/5.41 % (2692944)Instructions burned: 715 (million)
% 14.61/5.41 % (2692954)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1994550060:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 14.61/5.41 % TRYING [1]
% 14.61/5.41 % TRYING [2]
% 14.61/5.41 % TRYING [3]
% 14.61/5.41 % (2692956)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=907404298:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 14.61/5.41 % TRYING [4]
% 14.61/5.41 % TRYING [6]
% 14.61/5.41 % (2692947)Instruction limit reached!
% 14.61/5.41 % (2692947)------------------------------
% 14.61/5.41 % (2692947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692947)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692947)Termination reason: Instruction limit
% 14.61/5.41 % (2692947)Termination phase: Saturation
% 14.61/5.41 % (2692947)Time elapsed: 0.627 s
% 14.61/5.41 % (2692947)Peak memory usage: 16 MB
% 14.61/5.41 % (2692947)Instructions burned: 684 (million)
% 14.61/5.41 % (2692958)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2008572279:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 14.61/5.41 % (2692952)Instruction limit reached!
% 14.61/5.41 % (2692952)------------------------------
% 14.61/5.41 % (2692952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692952)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692952)Termination reason: Instruction limit
% 14.61/5.41 % (2692952)Termination phase: Saturation
% 14.61/5.41 % (2692952)Time elapsed: 0.532 s
% 14.61/5.41 % (2692952)Peak memory usage: 15 MB
% 14.61/5.41 % (2692952)Instructions burned: 477 (million)
% 14.61/5.41 % TRYING [5]
% 14.61/5.41 % (2692960)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=921783623:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 14.61/5.41 % (2692954)Instruction limit reached!
% 14.61/5.41 % (2692954)------------------------------
% 14.61/5.41 % (2692954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692954)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692954)Termination reason: Instruction limit
% 14.61/5.41 % (2692954)Termination phase: Finite model building constraint generation
% 14.61/5.41 % (2692954)Time elapsed: 0.581 s
% 14.61/5.41 % (2692954)Peak memory usage: 22 MB
% 14.61/5.41 % (2692954)Instructions burned: 865 (million)
% 14.61/5.41 % (2692962)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2711053921:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 14.61/5.41 % (2692956)Instruction limit reached!
% 14.61/5.41 % (2692956)------------------------------
% 14.61/5.41 % (2692956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692956)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692956)Termination reason: Instruction limit
% 14.61/5.41 % (2692956)Termination phase: Saturation
% 14.61/5.41 % (2692956)Time elapsed: 0.677 s
% 14.61/5.41 % (2692956)Peak memory usage: 26 MB
% 14.61/5.41 % (2692956)Instructions burned: 1180 (million)
% 14.61/5.41 % (2692964)fmb+10_1_sil=64000:random_seed=2737504737:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 14.61/5.41 % TRYING [1]
% 14.61/5.41 % TRYING [2]
% 14.61/5.41 % TRYING [3]
% 14.61/5.41 % TRYING [4]
% 14.61/5.41 % TRYING [5]
% 14.61/5.41 % (2692960)Instruction limit reached!
% 14.61/5.41 % (2692960)------------------------------
% 14.61/5.41 % (2692960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692960)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692960)Termination reason: Instruction limit
% 14.61/5.41 % (2692960)Termination phase: Saturation
% 14.61/5.41 % (2692960)Time elapsed: 0.650 s
% 14.61/5.41 % (2692960)Peak memory usage: 20 MB
% 14.61/5.41 % (2692960)Instructions burned: 692 (million)
% 14.61/5.41 % TRYING [7]
% 14.61/5.41 % (2692966)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3530709718:i=9515:nm=5_2983 on theBenchmark for (2983ds/9515Mi)
% 14.61/5.41 % TRYING [20]
% 14.61/5.41 % (2692958)Instruction limit reached!
% 14.61/5.41 % (2692958)------------------------------
% 14.61/5.41 % (2692958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692958)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692958)Termination reason: Instruction limit
% 14.61/5.41 % (2692958)Termination phase: Finite model building constraint generation
% 14.61/5.41 % (2692958)Time elapsed: 0.758 s
% 14.61/5.41 % (2692958)Peak memory usage: 108 MB
% 14.61/5.41 % (2692958)Instructions burned: 890 (million)
% 14.61/5.41 % (2692968)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3371822438:fmbsr=1.7:i=920_2983 on theBenchmark for (2983ds/920Mi)
% 14.61/5.41 % TRYING [8]
% 14.61/5.41 % (2692962)Instruction limit reached!
% 14.61/5.41 % (2692962)------------------------------
% 14.61/5.41 % (2692962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692962)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692962)Termination reason: Instruction limit
% 14.61/5.41 % (2692962)Termination phase: Saturation
% 14.61/5.41 % (2692962)Time elapsed: 0.901 s
% 14.61/5.41 % (2692962)Peak memory usage: 18 MB
% 14.61/5.41 % (2692962)Instructions burned: 880 (million)
% 14.61/5.41 % (2692970)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=248650707:i=5131_2980 on theBenchmark for (2980ds/5131Mi)
% 14.61/5.41 % TRYING [6]
% 14.61/5.41 % (2692968)Instruction limit reached!
% 14.61/5.41 % (2692968)------------------------------
% 14.61/5.41 % (2692968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692968)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692968)Termination reason: Instruction limit
% 14.61/5.41 % (2692968)Termination phase: Finite model building constraint generation
% 14.61/5.41 % (2692968)Time elapsed: 0.518 s
% 14.61/5.41 % (2692968)Peak memory usage: 63 MB
% 14.61/5.41 % (2692968)Instructions burned: 920 (million)
% 14.61/5.41 % (2692972)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3284175842:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi)
% 14.61/5.41 % (2692972)Instruction limit reached!
% 14.61/5.41 % (2692972)------------------------------
% 14.61/5.41 % (2692972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692972)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692972)Termination reason: Instruction limit
% 14.61/5.41 % (2692972)Termination phase: Saturation
% 14.61/5.41 % (2692972)Time elapsed: 1.196 s
% 14.61/5.41 % (2692972)Peak memory usage: 22 MB
% 14.61/5.41 % (2692972)Instructions burned: 1472 (million)
% 14.61/5.41 % (2692974)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1886968331:i=6324_2965 on theBenchmark for (2965ds/6324Mi)
% 14.61/5.41 % (2692974)Cannot represent all propositional literals internally
% 14.61/5.41 % (2692974)Refutation not found, incomplete strategy
% 14.61/5.41 % (2692974)------------------------------
% 14.61/5.41 % (2692974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692974)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692974)Termination reason: Refutation not found, incomplete strategy
% 14.61/5.41 % (2692974)Time elapsed: 0.002 s
% 14.61/5.41 % (2692974)Peak memory usage: 10 MB
% 14.61/5.41 % (2692974)Instructions burned: 8 (million)
% 14.61/5.41 % (2692974)------------------------------
% 14.61/5.41 % (2692974)------------------------------
% 14.61/5.41 % (2692976)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=927072817:fmbsr=2.30978:i=2174_2964 on theBenchmark for (2964ds/2174Mi)
% 14.61/5.41 % TRYING [16]
% 14.61/5.41 % (2692976)Instruction limit reached!
% 14.61/5.41 % (2692976)------------------------------
% 14.61/5.41 % (2692976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % TRYING [7]
% 14.61/5.41 % (2692976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692976)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692976)Termination reason: Instruction limit
% 14.61/5.41 % (2692976)Termination phase: Finite model building constraint generation
% 14.61/5.41 % (2692976)Time elapsed: 0.406 s
% 14.61/5.41 % (2692976)Peak memory usage: 132 MB
% 14.61/5.41 % (2692976)Instructions burned: 2178 (million)
% 14.61/5.41 % (2692978)ott-2_1_sil=16000:newcnf=on:random_seed=837245076:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2960 on theBenchmark for (2960ds/869Mi)
% 14.61/5.41 % (2692978)Instruction limit reached!
% 14.61/5.41 % (2692978)------------------------------
% 14.61/5.41 % (2692978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692978)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692978)Termination reason: Instruction limit
% 14.61/5.41 % (2692978)Termination phase: Saturation
% 14.61/5.41 % (2692978)Time elapsed: 0.282 s
% 14.61/5.41 % (2692978)Peak memory usage: 22 MB
% 14.61/5.41 % (2692978)Instructions burned: 872 (million)
% 14.61/5.41 % (2692980)ott+10_1_sil=32000:tgt=ground:random_seed=3921404828:i=5114:av=off_2957 on theBenchmark for (2957ds/5114Mi)
% 14.61/5.41 % (2692980) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2692925-2692980"...
% 14.61/5.41 % (2692980)...printing done.
% 14.61/5.41 % (2692980)Refutation found. Thanks to Tanya!
% 14.61/5.41 % SZS status Theorem for theBenchmark
% 14.61/5.41 % SZS output start Proof for theBenchmark
% See solution above
% 14.61/5.41 % (2692980)------------------------------
% 14.61/5.41 % (2692980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.61/5.41 % (2692980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/5.41 % (2692980)CaDiCaL version: 2.1.3
% 14.61/5.41 % (2692980)Termination reason: Refutation
% 14.61/5.41 % (2692980)Time elapsed: 0.566 s
% 14.61/5.41 % (2692980)Peak memory usage: 31 MB
% 14.61/5.41 % (2692980)Instructions burned: 1650 (million)
% 14.61/5.41 % (2692925)Success in time 4.925 s
% 14.61/5.41 % Vampire exiting
%------------------------------------------------------------------------------