%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : DAT436-2 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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 09:48:38 AM UTC 2026
% Result : Unsatisfiable 60.37s 12.16s
% Output : Refutation 60.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 20
% Syntax : Number of formulae : 100 ( 100 unt; 0 def)
% Number of atoms : 100 ( 99 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 11 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-4 aty)
% Number of variables : 202 ( 202 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
eq(zero,zero) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule1) ).
fof(f2,axiom,
! [X0] : eq(zero,s(X0)) = false,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule2) ).
fof(f3,axiom,
! [X0] : eq(s(X0),zero) = false,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule3) ).
fof(f4,plain,
! [X0] : false = eq(s(X0),zero),
inference(reorient_equations,[],[f3]) ).
fof(f5,axiom,
! [X0,X1] : eq(s(X0),s(X1)) = eq(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule4) ).
fof(f6,axiom,
! [X0] : le(zero,X0) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule5) ).
fof(f7,plain,
! [X0] : true = le(zero,X0),
inference(reorient_equations,[],[f6]) ).
fof(f8,axiom,
! [X0] : le(s(X0),zero) = false,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule6) ).
fof(f9,plain,
! [X0] : false = le(s(X0),zero),
inference(reorient_equations,[],[f8]) ).
fof(f10,axiom,
! [X0,X1] : le(s(X0),s(X1)) = le(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule7) ).
fof(f11,axiom,
min(cons(zero,nil)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule8) ).
fof(f12,plain,
zero = min(cons(zero,nil)),
inference(reorient_equations,[],[f11]) ).
fof(f13,axiom,
! [X0] : min(cons(s(X0),nil)) = s(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule9) ).
fof(f14,plain,
! [X0] : s(X0) = min(cons(s(X0),nil)),
inference(reorient_equations,[],[f13]) ).
fof(f15,axiom,
! [X2,X0,X1] : min(cons(X0,cons(X1,X2))) = ifmin(le(X0,X1),cons(X0,cons(X1,X2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule10) ).
fof(f16,axiom,
! [X2,X0,X1] : ifmin(true,cons(X0,cons(X1,X2))) = min(cons(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule11) ).
fof(f17,axiom,
! [X2,X0,X1] : ifmin(false,cons(X0,cons(X1,X2))) = min(cons(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule12) ).
fof(f20,axiom,
! [X2,X3,X0,X1] : replace(X0,X1,cons(X2,X3)) = ifrepl(eq(X0,X2),X0,X1,cons(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule14) ).
fof(f21,axiom,
! [X2,X3,X0,X1] : ifrepl(true,X0,X1,cons(X2,X3)) = cons(X1,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule15) ).
fof(f22,axiom,
! [X2,X3,X0,X1] : ifrepl(false,X0,X1,cons(X2,X3)) = cons(X2,replace(X0,X1,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule16) ).
fof(f23,axiom,
selsort(nil) = nil,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule17) ).
fof(f24,plain,
nil = selsort(nil),
inference(reorient_equations,[],[f23]) ).
fof(f25,axiom,
! [X0,X1] : selsort(cons(X0,X1)) = ifselsort(eq(X0,min(cons(X0,X1))),cons(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule18) ).
fof(f26,axiom,
! [X0,X1] : ifselsort(true,cons(X0,X1)) = cons(X0,selsort(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule19) ).
fof(f27,axiom,
! [X0,X1] : ifselsort(false,cons(X0,X1)) = cons(min(cons(X0,X1)),selsort(replace(min(cons(X0,X1)),X0,X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule20) ).
fof(f28,negated_conjecture,
! [X0] : selsort(cons(X0,cons(s(zero),cons(s(s(zero)),cons(s(s(s(s(zero)))),cons(zero,nil)))))) != cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f29,plain,
! [X0] : eq(zero,zero) = le(zero,X0),
inference(forward_demodulation,[],[f7,f1]) ).
fof(f64,plain,
! [X0,X1] : cons(X0,selsort(X1)) = ifselsort(eq(zero,zero),cons(X0,X1)),
inference(forward_demodulation,[],[f26,f1]) ).
fof(f65,plain,
! [X2,X3,X0,X1] : cons(X1,X3) = ifrepl(eq(zero,zero),X0,X1,cons(X2,X3)),
inference(forward_demodulation,[],[f21,f1]) ).
fof(f66,plain,
! [X2,X0,X1] : min(cons(X0,X2)) = ifmin(eq(zero,zero),cons(X0,cons(X1,X2))),
inference(forward_demodulation,[],[f16,f1]) ).
fof(f72,plain,
! [X0] : selsort(cons(s(X0),nil)) = ifselsort(eq(s(X0),s(X0)),cons(s(X0),nil)),
inference(superposition,[],[f25,f14]) ).
fof(f73,plain,
! [X0] : selsort(cons(s(X0),nil)) = ifselsort(eq(X0,X0),cons(s(X0),nil)),
inference(forward_demodulation,[],[f72,f5]) ).
fof(f76,plain,
! [X0] : selsort(cons(s(s(X0)),nil)) = ifselsort(eq(X0,X0),cons(s(s(X0)),nil)),
inference(superposition,[],[f73,f5]) ).
fof(f89,plain,
! [X0,X1] : min(cons(s(X0),cons(zero,X1))) = ifmin(false,cons(s(X0),cons(zero,X1))),
inference(superposition,[],[f15,f9]) ).
fof(f90,plain,
! [X2,X0,X1] : min(cons(s(X0),cons(s(X1),X2))) = ifmin(le(X0,X1),cons(s(X0),cons(s(X1),X2))),
inference(superposition,[],[f15,f10]) ).
fof(f93,plain,
! [X0,X1] : min(cons(s(X0),cons(zero,X1))) = min(cons(zero,X1)),
inference(forward_demodulation,[],[f89,f17]) ).
fof(f99,plain,
! [X2,X0,X1] : replace(zero,X0,cons(s(X1),X2)) = ifrepl(false,zero,X0,cons(s(X1),X2)),
inference(superposition,[],[f20,f2]) ).
fof(f104,plain,
! [X2,X3,X0,X1] : replace(s(X0),X2,cons(s(X1),X3)) = ifrepl(eq(X0,X1),s(X0),X2,cons(s(X1),X3)),
inference(superposition,[],[f20,f5]) ).
fof(f105,plain,
! [X0,X1] : cons(X0,X1) = replace(zero,X0,cons(zero,X1)),
inference(superposition,[],[f20,f65]) ).
fof(f108,plain,
! [X2,X0,X1] : replace(zero,X0,cons(s(X1),X2)) = cons(s(X1),replace(zero,X0,X2)),
inference(forward_demodulation,[],[f99,f22]) ).
fof(f109,plain,
! [X0] : selsort(cons(s(s(s(X0))),nil)) = ifselsort(eq(X0,X0),cons(s(s(s(X0))),nil)),
inference(superposition,[],[f76,f5]) ).
fof(f126,plain,
! [X0] : selsort(cons(s(s(s(s(X0)))),nil)) = ifselsort(eq(X0,X0),cons(s(s(s(s(X0)))),nil)),
inference(superposition,[],[f109,f5]) ).
fof(f131,plain,
! [X2,X0,X1] : cons(min(cons(X1,X2)),selsort(replace(min(cons(X1,X2)),X1,X2))) = ifselsort(eq(s(X0),zero),cons(X1,X2)),
inference(superposition,[],[f27,f4]) ).
fof(f142,plain,
! [X0,X1] : min(cons(s(s(X0)),cons(s(zero),X1))) = ifmin(false,cons(s(s(X0)),cons(s(zero),X1))),
inference(superposition,[],[f90,f9]) ).
fof(f143,plain,
! [X2,X0,X1] : min(cons(s(s(X0)),cons(s(s(X1)),X2))) = ifmin(le(X0,X1),cons(s(s(X0)),cons(s(s(X1)),X2))),
inference(superposition,[],[f90,f10]) ).
fof(f144,plain,
! [X0,X1] : min(cons(s(zero),cons(s(X0),X1))) = ifmin(eq(zero,zero),cons(s(zero),cons(s(X0),X1))),
inference(superposition,[],[f90,f29]) ).
fof(f145,plain,
! [X0,X1] : min(cons(s(zero),cons(s(X0),X1))) = min(cons(s(zero),X1)),
inference(forward_demodulation,[],[f144,f66]) ).
fof(f146,plain,
! [X0,X1] : min(cons(s(s(X0)),cons(s(zero),X1))) = min(cons(s(zero),X1)),
inference(forward_demodulation,[],[f142,f17]) ).
fof(f147,plain,
! [X0,X1] : selsort(cons(s(zero),cons(s(X1),X0))) = ifselsort(eq(s(zero),min(cons(s(zero),X0))),cons(s(zero),cons(s(X1),X0))),
inference(superposition,[],[f25,f145]) ).
fof(f148,plain,
! [X0,X1] : selsort(cons(s(s(X1)),cons(s(zero),X0))) = ifselsort(eq(s(s(X1)),min(cons(s(zero),X0))),cons(s(s(X1)),cons(s(zero),X0))),
inference(superposition,[],[f25,f146]) ).
fof(f157,plain,
! [X2,X3,X0,X1] : replace(s(s(X0)),X2,cons(s(s(X1)),X3)) = ifrepl(eq(X0,X1),s(s(X0)),X2,cons(s(s(X1)),X3)),
inference(superposition,[],[f104,f5]) ).
fof(f178,plain,
cons(s(s(s(s(zero)))),selsort(nil)) = selsort(cons(s(s(s(s(zero)))),nil)),
inference(superposition,[],[f64,f126]) ).
fof(f179,plain,
cons(s(s(s(s(zero)))),nil) = selsort(cons(s(s(s(s(zero)))),nil)),
inference(forward_demodulation,[],[f178,f24]) ).
fof(f200,plain,
! [X2,X0,X1] : min(cons(s(s(s(X0))),cons(s(s(s(X1))),X2))) = ifmin(le(X0,X1),cons(s(s(s(X0))),cons(s(s(s(X1))),X2))),
inference(superposition,[],[f143,f10]) ).
fof(f201,plain,
! [X0,X1] : min(cons(s(s(zero)),cons(s(s(X0)),X1))) = ifmin(eq(zero,zero),cons(s(s(zero)),cons(s(s(X0)),X1))),
inference(superposition,[],[f143,f29]) ).
fof(f202,plain,
! [X0,X1] : min(cons(s(s(zero)),cons(s(s(X0)),X1))) = min(cons(s(s(zero)),X1)),
inference(forward_demodulation,[],[f201,f66]) ).
fof(f204,plain,
! [X0,X1] : selsort(cons(s(s(zero)),cons(s(s(X1)),X0))) = ifselsort(eq(s(s(zero)),min(cons(s(s(zero)),X0))),cons(s(s(zero)),cons(s(s(X1)),X0))),
inference(superposition,[],[f25,f202]) ).
fof(f214,plain,
! [X2,X3,X0,X1] : replace(s(s(s(X0))),X2,cons(s(s(s(X1))),X3)) = ifrepl(eq(X0,X1),s(s(s(X0))),X2,cons(s(s(s(X1))),X3)),
inference(superposition,[],[f157,f5]) ).
fof(f236,plain,
! [X2,X0,X1] : selsort(cons(s(zero),cons(s(X1),cons(s(X2),X0)))) = ifselsort(eq(s(zero),min(cons(s(zero),X0))),cons(s(zero),cons(s(X1),cons(s(X2),X0)))),
inference(superposition,[],[f147,f145]) ).
fof(f256,plain,
! [X2,X0,X1] : selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),X0)))) = ifselsort(eq(s(s(X1)),min(cons(s(zero),X0))),cons(s(s(X1)),cons(s(zero),cons(s(X2),X0)))),
inference(superposition,[],[f148,f145]) ).
fof(f262,plain,
! [X0,X1] : min(cons(s(s(s(s(X0)))),cons(s(s(s(zero))),X1))) = ifmin(false,cons(s(s(s(s(X0)))),cons(s(s(s(zero))),X1))),
inference(superposition,[],[f200,f9]) ).
fof(f266,plain,
! [X0,X1] : min(cons(s(s(s(s(X0)))),cons(s(s(s(zero))),X1))) = min(cons(s(s(s(zero))),X1)),
inference(forward_demodulation,[],[f262,f17]) ).
fof(f268,plain,
! [X0,X1] : selsort(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X0))) = ifselsort(eq(s(s(s(s(X1)))),min(cons(s(s(s(zero))),X0))),cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X0))),
inference(superposition,[],[f25,f266]) ).
fof(f278,plain,
! [X0,X1] : cons(X0,X1) = replace(s(s(s(zero))),X0,cons(s(s(s(zero))),X1)),
inference(superposition,[],[f214,f65]) ).
fof(f502,plain,
! [X2,X0,X1] : selsort(cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),X0)))) = ifselsort(eq(s(s(zero)),min(cons(s(s(zero)),X0))),cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),X0)))),
inference(superposition,[],[f204,f202]) ).
fof(f509,plain,
! [X2,X3,X0,X1] : selsort(cons(s(zero),cons(s(X1),cons(s(X2),cons(s(X3),X0))))) = ifselsort(eq(s(zero),min(cons(s(zero),X0))),cons(s(zero),cons(s(X1),cons(s(X2),cons(s(X3),X0))))),
inference(superposition,[],[f236,f145]) ).
fof(f1027,plain,
! [X2,X3,X0,X1] : selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),X0))))) = ifselsort(eq(s(s(X1)),min(cons(s(zero),X0))),cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),X0))))),
inference(superposition,[],[f256,f145]) ).
fof(f7130,plain,
! [X2,X0,X1] : selsort(cons(s(zero),cons(s(X0),cons(s(X1),cons(s(X2),nil))))) = ifselsort(eq(s(zero),s(zero)),cons(s(zero),cons(s(X0),cons(s(X1),cons(s(X2),nil))))),
inference(superposition,[],[f509,f14]) ).
fof(f7182,plain,
! [X2,X0,X1] : selsort(cons(s(zero),cons(s(X0),cons(s(X1),cons(s(X2),nil))))) = ifselsort(eq(zero,zero),cons(s(zero),cons(s(X0),cons(s(X1),cons(s(X2),nil))))),
inference(forward_demodulation,[],[f7130,f5]) ).
fof(f7187,plain,
! [X2,X0,X1] : selsort(cons(s(zero),cons(s(X0),cons(s(X1),cons(s(X2),nil))))) = cons(s(zero),selsort(cons(s(X0),cons(s(X1),cons(s(X2),nil))))),
inference(forward_demodulation,[],[f7182,f64]) ).
fof(f7460,plain,
! [X0,X1] : selsort(cons(s(s(zero)),cons(s(s(X0)),cons(s(s(X1)),nil)))) = ifselsort(eq(s(s(zero)),s(s(zero))),cons(s(s(zero)),cons(s(s(X0)),cons(s(s(X1)),nil)))),
inference(superposition,[],[f502,f14]) ).
fof(f7505,plain,
! [X0,X1] : selsort(cons(s(s(zero)),cons(s(s(X0)),cons(s(s(X1)),nil)))) = ifselsort(eq(s(zero),s(zero)),cons(s(s(zero)),cons(s(s(X0)),cons(s(s(X1)),nil)))),
inference(forward_demodulation,[],[f7460,f5]) ).
fof(f7510,plain,
! [X0,X1] : selsort(cons(s(s(zero)),cons(s(s(X0)),cons(s(s(X1)),nil)))) = ifselsort(eq(zero,zero),cons(s(s(zero)),cons(s(s(X0)),cons(s(s(X1)),nil)))),
inference(forward_demodulation,[],[f7505,f5]) ).
fof(f7511,plain,
! [X0,X1] : selsort(cons(s(s(zero)),cons(s(s(X0)),cons(s(s(X1)),nil)))) = cons(s(s(zero)),selsort(cons(s(s(X0)),cons(s(s(X1)),nil)))),
inference(forward_demodulation,[],[f7510,f64]) ).
fof(f10879,plain,
! [X0] : selsort(cons(s(s(s(s(X0)))),cons(s(s(s(zero))),nil))) = ifselsort(eq(s(s(s(s(X0)))),s(s(s(zero)))),cons(s(s(s(s(X0)))),cons(s(s(s(zero))),nil))),
inference(superposition,[],[f268,f14]) ).
fof(f10935,plain,
! [X0] : selsort(cons(s(s(s(s(X0)))),cons(s(s(s(zero))),nil))) = ifselsort(eq(s(s(s(X0))),s(s(zero))),cons(s(s(s(s(X0)))),cons(s(s(s(zero))),nil))),
inference(forward_demodulation,[],[f10879,f5]) ).
fof(f10937,plain,
! [X0] : selsort(cons(s(s(s(s(X0)))),cons(s(s(s(zero))),nil))) = ifselsort(eq(s(s(X0)),s(zero)),cons(s(s(s(s(X0)))),cons(s(s(s(zero))),nil))),
inference(forward_demodulation,[],[f10935,f5]) ).
fof(f10938,plain,
! [X0] : selsort(cons(s(s(s(s(X0)))),cons(s(s(s(zero))),nil))) = ifselsort(eq(s(X0),zero),cons(s(s(s(s(X0)))),cons(s(s(s(zero))),nil))),
inference(forward_demodulation,[],[f10937,f5]) ).
fof(f10939,plain,
! [X0] : selsort(cons(s(s(s(s(X0)))),cons(s(s(s(zero))),nil))) = cons(min(cons(s(s(s(s(X0)))),cons(s(s(s(zero))),nil))),selsort(replace(min(cons(s(s(s(s(X0)))),cons(s(s(s(zero))),nil))),s(s(s(s(X0)))),cons(s(s(s(zero))),nil)))),
inference(forward_demodulation,[],[f10938,f131]) ).
fof(f10940,plain,
! [X0] : selsort(cons(s(s(s(s(X0)))),cons(s(s(s(zero))),nil))) = cons(min(cons(s(s(s(zero))),nil)),selsort(replace(min(cons(s(s(s(zero))),nil)),s(s(s(s(X0)))),cons(s(s(s(zero))),nil)))),
inference(forward_demodulation,[],[f10939,f266]) ).
fof(f10941,plain,
! [X0] : selsort(cons(s(s(s(s(X0)))),cons(s(s(s(zero))),nil))) = cons(s(s(s(zero))),selsort(replace(s(s(s(zero))),s(s(s(s(X0)))),cons(s(s(s(zero))),nil)))),
inference(forward_demodulation,[],[f10940,f14]) ).
fof(f10942,plain,
! [X0] : selsort(cons(s(s(s(s(X0)))),cons(s(s(s(zero))),nil))) = cons(s(s(s(zero))),selsort(cons(s(s(s(s(X0)))),nil))),
inference(forward_demodulation,[],[f10941,f278]) ).
fof(f11883,plain,
! [X2,X3,X0,X1] : selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,X0)))))) = ifselsort(eq(s(s(X1)),min(cons(zero,X0))),cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,X0)))))),
inference(superposition,[],[f1027,f93]) ).
fof(f51706,plain,
! [X2,X0,X1] : selsort(cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))) = ifselsort(eq(s(s(X0)),zero),cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))),
inference(superposition,[],[f11883,f12]) ).
fof(f52130,plain,
! [X2,X0,X1] : selsort(cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))) = cons(min(cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))),selsort(replace(min(cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))),s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil))))))),
inference(forward_demodulation,[],[f51706,f131]) ).
fof(f52152,plain,
! [X2,X0,X1] : selsort(cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))) = cons(min(cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil))))),selsort(replace(min(cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil))))),s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil))))))),
inference(forward_demodulation,[],[f52130,f146]) ).
fof(f52159,plain,
! [X2,X0,X1] : selsort(cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))) = cons(min(cons(s(zero),cons(s(X2),cons(zero,nil)))),selsort(replace(min(cons(s(zero),cons(s(X2),cons(zero,nil)))),s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil))))))),
inference(forward_demodulation,[],[f52152,f145]) ).
fof(f52161,plain,
! [X2,X0,X1] : selsort(cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))) = cons(min(cons(s(zero),cons(zero,nil))),selsort(replace(min(cons(s(zero),cons(zero,nil))),s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil))))))),
inference(forward_demodulation,[],[f52159,f145]) ).
fof(f52162,plain,
! [X2,X0,X1] : selsort(cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))) = cons(min(cons(zero,nil)),selsort(replace(min(cons(zero,nil)),s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil))))))),
inference(forward_demodulation,[],[f52161,f93]) ).
fof(f52163,plain,
! [X2,X0,X1] : selsort(cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))) = cons(zero,selsort(replace(zero,s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil))))))),
inference(forward_demodulation,[],[f52162,f12]) ).
fof(f52164,plain,
! [X2,X0,X1] : selsort(cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))) = cons(zero,selsort(cons(s(zero),replace(zero,s(s(X0)),cons(s(X1),cons(s(X2),cons(zero,nil))))))),
inference(forward_demodulation,[],[f52163,f108]) ).
fof(f52165,plain,
! [X2,X0,X1] : selsort(cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))) = cons(zero,selsort(cons(s(zero),cons(s(X1),replace(zero,s(s(X0)),cons(s(X2),cons(zero,nil))))))),
inference(forward_demodulation,[],[f52164,f108]) ).
fof(f52166,plain,
! [X2,X0,X1] : selsort(cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))) = cons(zero,selsort(cons(s(zero),cons(s(X1),cons(s(X2),replace(zero,s(s(X0)),cons(zero,nil))))))),
inference(forward_demodulation,[],[f52165,f108]) ).
fof(f52167,plain,
! [X2,X0,X1] : selsort(cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))) = cons(zero,selsort(cons(s(zero),cons(s(X1),cons(s(X2),cons(s(s(X0)),nil)))))),
inference(forward_demodulation,[],[f52166,f105]) ).
fof(f52168,plain,
! [X2,X0,X1] : selsort(cons(s(s(X0)),cons(s(zero),cons(s(X1),cons(s(X2),cons(zero,nil)))))) = cons(zero,cons(s(zero),selsort(cons(s(X1),cons(s(X2),cons(s(s(X0)),nil)))))),
inference(forward_demodulation,[],[f52167,f7187]) ).
fof(f52178,plain,
! [X0] : cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))) != cons(zero,cons(s(zero),selsort(cons(s(s(zero)),cons(s(s(s(s(zero)))),cons(s(s(X0)),nil)))))),
inference(superposition,[],[f28,f52168]) ).
fof(f52275,plain,
! [X0] : cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))) != cons(zero,cons(s(zero),cons(s(s(zero)),selsort(cons(s(s(s(s(zero)))),cons(s(s(X0)),nil)))))),
inference(forward_demodulation,[],[f52178,f7511]) ).
fof(f52279,plain,
cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))) != cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),selsort(cons(s(s(s(s(zero)))),nil)))))),
inference(superposition,[],[f52275,f10942]) ).
fof(f52281,plain,
cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))) != cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))),
inference(forward_demodulation,[],[f52279,f179]) ).
fof(f52282,plain,
$false,
inference(trivial_inequality_removal,[],[f52281]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : DAT436-2 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.17 % Computer : n002.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Tue Sep 29 00:24:52 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 Running first-order model finding
% 0.10/0.19 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
% 14.88/2.37 % (936321)Will run a generic schedule for satisfiability detection.
% 14.88/2.37 % (936328)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3068104269:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.88/2.37 % (936327)% WARNING: option uhcvi not known.
% 14.88/2.37 % (936326)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3240336817_2999 on theBenchmark for (2999ds/0Mi)
% 14.88/2.37 % (936329)dis+10_1_sil=32000:sp=arity:random_seed=3868508021:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.88/2.37 % (936332)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1342513320:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.88/2.37 % (936330)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1048512502:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.88/2.37 % (936331)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=136422963:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.88/2.37 % (936327)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3556468061:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.88/2.37 % TRYING [1]
% 14.88/2.37 % TRYING [2]
% 14.88/2.37 % TRYING [3]
% 14.88/2.37 % TRYING [4]
% 14.88/2.37 % (936329)Instruction limit reached!
% 14.88/2.37 % (936329)------------------------------
% 14.88/2.37 % (936329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.88/2.37 % (936329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.37 % (936329)CaDiCaL version: 2.1.3
% 14.88/2.37 % (936329)Termination reason: Instruction limit
% 14.88/2.37 % (936329)Termination phase: Saturation
% 14.88/2.37 % (936329)Time elapsed: 0.056 s
% 14.88/2.37 % (936329)Peak memory usage: 12 MB
% 14.88/2.37 % (936329)Instructions burned: 103 (million)
% 14.88/2.37 % TRYING [5]
% 14.88/2.37 % (936330)Instruction limit reached!
% 14.88/2.37 % (936330)------------------------------
% 14.88/2.37 % (936330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.88/2.37 % (936330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.37 % (936330)CaDiCaL version: 2.1.3
% 14.88/2.37 % (936330)Termination reason: Instruction limit
% 14.88/2.37 % (936330)Termination phase: Saturation
% 14.88/2.37 % (936330)Time elapsed: 0.068 s
% 14.88/2.37 % (936330)Peak memory usage: 13 MB
% 14.88/2.37 % (936330)Instructions burned: 116 (million)
% 14.88/2.37 % (936331)Instruction limit reached!
% 14.88/2.37 % (936331)------------------------------
% 14.88/2.37 % (936331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.88/2.37 % (936331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.37 % (936331)CaDiCaL version: 2.1.3
% 14.88/2.37 % (936331)Termination reason: Instruction limit
% 14.88/2.37 % (936331)Termination phase: Saturation
% 14.88/2.37 % (936331)Time elapsed: 0.072 s
% 14.88/2.37 % (936331)Peak memory usage: 12 MB
% 14.88/2.37 % (936331)Instructions burned: 131 (million)
% 14.88/2.37 % (936340)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3135059918:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.88/2.37 % TRYING [1]
% 14.88/2.37 % TRYING [2]
% 14.88/2.37 % TRYING [3]
% 14.88/2.37 % (936341)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4257720072:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.88/2.37 % (936342)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=3345010222:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.88/2.37 % (936332)Instruction limit reached!
% 14.88/2.37 % (936332)------------------------------
% 14.88/2.37 % (936332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.88/2.37 % (936332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.37 % (936332)CaDiCaL version: 2.1.3
% 14.88/2.37 % (936332)Termination reason: Instruction limit
% 14.88/2.37 % (936332)Termination phase: Saturation
% 14.88/2.37 % (936332)Time elapsed: 0.093 s
% 14.88/2.37 % (936332)Peak memory usage: 12 MB
% 14.88/2.37 % (936332)Instructions burned: 160 (million)
% 14.88/2.37 % TRYING [4]
% 14.88/2.37 % (936346)ott-21_1_sil=16000:fs=off:random_seed=1896902576:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.88/2.37 % TRYING [5]
% 14.88/2.37 % (936341)Instruction limit reached!
% 14.88/2.37 % (936341)------------------------------
% 14.88/2.37 % (936341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.88/2.37 % (936341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.67/6.54 % (936341)CaDiCaL version: 2.1.3
% 44.67/6.54 % (936341)Termination reason: Instruction limit
% 44.67/6.54 % (936341)Termination phase: Saturation
% 44.67/6.54 % (936341)Time elapsed: 0.082 s
% 44.67/6.54 % (936341)Peak memory usage: 13 MB
% 44.67/6.54 % (936341)Instructions burned: 131 (million)
% 44.67/6.54 % (936348)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3517057447:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 44.67/6.54 % TRYING [6]
% 44.67/6.54 % (936346)Instruction limit reached!
% 44.67/6.54 % (936346)------------------------------
% 44.67/6.54 % (936346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.67/6.54 % (936346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.67/6.54 % (936346)CaDiCaL version: 2.1.3
% 44.67/6.54 % (936346)Termination reason: Instruction limit
% 44.67/6.54 % (936346)Termination phase: Saturation
% 44.67/6.54 % (936346)Time elapsed: 0.092 s
% 44.67/6.54 % (936346)Peak memory usage: 12 MB
% 44.67/6.54 % (936346)Instructions burned: 181 (million)
% 44.67/6.54 % (936350)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1019148167:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 44.67/6.54 % TRYING [1]
% 44.67/6.54 % TRYING [2]
% 44.67/6.54 % TRYING [3]
% 44.67/6.54 % TRYING [6]
% 44.67/6.54 % TRYING [4]
% 44.67/6.54 % (936340)Instruction limit reached!
% 44.67/6.54 % (936340)------------------------------
% 44.67/6.54 % (936340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.67/6.54 % (936340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.67/6.54 % (936340)CaDiCaL version: 2.1.3
% 44.67/6.54 % (936340)Termination reason: Instruction limit
% 44.67/6.54 % (936340)Termination phase: Finite model building constraint generation
% 44.67/6.54 % (936340)Time elapsed: 0.273 s
% 44.67/6.54 % (936340)Peak memory usage: 35 MB
% 44.67/6.54 % (936340)Instructions burned: 716 (million)
% 44.67/6.54 % TRYING [5]
% 44.67/6.54 % (936352)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=358913699:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 44.67/6.54 % (936342)Instruction limit reached!
% 44.67/6.54 % (936342)------------------------------
% 44.67/6.54 % (936342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.67/6.54 % (936342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.67/6.54 % (936342)CaDiCaL version: 2.1.3
% 44.67/6.54 % (936342)Termination reason: Instruction limit
% 44.67/6.54 % (936342)Termination phase: Saturation
% 44.67/6.54 % (936342)Time elapsed: 0.353 s
% 44.67/6.54 % (936342)Peak memory usage: 18 MB
% 44.67/6.54 % (936342)Instructions burned: 685 (million)
% 44.67/6.54 % (936348)Instruction limit reached!
% 44.67/6.54 % (936348)------------------------------
% 44.67/6.54 % (936348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.67/6.54 % (936348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.67/6.54 % (936348)CaDiCaL version: 2.1.3
% 44.67/6.54 % (936348)Termination reason: Instruction limit
% 44.67/6.54 % (936348)Termination phase: Saturation
% 44.67/6.54 % (936348)Time elapsed: 0.264 s
% 44.67/6.54 % (936348)Peak memory usage: 16 MB
% 44.67/6.54 % (936348)Instructions burned: 478 (million)
% 44.67/6.54 % (936354)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=85930766:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 44.67/6.54 % (936355)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=2190966132:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 44.67/6.54 % TRYING [7]
% 44.67/6.54 % (936350)Instruction limit reached!
% 44.67/6.54 % (936350)------------------------------
% 44.67/6.54 % (936350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.67/6.54 % (936350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.67/6.54 % (936350)CaDiCaL version: 2.1.3
% 44.67/6.54 % (936350)Termination reason: Instruction limit
% 44.67/6.54 % (936350)Termination phase: Finite model building SAT solving
% 44.67/6.54 % (936350)Time elapsed: 0.339 s
% 44.67/6.54 % (936350)Peak memory usage: 26 MB
% 44.67/6.54 % (936350)Instructions burned: 867 (million)
% 44.67/6.54 % (936358)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1192825455:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 44.67/6.54 % TRYING [14]
% 44.67/6.54 % (936354)Instruction limit reached!
% 44.67/6.54 % (936354)------------------------------
% 44.67/6.54 % (936354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936354)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936354)Termination reason: Instruction limit
% 60.37/12.16 % (936354)Termination phase: Finite model building constraint generation
% 60.37/12.16 % (936354)Time elapsed: 0.403 s
% 60.37/12.16 % (936354)Peak memory usage: 105 MB
% 60.37/12.16 % (936354)Instructions burned: 891 (million)
% 60.37/12.16 % (936360)fmb+10_1_sil=64000:random_seed=854931082:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 60.37/12.16 % (936355)Instruction limit reached!
% 60.37/12.16 % (936355)------------------------------
% 60.37/12.16 % (936355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936355)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936355)Termination reason: Instruction limit
% 60.37/12.16 % (936355)Termination phase: Saturation
% 60.37/12.16 % (936355)Time elapsed: 0.429 s
% 60.37/12.16 % (936355)Peak memory usage: 22 MB
% 60.37/12.16 % (936355)Instructions burned: 695 (million)
% 60.37/12.16 % TRYING [1]
% 60.37/12.16 % TRYING [2]
% 60.37/12.16 % TRYING [3]
% 60.37/12.16 % (936362)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3450185301:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 60.37/12.16 % TRYING [20]
% 60.37/12.16 % TRYING [4]
% 60.37/12.16 % TRYING [5]
% 60.37/12.16 % (936358)Instruction limit reached!
% 60.37/12.16 % (936358)------------------------------
% 60.37/12.16 % (936358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936358)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936358)Termination reason: Instruction limit
% 60.37/12.16 % (936358)Termination phase: Saturation
% 60.37/12.16 % (936358)Time elapsed: 0.465 s
% 60.37/12.16 % (936358)Peak memory usage: 20 MB
% 60.37/12.16 % (936358)Instructions burned: 880 (million)
% 60.37/12.16 % (936352)Instruction limit reached!
% 60.37/12.16 % (936352)------------------------------
% 60.37/12.16 % (936352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936352)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936352)Termination reason: Instruction limit
% 60.37/12.16 % (936352)Termination phase: Saturation
% 60.37/12.16 % (936352)Time elapsed: 0.681 s
% 60.37/12.16 % (936352)Peak memory usage: 28 MB
% 60.37/12.16 % (936352)Instructions burned: 1180 (million)
% 60.37/12.16 % (936364)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3319827708:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 60.37/12.16 % (936365)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2507518462:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 60.37/12.16 % TRYING [8]
% 60.37/12.16 % TRYING [8]
% 60.37/12.16 % TRYING [6]
% 60.37/12.16 % (936364)Instruction limit reached!
% 60.37/12.16 % (936364)------------------------------
% 60.37/12.16 % (936364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936364)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936364)Termination reason: Instruction limit
% 60.37/12.16 % (936364)Termination phase: Finite model building constraint generation
% 60.37/12.16 % (936364)Time elapsed: 0.350 s
% 60.37/12.16 % (936364)Peak memory usage: 82 MB
% 60.37/12.16 % (936364)Instructions burned: 921 (million)
% 60.37/12.16 % (936368)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3135265873:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 60.37/12.16 % TRYING [7]
% 60.37/12.16 % (936368)Instruction limit reached!
% 60.37/12.16 % (936368)------------------------------
% 60.37/12.16 % (936368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936368)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936368)Termination reason: Instruction limit
% 60.37/12.16 % (936368)Termination phase: Saturation
% 60.37/12.16 % (936368)Time elapsed: 0.668 s
% 60.37/12.16 % (936368)Peak memory usage: 23 MB
% 60.37/12.16 % (936368)Instructions burned: 1474 (million)
% 60.37/12.16 % (936370)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2486830040:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 60.37/12.16 % (936370)Cannot represent all propositional literals internally
% 60.37/12.16 % (936370)Refutation not found, incomplete strategy
% 60.37/12.16 % (936370)------------------------------
% 60.37/12.16 % (936370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936370)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936370)Termination reason: Refutation not found, incomplete strategy
% 60.37/12.16 % (936370)Time elapsed: 0.004 s
% 60.37/12.16 % (936370)Peak memory usage: 10 MB
% 60.37/12.16 % (936370)Instructions burned: 6 (million)
% 60.37/12.16 % (936370)------------------------------
% 60.37/12.16 % (936370)------------------------------
% 60.37/12.16 % (936372)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2761911117:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 60.37/12.16 % TRYING [16]
% 60.37/12.16 % TRYING [9]
% 60.37/12.16 % (936372)Instruction limit reached!
% 60.37/12.16 % (936372)------------------------------
% 60.37/12.16 % (936372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936372)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936372)Termination reason: Instruction limit
% 60.37/12.16 % (936372)Termination phase: Finite model building constraint generation
% 60.37/12.16 % (936372)Time elapsed: 0.740 s
% 60.37/12.16 % (936372)Peak memory usage: 132 MB
% 60.37/12.16 % (936372)Instructions burned: 2175 (million)
% 60.37/12.16 % (936374)ott-2_1_sil=16000:newcnf=on:random_seed=2991564362:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2970 on theBenchmark for (2970ds/869Mi)
% 60.37/12.16 % (936374)Instruction limit reached!
% 60.37/12.16 % (936374)------------------------------
% 60.37/12.16 % (936374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936374)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936374)Termination reason: Instruction limit
% 60.37/12.16 % (936374)Termination phase: Saturation
% 60.37/12.16 % (936374)Time elapsed: 0.497 s
% 60.37/12.16 % (936374)Peak memory usage: 24 MB
% 60.37/12.16 % (936374)Instructions burned: 871 (million)
% 60.37/12.16 % (936376)ott+10_1_sil=32000:tgt=ground:random_seed=1240850370:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi)
% 60.37/12.16 % (936365)Instruction limit reached!
% 60.37/12.16 % (936365)------------------------------
% 60.37/12.16 % (936365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936365)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936365)Termination reason: Instruction limit
% 60.37/12.16 % (936365)Termination phase: Saturation
% 60.37/12.16 % (936365)Time elapsed: 2.642 s
% 60.37/12.16 % (936365)Peak memory usage: 54 MB
% 60.37/12.16 % (936365)Instructions burned: 5132 (million)
% 60.37/12.16 % (936378)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=37198114:i=54282_2962 on theBenchmark for (2962ds/54282Mi)
% 60.37/12.16 % TRYING [1]
% 60.37/12.16 % TRYING [2]
% 60.37/12.16 % TRYING [3]
% 60.37/12.16 % TRYING [4]
% 60.37/12.16 % TRYING [5]
% 60.37/12.16 % TRYING [8]
% 60.37/12.16 % TRYING [6]
% 60.37/12.16 % (936362)Instruction limit reached!
% 60.37/12.16 % (936362)------------------------------
% 60.37/12.16 % (936362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936362)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936362)Termination reason: Instruction limit
% 60.37/12.16 % (936362)Termination phase: Finite model building constraint generation
% 60.37/12.16 % (936362)Time elapsed: 3.367 s
% 60.37/12.16 % (936362)Peak memory usage: 607 MB
% 60.37/12.16 % (936362)Instructions burned: 9515 (million)
% 60.37/12.16 % TRYING [7]
% 60.37/12.16 % (936380)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=308627882:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi)
% 60.37/12.16 % TRYING [8]
% 60.37/12.16 % TRYING [10]
% 60.37/12.16 % (936380)Instruction limit reached!
% 60.37/12.16 % (936380)------------------------------
% 60.37/12.16 % (936380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936380)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936380)Termination reason: Instruction limit
% 60.37/12.16 % (936380)Termination phase: Saturation
% 60.37/12.16 % (936380)Time elapsed: 1.859 s
% 60.37/12.16 % (936380)Peak memory usage: 42 MB
% 60.37/12.16 % (936380)Instructions burned: 3512 (million)
% 60.37/12.16 % (936382)dis+21_1_sil=32000:sas=cadical:random_seed=1340538772:i=3773:amm=off_2937 on theBenchmark for (2937ds/3773Mi)
% 60.37/12.16 % (936376)Instruction limit reached!
% 60.37/12.16 % (936376)------------------------------
% 60.37/12.16 % (936376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936376)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936376)Termination reason: Instruction limit
% 60.37/12.16 % (936376)Termination phase: Saturation
% 60.37/12.16 % (936376)Time elapsed: 2.853 s
% 60.37/12.16 % (936376)Peak memory usage: 78 MB
% 60.37/12.16 % (936376)Instructions burned: 5115 (million)
% 60.37/12.16 % (936384)ott+11_1_sil=16000:gs=on:random_seed=1898244140:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2936 on theBenchmark for (2936ds/2251Mi)
% 60.37/12.16 % TRYING [9]
% 60.37/12.16 % (936384)Instruction limit reached!
% 60.37/12.16 % (936384)------------------------------
% 60.37/12.16 % (936384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936384)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936384)Termination reason: Instruction limit
% 60.37/12.16 % (936384)Termination phase: Saturation
% 60.37/12.16 % (936384)Time elapsed: 1.030 s
% 60.37/12.16 % (936384)Peak memory usage: 33 MB
% 60.37/12.16 % (936384)Instructions burned: 2252 (million)
% 60.37/12.16 % (936386)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2081035174:fmbsr=1.6:i=67534_2925 on theBenchmark for (2925ds/67534Mi)
% 60.37/12.16 % TRYING [7]
% 60.37/12.16 % (936382)Instruction limit reached!
% 60.37/12.16 % (936382)------------------------------
% 60.37/12.16 % (936382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936382)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936382)Termination reason: Instruction limit
% 60.37/12.16 % (936382)Termination phase: Saturation
% 60.37/12.16 % (936382)Time elapsed: 1.936 s
% 60.37/12.16 % (936382)Peak memory usage: 42 MB
% 60.37/12.16 % (936382)Instructions burned: 3774 (million)
% 60.37/12.16 % (936388)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3109269948:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2917 on theBenchmark for (2917ds/4591Mi)
% 60.37/12.16 % TRYING [9]
% 60.37/12.16 % TRYING [8]
% 60.37/12.16 % (936360)Instruction limit reached!
% 60.37/12.16 % (936360)------------------------------
% 60.37/12.16 % (936360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936360)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936360)Termination reason: Instruction limit
% 60.37/12.16 % (936360)Termination phase: Finite model building constraint generation
% 60.37/12.16 % (936360)Time elapsed: 8.404 s
% 60.37/12.16 % (936360)Peak memory usage: 206 MB
% 60.37/12.16 % (936360)Instructions burned: 22062 (million)
% 60.37/12.16 % (936390)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2502482682:i=29340_2906 on theBenchmark for (2906ds/29340Mi)
% 60.37/12.16 % TRYING [10]
% 60.37/12.16 % (936388)Instruction limit reached!
% 60.37/12.16 % (936388)------------------------------
% 60.37/12.16 % (936388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.16 % (936388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.16 % (936388)CaDiCaL version: 2.1.3
% 60.37/12.16 % (936388)Termination reason: Instruction limit
% 60.37/12.16 % (936388)Termination phase: Saturation
% 60.37/12.16 % (936388)Time elapsed: 2.213 s
% 60.37/12.16 % (936388)Peak memory usage: 53 MB
% 60.37/12.16 % (936388)Instructions burned: 4591 (million)
% 60.37/12.16 % (936392)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2504363550:i=5211_2895 on theBenchmark for (2895ds/5211Mi)
% 60.37/12.16 % (936390) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-936321-936390"...
% 60.37/12.16 % (936390)...printing done.
% 60.37/12.16 % (936390)Refutation found. Thanks to Tanya!
% 60.37/12.16 % SZS status Unsatisfiable for theBenchmark
% 60.37/12.16 % SZS output start Proof for theBenchmark
% See solution above
% 60.37/12.17 % (936390)------------------------------
% 60.37/12.17 % (936390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.37/12.17 % (936390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/12.17 % (936390)CaDiCaL version: 2.1.3
% 60.37/12.17 % (936390)Termination reason: Refutation
% 60.37/12.17 % (936390)Time elapsed: 2.479 s
% 60.37/12.17 % (936390)Peak memory usage: 36 MB
% 60.37/12.17 % (936390)Instructions burned: 4797 (million)
% 60.37/12.17 % (936321)Success in time 11.964 s
% 60.37/12.17 % Vampire exiting
%------------------------------------------------------------------------------