%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR049-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:42:18 AM UTC 2026
% Result : Unsatisfiable 59.76s 10.39s
% Output : Refutation 68.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 68
% Number of leaves : 38
% Syntax : Number of formulae : 200 ( 200 unt; 0 def)
% Number of atoms : 200 ( 199 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 1 ( 1 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 39 ( 39 usr; 35 con; 0-4 aty)
% Number of variables : 82 ( 82 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq4(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f2,axiom,
! [X2,X0,X1] : ifeq3(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom_001) ).
fof(f160,axiom,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_79) ).
fof(f161,plain,
true = genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
inference(reorient_equations,[],[f160]) ).
fof(f168,axiom,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_83) ).
fof(f169,plain,
true = genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
inference(reorient_equations,[],[f168]) ).
fof(f488,axiom,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_244) ).
fof(f489,plain,
true = genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
inference(reorient_equations,[],[f488]) ).
fof(f832,axiom,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_416) ).
fof(f833,plain,
true = genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
inference(reorient_equations,[],[f832]) ).
fof(f920,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_460) ).
fof(f921,plain,
true = genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(reorient_equations,[],[f920]) ).
fof(f1006,axiom,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_504) ).
fof(f1007,plain,
true = genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
inference(reorient_equations,[],[f1006]) ).
fof(f1136,axiom,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_569) ).
fof(f1137,plain,
true = genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
inference(reorient_equations,[],[f1136]) ).
fof(f1184,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_593) ).
fof(f1185,plain,
true = genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(reorient_equations,[],[f1184]) ).
fof(f1390,axiom,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_696) ).
fof(f1391,plain,
true = genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
inference(reorient_equations,[],[f1390]) ).
fof(f1482,axiom,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_742) ).
fof(f1483,plain,
true = genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
inference(reorient_equations,[],[f1482]) ).
fof(f1730,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_867) ).
fof(f1731,plain,
true = genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(reorient_equations,[],[f1730]) ).
fof(f2014,axiom,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1009) ).
fof(f2015,plain,
true = genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
inference(reorient_equations,[],[f2014]) ).
fof(f2142,axiom,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1073) ).
fof(f2143,plain,
true = genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
inference(reorient_equations,[],[f2142]) ).
fof(f2286,axiom,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1145) ).
fof(f2287,plain,
true = genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
inference(reorient_equations,[],[f2286]) ).
fof(f2356,axiom,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1180) ).
fof(f2357,plain,
true = genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
inference(reorient_equations,[],[f2356]) ).
fof(f2396,axiom,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1200) ).
fof(f2397,plain,
true = genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
inference(reorient_equations,[],[f2396]) ).
fof(f2492,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1248) ).
fof(f2493,plain,
true = disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(reorient_equations,[],[f2492]) ).
fof(f3098,axiom,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1553) ).
fof(f3099,plain,
true = genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
inference(reorient_equations,[],[f3098]) ).
fof(f3378,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1694) ).
fof(f3379,plain,
true = genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(reorient_equations,[],[f3378]) ).
fof(f3420,axiom,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1715) ).
fof(f3421,plain,
true = genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
inference(reorient_equations,[],[f3420]) ).
fof(f3820,axiom,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1917) ).
fof(f3821,plain,
true = genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
inference(reorient_equations,[],[f3820]) ).
fof(f3870,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1942) ).
fof(f3871,plain,
true = genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(reorient_equations,[],[f3870]) ).
fof(f4002,axiom,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2008) ).
fof(f4003,plain,
true = genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
inference(reorient_equations,[],[f4002]) ).
fof(f4030,axiom,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2022) ).
fof(f4031,plain,
true = genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
inference(reorient_equations,[],[f4030]) ).
fof(f4388,axiom,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2202) ).
fof(f4389,plain,
true = genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
inference(reorient_equations,[],[f4388]) ).
fof(f6004,axiom,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3013) ).
fof(f6005,plain,
true = genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
inference(reorient_equations,[],[f6004]) ).
fof(f6404,axiom,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3214) ).
fof(f6405,plain,
true = genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
inference(reorient_equations,[],[f6404]) ).
fof(f6480,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3253) ).
fof(f6481,plain,
true = genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(reorient_equations,[],[f6480]) ).
fof(f6846,axiom,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3436) ).
fof(f6847,plain,
true = genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
inference(reorient_equations,[],[f6846]) ).
fof(f7000,axiom,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3513) ).
fof(f7001,plain,
true = genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
inference(reorient_equations,[],[f7000]) ).
fof(f7232,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3629) ).
fof(f7233,plain,
true = genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(reorient_equations,[],[f7232]) ).
fof(f15028,axiom,
! [X0,X1] : ifeq4(disjointwith(X0,X1),true,disjointwith(X1,X0),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_7584) ).
fof(f15029,plain,
! [X0,X1] : true = ifeq4(disjointwith(X0,X1),true,disjointwith(X1,X0),true),
inference(reorient_equations,[],[f15028]) ).
fof(f15032,axiom,
! [X2,X0,X1] : ifeq4(disjointwith(X0,X1),true,ifeq4(genls(X2,X0),true,disjointwith(X2,X1),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_7586) ).
fof(f15033,plain,
! [X2,X0,X1] : true = ifeq4(disjointwith(X0,X1),true,ifeq4(genls(X2,X0),true,disjointwith(X2,X1),true),true),
inference(reorient_equations,[],[f15032]) ).
fof(f15836,axiom,
! [X2,X0,X1] : ifeq4(genls(X0,X1),true,ifeq4(genls(X2,X0),true,genls(X2,X1),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_7991) ).
fof(f15837,plain,
! [X2,X0,X1] : true = ifeq4(genls(X0,X1),true,ifeq4(genls(X2,X0),true,genls(X2,X1),true),true),
inference(reorient_equations,[],[f15836]) ).
fof(f16016,negated_conjecture,
ifeq3(disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),true,a,b) = b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query149_1) ).
fof(f16017,plain,
b = ifeq3(disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),true,a,b),
inference(reorient_equations,[],[f16016]) ).
fof(f16018,negated_conjecture,
a != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f16210,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_12_26919,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_13_26920,X0),true),true),
inference(superposition,[],[f15033,f1391]) ).
fof(f16211,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_9_26885,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_10_26886,X0),true),true),
inference(superposition,[],[f15033,f161]) ).
fof(f16212,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_8_26629,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_9_26885,X0),true),true),
inference(superposition,[],[f15033,f7001]) ).
fof(f16213,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_7_26628,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_8_26629,X0),true),true),
inference(superposition,[],[f15033,f169]) ).
fof(f16214,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_6_26627,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_7_26628,X0),true),true),
inference(superposition,[],[f15033,f3099]) ).
fof(f16215,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_14_26921,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_15_26925,X0),true),true),
inference(superposition,[],[f15033,f489]) ).
fof(f16216,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_13_26920,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_14_26921,X0),true),true),
inference(superposition,[],[f15033,f3821]) ).
fof(f16217,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_4_24578,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_5_24579,X0),true),true),
inference(superposition,[],[f15033,f2015]) ).
fof(f16218,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_10_92166,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_11_92230,X0),true),true),
inference(superposition,[],[f15033,f833]) ).
fof(f16219,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_9_92165,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_10_92166,X0),true),true),
inference(superposition,[],[f15033,f2287]) ).
fof(f16220,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_11_26887,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_12_26919,X0),true),true),
inference(superposition,[],[f15033,f1007]) ).
fof(f16221,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_10_26886,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_11_26887,X0),true),true),
inference(superposition,[],[f15033,f2143]) ).
fof(f16222,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_6_92162,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_7_92163,X0),true),true),
inference(superposition,[],[f15033,f1137]) ).
fof(f16223,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_13_92263,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_14_92264,X0),true),true),
inference(superposition,[],[f15033,f1483]) ).
fof(f16224,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_12_92262,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_13_92263,X0),true),true),
inference(superposition,[],[f15033,f4003]) ).
fof(f16226,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_7_92163,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_8_92164,X0),true),true),
inference(superposition,[],[f15033,f4031]) ).
fof(f16227,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_3_16386,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_4_24578,X0),true),true),
inference(superposition,[],[f15033,f6405]) ).
fof(f16228,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_8_92164,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_9_92165,X0),true),true),
inference(superposition,[],[f15033,f4389]) ).
fof(f16231,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_15_26925,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_16_26926,X0),true),true),
inference(superposition,[],[f15033,f2397]) ).
fof(f16232,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_5_24579,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_6_26627,X0),true),true),
inference(superposition,[],[f15033,f6005]) ).
fof(f16233,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_11_92230,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_12_92262,X0),true),true),
inference(superposition,[],[f15033,f6847]) ).
fof(f16237,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_11_92230,X0),true,disjointwith(c_tptpcol_12_92262,X0),true),
inference(forward_demodulation,[],[f16233,f1]) ).
fof(f16238,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_5_24579,X0),true,disjointwith(c_tptpcol_6_26627,X0),true),
inference(forward_demodulation,[],[f16232,f1]) ).
fof(f16239,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_15_26925,X0),true,disjointwith(c_tptpcol_16_26926,X0),true),
inference(forward_demodulation,[],[f16231,f1]) ).
fof(f16242,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_8_92164,X0),true,disjointwith(c_tptpcol_9_92165,X0),true),
inference(forward_demodulation,[],[f16228,f1]) ).
fof(f16243,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_3_16386,X0),true,disjointwith(c_tptpcol_4_24578,X0),true),
inference(forward_demodulation,[],[f16227,f1]) ).
fof(f16244,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_7_92163,X0),true,disjointwith(c_tptpcol_8_92164,X0),true),
inference(forward_demodulation,[],[f16226,f1]) ).
fof(f16246,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_12_92262,X0),true,disjointwith(c_tptpcol_13_92263,X0),true),
inference(forward_demodulation,[],[f16224,f1]) ).
fof(f16247,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_13_92263,X0),true,disjointwith(c_tptpcol_14_92264,X0),true),
inference(forward_demodulation,[],[f16223,f1]) ).
fof(f16248,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_6_92162,X0),true,disjointwith(c_tptpcol_7_92163,X0),true),
inference(forward_demodulation,[],[f16222,f1]) ).
fof(f16249,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_10_26886,X0),true,disjointwith(c_tptpcol_11_26887,X0),true),
inference(forward_demodulation,[],[f16221,f1]) ).
fof(f16250,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_11_26887,X0),true,disjointwith(c_tptpcol_12_26919,X0),true),
inference(forward_demodulation,[],[f16220,f1]) ).
fof(f16251,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_9_92165,X0),true,disjointwith(c_tptpcol_10_92166,X0),true),
inference(forward_demodulation,[],[f16219,f1]) ).
fof(f16252,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_10_92166,X0),true,disjointwith(c_tptpcol_11_92230,X0),true),
inference(forward_demodulation,[],[f16218,f1]) ).
fof(f16253,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_4_24578,X0),true,disjointwith(c_tptpcol_5_24579,X0),true),
inference(forward_demodulation,[],[f16217,f1]) ).
fof(f16254,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_13_26920,X0),true,disjointwith(c_tptpcol_14_26921,X0),true),
inference(forward_demodulation,[],[f16216,f1]) ).
fof(f16255,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_14_26921,X0),true,disjointwith(c_tptpcol_15_26925,X0),true),
inference(forward_demodulation,[],[f16215,f1]) ).
fof(f16256,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_6_26627,X0),true,disjointwith(c_tptpcol_7_26628,X0),true),
inference(forward_demodulation,[],[f16214,f1]) ).
fof(f16257,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_7_26628,X0),true,disjointwith(c_tptpcol_8_26629,X0),true),
inference(forward_demodulation,[],[f16213,f1]) ).
fof(f16258,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_8_26629,X0),true,disjointwith(c_tptpcol_9_26885,X0),true),
inference(forward_demodulation,[],[f16212,f1]) ).
fof(f16259,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_9_26885,X0),true,disjointwith(c_tptpcol_10_26886,X0),true),
inference(forward_demodulation,[],[f16211,f1]) ).
fof(f16260,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_12_26919,X0),true,disjointwith(c_tptpcol_13_26920,X0),true),
inference(forward_demodulation,[],[f16210,f1]) ).
fof(f16484,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_15_92268,X0),true,ifeq4(true,true,genls(c_tptpcol_16_92269,X0),true),true),
inference(superposition,[],[f15837,f2357]) ).
fof(f16518,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_15_92268,X0),true,genls(c_tptpcol_16_92269,X0),true),
inference(forward_demodulation,[],[f16484,f1]) ).
fof(f18121,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_4_90113,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_5_90114,X0),true),true),
inference(superposition,[],[f15033,f3871]) ).
fof(f18136,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_4_90113,X0),true,disjointwith(c_tptpcol_5_90114,X0),true),
inference(forward_demodulation,[],[f18121,f1]) ).
fof(f19957,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_5_90114,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_6_92162,X0),true),true),
inference(superposition,[],[f15033,f3379]) ).
fof(f19972,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_5_90114,X0),true,disjointwith(c_tptpcol_6_92162,X0),true),
inference(forward_demodulation,[],[f19957,f1]) ).
fof(f20063,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_3_81921,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_4_90113,X0),true),true),
inference(superposition,[],[f15033,f7233]) ).
fof(f20078,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_3_81921,X0),true,disjointwith(c_tptpcol_4_90113,X0),true),
inference(forward_demodulation,[],[f20063,f1]) ).
fof(f20847,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_1_1,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_2_2,X0),true),true),
inference(superposition,[],[f15033,f6481]) ).
fof(f20863,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_1_1,X0),true,disjointwith(c_tptpcol_2_2,X0),true),
inference(forward_demodulation,[],[f20847,f1]) ).
fof(f20867,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536),true),
inference(superposition,[],[f20863,f2493]) ).
fof(f20868,plain,
true = disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f20867,f1]) ).
fof(f21207,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_2_2,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_3_16386,X0),true),true),
inference(superposition,[],[f15033,f921]) ).
fof(f21223,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_2_2,X0),true,disjointwith(c_tptpcol_3_16386,X0),true),
inference(forward_demodulation,[],[f21207,f1]) ).
fof(f21227,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_3_16386,c_tptpcol_1_65536),true),
inference(superposition,[],[f21223,f20868]) ).
fof(f21228,plain,
true = disjointwith(c_tptpcol_3_16386,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f21227,f1]) ).
fof(f21230,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_4_24578,c_tptpcol_1_65536),true),
inference(superposition,[],[f16243,f21228]) ).
fof(f21248,plain,
true = disjointwith(c_tptpcol_4_24578,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f21230,f1]) ).
fof(f21266,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_5_24579,c_tptpcol_1_65536),true),
inference(superposition,[],[f16253,f21248]) ).
fof(f21282,plain,
true = disjointwith(c_tptpcol_5_24579,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f21266,f1]) ).
fof(f21298,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_6_26627,c_tptpcol_1_65536),true),
inference(superposition,[],[f16238,f21282]) ).
fof(f21315,plain,
true = disjointwith(c_tptpcol_6_26627,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f21298,f1]) ).
fof(f21317,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_7_26628,c_tptpcol_1_65536),true),
inference(superposition,[],[f16256,f21315]) ).
fof(f21332,plain,
true = disjointwith(c_tptpcol_7_26628,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f21317,f1]) ).
fof(f21333,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_8_26629,c_tptpcol_1_65536),true),
inference(superposition,[],[f16257,f21332]) ).
fof(f21349,plain,
true = disjointwith(c_tptpcol_8_26629,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f21333,f1]) ).
fof(f21351,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_9_26885,c_tptpcol_1_65536),true),
inference(superposition,[],[f16258,f21349]) ).
fof(f21366,plain,
true = disjointwith(c_tptpcol_9_26885,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f21351,f1]) ).
fof(f21367,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_10_26886,c_tptpcol_1_65536),true),
inference(superposition,[],[f16259,f21366]) ).
fof(f21383,plain,
true = disjointwith(c_tptpcol_10_26886,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f21367,f1]) ).
fof(f21385,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_11_26887,c_tptpcol_1_65536),true),
inference(superposition,[],[f16249,f21383]) ).
fof(f21400,plain,
true = disjointwith(c_tptpcol_11_26887,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f21385,f1]) ).
fof(f21401,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_12_26919,c_tptpcol_1_65536),true),
inference(superposition,[],[f16250,f21400]) ).
fof(f21417,plain,
true = disjointwith(c_tptpcol_12_26919,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f21401,f1]) ).
fof(f21419,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_13_26920,c_tptpcol_1_65536),true),
inference(superposition,[],[f16260,f21417]) ).
fof(f21434,plain,
true = disjointwith(c_tptpcol_13_26920,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f21419,f1]) ).
fof(f21435,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_14_26921,c_tptpcol_1_65536),true),
inference(superposition,[],[f16254,f21434]) ).
fof(f21451,plain,
true = disjointwith(c_tptpcol_14_26921,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f21435,f1]) ).
fof(f21453,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_26925,c_tptpcol_1_65536),true),
inference(superposition,[],[f16255,f21451]) ).
fof(f21468,plain,
true = disjointwith(c_tptpcol_15_26925,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f21453,f1]) ).
fof(f21471,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_16_26926,c_tptpcol_1_65536),true),
inference(superposition,[],[f16239,f21468]) ).
fof(f21487,plain,
true = disjointwith(c_tptpcol_16_26926,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f21471,f1]) ).
fof(f21492,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_1_65536,c_tptpcol_16_26926),true),
inference(superposition,[],[f15029,f21487]) ).
fof(f21502,plain,
true = disjointwith(c_tptpcol_1_65536,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f21492,f1]) ).
fof(f48599,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_2_65537,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_3_81921,X0),true),true),
inference(superposition,[],[f15033,f1185]) ).
fof(f48616,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_2_65537,X0),true,disjointwith(c_tptpcol_3_81921,X0),true),
inference(forward_demodulation,[],[f48599,f1]) ).
fof(f49277,plain,
true = ifeq4(true,true,genls(c_tptpcol_16_92269,c_tptpcol_14_92264),true),
inference(superposition,[],[f16518,f3421]) ).
fof(f49283,plain,
true = genls(c_tptpcol_16_92269,c_tptpcol_14_92264),
inference(forward_demodulation,[],[f49277,f1]) ).
fof(f49287,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_14_92264,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_16_92269,X0),true),true),
inference(superposition,[],[f15033,f49283]) ).
fof(f49304,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_14_92264,X0),true,disjointwith(c_tptpcol_16_92269,X0),true),
inference(forward_demodulation,[],[f49287,f1]) ).
fof(f50145,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_1_65536,X0),true,ifeq4(true,true,disjointwith(c_tptpcol_2_65537,X0),true),true),
inference(superposition,[],[f15033,f1731]) ).
fof(f50162,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_1_65536,X0),true,disjointwith(c_tptpcol_2_65537,X0),true),
inference(forward_demodulation,[],[f50145,f1]) ).
fof(f50189,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_2_65537,c_tptpcol_16_26926),true),
inference(superposition,[],[f50162,f21502]) ).
fof(f50198,plain,
true = disjointwith(c_tptpcol_2_65537,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f50189,f1]) ).
fof(f55224,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_3_81921,c_tptpcol_16_26926),true),
inference(superposition,[],[f48616,f50198]) ).
fof(f55244,plain,
true = disjointwith(c_tptpcol_3_81921,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f55224,f1]) ).
fof(f55562,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_4_90113,c_tptpcol_16_26926),true),
inference(superposition,[],[f20078,f55244]) ).
fof(f55579,plain,
true = disjointwith(c_tptpcol_4_90113,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f55562,f1]) ).
fof(f55582,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_5_90114,c_tptpcol_16_26926),true),
inference(superposition,[],[f18136,f55579]) ).
fof(f55599,plain,
true = disjointwith(c_tptpcol_5_90114,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f55582,f1]) ).
fof(f55601,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_6_92162,c_tptpcol_16_26926),true),
inference(superposition,[],[f19972,f55599]) ).
fof(f55619,plain,
true = disjointwith(c_tptpcol_6_92162,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f55601,f1]) ).
fof(f55623,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_7_92163,c_tptpcol_16_26926),true),
inference(superposition,[],[f16248,f55619]) ).
fof(f55640,plain,
true = disjointwith(c_tptpcol_7_92163,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f55623,f1]) ).
fof(f55643,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_8_92164,c_tptpcol_16_26926),true),
inference(superposition,[],[f16244,f55640]) ).
fof(f55661,plain,
true = disjointwith(c_tptpcol_8_92164,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f55643,f1]) ).
fof(f55664,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_9_92165,c_tptpcol_16_26926),true),
inference(superposition,[],[f16242,f55661]) ).
fof(f55681,plain,
true = disjointwith(c_tptpcol_9_92165,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f55664,f1]) ).
fof(f55683,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_10_92166,c_tptpcol_16_26926),true),
inference(superposition,[],[f16251,f55681]) ).
fof(f55701,plain,
true = disjointwith(c_tptpcol_10_92166,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f55683,f1]) ).
fof(f55703,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_11_92230,c_tptpcol_16_26926),true),
inference(superposition,[],[f16252,f55701]) ).
fof(f55721,plain,
true = disjointwith(c_tptpcol_11_92230,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f55703,f1]) ).
fof(f55723,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_12_92262,c_tptpcol_16_26926),true),
inference(superposition,[],[f16237,f55721]) ).
fof(f55741,plain,
true = disjointwith(c_tptpcol_12_92262,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f55723,f1]) ).
fof(f55744,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_13_92263,c_tptpcol_16_26926),true),
inference(superposition,[],[f16246,f55741]) ).
fof(f55761,plain,
true = disjointwith(c_tptpcol_13_92263,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f55744,f1]) ).
fof(f55764,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_14_92264,c_tptpcol_16_26926),true),
inference(superposition,[],[f16247,f55761]) ).
fof(f55781,plain,
true = disjointwith(c_tptpcol_14_92264,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f55764,f1]) ).
fof(f55782,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_16_92269,c_tptpcol_16_26926),true),
inference(superposition,[],[f49304,f55781]) ).
fof(f55803,plain,
true = disjointwith(c_tptpcol_16_92269,c_tptpcol_16_26926),
inference(forward_demodulation,[],[f55782,f1]) ).
fof(f55829,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),true),
inference(superposition,[],[f15029,f55803]) ).
fof(f55840,plain,
true = disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),
inference(forward_demodulation,[],[f55829,f1]) ).
fof(f55843,plain,
b = ifeq3(true,true,a,b),
inference(backward_demodulation,[],[f16017,f55840]) ).
fof(f55844,plain,
a = b,
inference(forward_demodulation,[],[f55843,f2]) ).
fof(f55845,plain,
$false,
inference(forward_subsumption_resolution,[],[f55844,f16018]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR049-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n016.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 22:22:19 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 59.76/10.39 % (4102450)Detected a unit-equality problem, will run specialized UEQ schedule.
% 59.76/10.39 % (4102456)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1116841030:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/130792Mi)
% 59.76/10.39 % (4102459)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1867130092:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2997 on theBenchmark for (2997ds/181Mi)
% 59.76/10.39 % (4102460)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3613159703:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2997 on theBenchmark for (2997ds/257Mi)
% 59.76/10.39 % (4102455)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=801761252:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/138329Mi)
% 59.76/10.39 % (4102457)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2584398391:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2997 on theBenchmark for (2997ds/130716Mi)
% 59.76/10.39 % (4102461)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3801821802:i=1187:sd=4:av=off:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/1187Mi)
% 59.76/10.39 % (4102458)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3651188705:i=136:bd=preordered:ins=2:av=off_2997 on theBenchmark for (2997ds/136Mi)
% 59.76/10.39 % (4102459)Instruction limit reached!
% 59.76/10.39 % (4102459)------------------------------
% 59.76/10.39 % (4102459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.76/10.39 % (4102459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.76/10.39 % (4102459)CaDiCaL version: 2.1.3
% 59.76/10.39 % (4102459)Termination reason: Instruction limit
% 59.76/10.39 % (4102459)Termination phase: Twee Goal Transformation
% 59.76/10.39 % (4102459)Time elapsed: 0.082 s
% 59.76/10.39 % (4102459)Peak memory usage: 94 MB
% 59.76/10.39 % (4102459)Instructions burned: 181 (million)
% 59.76/10.39 % (4102458)Instruction limit reached!
% 59.76/10.39 % (4102458)------------------------------
% 59.76/10.39 % (4102458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.76/10.39 % (4102458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.76/10.39 % (4102458)CaDiCaL version: 2.1.3
% 59.76/10.39 % (4102458)Termination reason: Instruction limit
% 59.76/10.39 % (4102458)Termination phase: Saturation
% 59.76/10.39 % (4102458)Time elapsed: 0.115 s
% 59.76/10.39 % (4102458)Peak memory usage: 95 MB
% 59.76/10.39 % (4102458)Instructions burned: 137 (million)
% 59.76/10.39 % (4102460)Instruction limit reached!
% 59.76/10.39 % (4102460)------------------------------
% 59.76/10.39 % (4102460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.76/10.39 % (4102460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.76/10.39 % (4102460)CaDiCaL version: 2.1.3
% 59.76/10.39 % (4102460)Termination reason: Instruction limit
% 59.76/10.39 % (4102460)Termination phase: Saturation
% 59.76/10.39 % (4102460)Time elapsed: 0.152 s
% 59.76/10.39 % (4102460)Peak memory usage: 100 MB
% 59.76/10.39 % (4102460)Instructions burned: 257 (million)
% 59.76/10.39 % (4102469)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=534742550:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2995 on theBenchmark for (2995ds/2051Mi)
% 59.76/10.39 % (4102471)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2410458739:i=215:ep=RSTC_2994 on theBenchmark for (2994ds/215Mi)
% 59.76/10.39 % (4102470)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3272658477:i=4948:ss=axioms:sgt=16_2994 on theBenchmark for (2994ds/4948Mi)
% 59.76/10.39 % (4102471)Instruction limit reached!
% 59.76/10.39 % (4102471)------------------------------
% 59.76/10.39 % (4102471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.76/10.39 % (4102471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.76/10.39 % (4102471)CaDiCaL version: 2.1.3
% 59.76/10.39 % (4102471)Termination reason: Instruction limit
% 59.76/10.39 % (4102471)Termination phase: Saturation
% 59.76/10.39 % (4102471)Time elapsed: 0.110 s
% 59.76/10.39 % (4102471)Peak memory usage: 100 MB
% 59.76/10.39 % (4102471)Instructions burned: 216 (million)
% 59.76/10.39 % (4102475)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=2162203265:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2991 on theBenchmark for (2991ds/317Mi)
% 59.76/10.39 % (4102461)Instruction limit reached!
% 59.76/10.39 % (4102461)------------------------------
% 59.76/10.39 % (4102461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.76/10.39 % (4102461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.76/10.39 % (4102461)CaDiCaL version: 2.1.3
% 59.76/10.39 % (4102461)Termination reason: Instruction limit
% 59.76/10.39 % (4102461)Termination phase: Saturation
% 59.76/10.39 % (4102461)Time elapsed: 0.610 s
% 59.76/10.39 % (4102461)Peak memory usage: 111 MB
% 59.76/10.39 % (4102461)Instructions burned: 1189 (million)
% 59.76/10.39 % (4102475)Instruction limit reached!
% 59.76/10.39 % (4102475)------------------------------
% 59.76/10.39 % (4102475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.76/10.39 % (4102475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.76/10.39 % (4102475)CaDiCaL version: 2.1.3
% 59.76/10.39 % (4102475)Termination reason: Instruction limit
% 59.76/10.39 % (4102475)Termination phase: Saturation
% 59.76/10.39 % (4102475)Time elapsed: 0.134 s
% 59.76/10.39 % (4102475)Peak memory usage: 94 MB
% 59.76/10.39 % (4102475)Instructions burned: 317 (million)
% 59.76/10.39 % (4102477)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=1146205311:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/12125Mi)
% 59.76/10.39 % (4102478)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=379379549:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2988 on theBenchmark for (2988ds/2836Mi)
% 59.76/10.39 % (4102469)Instruction limit reached!
% 59.76/10.39 % (4102469)------------------------------
% 59.76/10.39 % (4102469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.76/10.39 % (4102469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.76/10.39 % (4102469)CaDiCaL version: 2.1.3
% 59.76/10.39 % (4102469)Termination reason: Instruction limit
% 59.76/10.39 % (4102469)Termination phase: Saturation
% 59.76/10.39 % (4102469)Time elapsed: 1.418 s
% 59.76/10.39 % (4102469)Peak memory usage: 210 MB
% 59.76/10.39 % (4102469)Instructions burned: 2051 (million)
% 59.76/10.39 % (4102481)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2100922054:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2979 on theBenchmark for (2979ds/14534Mi)
% 59.76/10.39 % (4102478)Instruction limit reached!
% 59.76/10.39 % (4102478)------------------------------
% 59.76/10.39 % (4102478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.76/10.39 % (4102478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.76/10.39 % (4102478)CaDiCaL version: 2.1.3
% 59.76/10.39 % (4102478)Termination reason: Instruction limit
% 59.76/10.39 % (4102478)Termination phase: Saturation
% 59.76/10.39 % (4102478)Time elapsed: 1.843 s
% 59.76/10.39 % (4102478)Peak memory usage: 157 MB
% 59.76/10.39 % (4102478)Instructions burned: 2837 (million)
% 59.76/10.39 % (4102483)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=3449577776:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2968 on theBenchmark for (2968ds/11832Mi)
% 59.76/10.39 % (4102470)Instruction limit reached!
% 59.76/10.39 % (4102470)------------------------------
% 59.76/10.39 % (4102470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.76/10.39 % (4102470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.76/10.39 % (4102470)CaDiCaL version: 2.1.3
% 59.76/10.39 % (4102470)Termination reason: Instruction limit
% 59.76/10.39 % (4102470)Termination phase: Saturation
% 59.76/10.39 % (4102470)Time elapsed: 3.272 s
% 59.76/10.39 % (4102470)Peak memory usage: 172 MB
% 59.76/10.39 % (4102470)Instructions burned: 4948 (million)
% 59.76/10.39 % (4102485)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=3084512962:i=2279:fgj=on:bd=all_2960 on theBenchmark for (2960ds/2279Mi)
% 59.76/10.39 % (4102485)Instruction limit reached!
% 59.76/10.39 % (4102485)------------------------------
% 59.76/10.39 % (4102485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.76/10.39 % (4102485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.76/10.39 % (4102485)CaDiCaL version: 2.1.3
% 59.76/10.39 % (4102485)Termination reason: Instruction limit
% 59.76/10.39 % (4102485)Termination phase: Saturation
% 59.76/10.39 % (4102485)Time elapsed: 1.372 s
% 59.76/10.39 % (4102485)Peak memory usage: 202 MB
% 59.76/10.39 % (4102485)Instructions burned: 2279 (million)
% 59.76/10.39 % (4102487)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:drc=off:fde=none:sp=reverse_arity:urr=ec_only:gs=on:s2agt=16:random_seed=3838221127:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2944 on theBenchmark for (2944ds/6225Mi)
% 59.76/10.39 % (4102487)Instruction limit reached!
% 59.76/10.39 % (4102487)------------------------------
% 59.76/10.39 % (4102487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.76/10.39 % (4102487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.76/10.39 % (4102487)CaDiCaL version: 2.1.3
% 59.76/10.39 % (4102487)Termination reason: Instruction limit
% 59.76/10.39 % (4102487)Termination phase: Saturation
% 59.76/10.39 % (4102487)Time elapsed: 2.777 s
% 59.76/10.39 % (4102487)Peak memory usage: 224 MB
% 59.76/10.39 % (4102487)Instructions burned: 6229 (million)
% 59.76/10.39 % (4102489)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=3898988518:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2915 on theBenchmark for (2915ds/21755Mi)
% 59.76/10.39 % (4102477)Instruction limit reached!
% 59.76/10.39 % (4102477)------------------------------
% 59.76/10.39 % (4102477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.76/10.39 % (4102477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.76/10.39 % (4102477)CaDiCaL version: 2.1.3
% 59.76/10.39 % (4102477)Termination reason: Instruction limit
% 59.76/10.39 % (4102477)Termination phase: Saturation
% 59.76/10.39 % (4102477)Time elapsed: 7.571 s
% 59.76/10.39 % (4102477)Peak memory usage: 219 MB
% 59.76/10.39 % (4102477)Instructions burned: 12126 (million)
% 59.76/10.39 % (4102491)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=3000835087:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2912 on theBenchmark for (2912ds/16427Mi)
% 59.76/10.39 % (4102481)First to succeed.
% 59.76/10.39 % (4102481)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4102450"
% 59.76/10.39 % (4102481)Refutation found. Thanks to Tanya!
% 59.76/10.39 % SZS status Unsatisfiable for theBenchmark
% 59.76/10.39 % SZS output start Proof for theBenchmark
% See solution above
% 68.00/10.59 % (4102481)------------------------------
% 68.00/10.59 % (4102481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.00/10.59 % (4102481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.00/10.59 % (4102481)CaDiCaL version: 2.1.3
% 68.00/10.59 % (4102481)Termination reason: Refutation
% 68.00/10.59 % (4102481)Time elapsed: 7.125 s
% 68.00/10.59 % (4102481)Peak memory usage: 237 MB
% 68.00/10.59 % (4102481)Instructions burned: 10650 (million)
% 68.00/10.59 % (4102481)------------------------------
% 68.00/10.59 % (4102481)------------------------------
% 68.00/10.59 % (4102450)Success in time 9.711 s
% 68.00/10.59 % Vampire exiting
%------------------------------------------------------------------------------