%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP050-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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 10:12:15 AM UTC 2026
% Result : Unsatisfiable 6.96s 1.71s
% Output : Refutation 8.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 5
% Syntax : Number of formulae : 102 ( 88 unt; 3 def)
% Number of atoms : 120 ( 93 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 34 ( 16 ~; 15 |; 0 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 11 ( 3 avg)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 231 ( 0 sgn 231 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),multiply(inverse(X1),multiply(inverse(X1),X1))))) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms) ).
fof(f3,plain,
( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| a2 != multiply(multiply(inverse(b2),b2),a2)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
inference(reorient_equations,[],[f2]) ).
fof(f5,definition,
( spl0_1
<=> multiply(multiply(a3,b3),c3) = multiply(a3,multiply(b3,c3)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f7,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| spl0_1 ),
inference(avatar_component_clause,[],[f5]) ).
fof(f9,definition,
( spl0_2
<=> a2 = multiply(multiply(inverse(b2),b2),a2) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f11,plain,
( a2 != multiply(multiply(inverse(b2),b2),a2)
| spl0_2 ),
inference(avatar_component_clause,[],[f9]) ).
fof(f13,definition,
( spl0_3
<=> multiply(inverse(a1),a1) = multiply(inverse(b1),b1) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f15,plain,
( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| spl0_3 ),
inference(avatar_component_clause,[],[f13]) ).
fof(f16,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f3,f13,f9,f5]) ).
fof(f18,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),X0)),multiply(inverse(X3),multiply(inverse(X3),X3)))) = multiply(X1,inverse(multiply(inverse(X0),multiply(inverse(X2),multiply(inverse(X2),X2))))),
inference(superposition,[],[f1,f1]) ).
fof(f36,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,X2)),multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(X2),multiply(inverse(X2),X2)))))) = X1,
inference(superposition,[],[f1,f18]) ).
fof(f40,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),multiply(inverse(multiply(X0,X1)),X3))),multiply(inverse(X2),multiply(inverse(X2),X2)))) = X3,
inference(superposition,[],[f1,f18]) ).
fof(f66,plain,
! [X0,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X4)),multiply(X0,X5))),multiply(inverse(X4),multiply(inverse(X4),X4)))) = X5,
inference(superposition,[],[f40,f40]) ).
fof(f108,plain,
! [X2,X0,X1] : multiply(inverse(X2),multiply(inverse(X2),X2)) = multiply(inverse(multiply(X1,X2)),inverse(multiply(X0,multiply(inverse(multiply(X1,X0)),multiply(inverse(multiply(X1,X0)),multiply(X1,X0)))))),
inference(superposition,[],[f1,f66]) ).
fof(f110,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X0)) = multiply(inverse(multiply(X3,X2)),multiply(X3,X0)),
inference(superposition,[],[f36,f66]) ).
fof(f147,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,multiply(inverse(X2),multiply(inverse(X2),X2)))),multiply(X1,X3)) = multiply(X0,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X0))),X3)),
inference(superposition,[],[f110,f66]) ).
fof(f259,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,inverse(X2)))),multiply(inverse(X0),multiply(inverse(X0),X0))) = X2,
inference(superposition,[],[f36,f108]) ).
fof(f384,plain,
! [X2,X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,multiply(inverse(X2),multiply(inverse(X2),X2)))),multiply(X1,multiply(inverse(X2),multiply(inverse(X2),X2)))),
inference(superposition,[],[f147,f259]) ).
fof(f476,plain,
! [X0,X1] : multiply(inverse(X1),X1) = multiply(inverse(X0),X0),
inference(superposition,[],[f384,f384]) ).
fof(f655,plain,
! [X2,X0,X1] : multiply(inverse(X2),multiply(inverse(X2),X2)) = multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(inverse(X0),X0)))),
inference(superposition,[],[f36,f476]) ).
fof(f661,plain,
! [X2,X0] : inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X2),multiply(inverse(X2),X2)))) = X2,
inference(superposition,[],[f66,f476]) ).
fof(f714,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(inverse(X1),X1)))) = X1,
inference(superposition,[],[f661,f110]) ).
fof(f721,plain,
! [X0] : multiply(inverse(X0),X0) = inverse(multiply(X0,multiply(inverse(X0),multiply(inverse(X0),X0)))),
inference(superposition,[],[f66,f661]) ).
fof(f771,plain,
! [X0,X1] : multiply(inverse(X0),X0) = inverse(multiply(X1,multiply(inverse(X1),multiply(inverse(X0),X0)))),
inference(superposition,[],[f721,f476]) ).
fof(f793,plain,
! [X0,X1] : multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,multiply(inverse(inverse(X0)),inverse(X0)))) = X0,
inference(superposition,[],[f36,f721]) ).
fof(f859,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X1)),X1)),multiply(inverse(X0),X0))) = X1,
inference(superposition,[],[f714,f476]) ).
fof(f883,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,multiply(X2,multiply(inverse(X0),X0)))),multiply(X1,X3)) = multiply(X0,multiply(inverse(multiply(X2,X0)),X3)),
inference(superposition,[],[f110,f714]) ).
fof(f955,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,multiply(inverse(X2),multiply(inverse(X0),X0)))),multiply(X1,X3)) = multiply(multiply(inverse(X0),X0),multiply(X2,X3)),
inference(superposition,[],[f110,f771]) ).
fof(f989,plain,
! [X2,X3,X0] : multiply(multiply(inverse(X0),X0),multiply(X2,X3)) = multiply(X0,multiply(inverse(multiply(inverse(X2),X0)),X3)),
inference(forward_demodulation,[],[f955,f883]) ).
fof(f1035,plain,
! [X0] : multiply(inverse(inverse(X0)),inverse(X0)) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0)))),X0)),
inference(superposition,[],[f714,f793]) ).
fof(f1055,plain,
! [X0] : inverse(multiply(inverse(X0),X0)) = multiply(inverse(inverse(X0)),inverse(X0)),
inference(forward_demodulation,[],[f1035,f859]) ).
fof(f1078,plain,
! [X0,X1] : multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(multiply(inverse(X0),X0)))) = X0,
inference(superposition,[],[f793,f1055]) ).
fof(f1091,plain,
! [X0,X1] : multiply(inverse(X1),X1) = inverse(multiply(inverse(X0),X0)),
inference(superposition,[],[f476,f1055]) ).
fof(f1124,plain,
! [X0] : multiply(inverse(inverse(X0)),multiply(inverse(inverse(X0)),inverse(X0))) = X0,
inference(forward_demodulation,[],[f1078,f655]) ).
fof(f1131,plain,
! [X0] : multiply(inverse(inverse(X0)),inverse(multiply(inverse(X0),X0))) = X0,
inference(forward_demodulation,[],[f1124,f1055]) ).
fof(f1203,plain,
! [X2,X0] : multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(inverse(X2)),multiply(inverse(inverse(X2)),inverse(X2)))) = X2,
inference(superposition,[],[f259,f1091]) ).
fof(f1258,plain,
! [X0,X1] : multiply(multiply(inverse(X0),X0),multiply(inverse(inverse(X1)),multiply(inverse(inverse(X1)),inverse(X1)))) = X1,
inference(superposition,[],[f793,f1091]) ).
fof(f1288,plain,
! [X0,X1] : multiply(multiply(inverse(X0),X0),multiply(inverse(inverse(X1)),inverse(multiply(inverse(X1),X1)))) = X1,
inference(forward_demodulation,[],[f1258,f1055]) ).
fof(f1298,plain,
! [X2,X0] : multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(inverse(X2)),inverse(multiply(inverse(X2),X2)))) = X2,
inference(forward_demodulation,[],[f1203,f1055]) ).
fof(f1304,plain,
! [X0,X1] : multiply(multiply(inverse(X0),X0),X1) = X1,
inference(forward_demodulation,[],[f1288,f1131]) ).
fof(f1309,plain,
! [X2,X0] : multiply(inverse(inverse(multiply(inverse(X0),X0))),X2) = X2,
inference(forward_demodulation,[],[f1298,f1131]) ).
fof(f1334,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(X0),X0)),X1) = X1,
inference(superposition,[],[f1304,f1055]) ).
fof(f1349,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X0)) = multiply(inverse(multiply(multiply(inverse(X3),X3),X2)),X0),
inference(superposition,[],[f110,f1304]) ).
fof(f1382,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X0)) = multiply(inverse(X2),X0),
inference(forward_demodulation,[],[f1349,f1304]) ).
fof(f1495,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(X2)))),multiply(inverse(X0),multiply(inverse(X0),X0))) = X2,
inference(superposition,[],[f259,f1309]) ).
fof(f1521,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(X2))),multiply(inverse(X0),X0)) = X2,
inference(forward_demodulation,[],[f1495,f1382]) ).
fof(f1552,plain,
! [X2,X0] : multiply(inverse(inverse(X2)),multiply(inverse(X0),X0)) = X2,
inference(forward_demodulation,[],[f1521,f1309]) ).
fof(f1572,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,X1)),X3) = multiply(inverse(multiply(inverse(X0),X1)),multiply(inverse(multiply(X2,X0)),X3)),
inference(superposition,[],[f1382,f1382]) ).
fof(f1580,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(X0,multiply(inverse(X1),multiply(inverse(X1),X1)))),multiply(X0,X2))),multiply(X3,X5)) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,X1)),multiply(X4,X3))),X2)),X5),
inference(superposition,[],[f1382,f147]) ).
fof(f1591,plain,
! [X2,X0,X1] : multiply(X0,multiply(inverse(multiply(X1,X0)),X2)) = multiply(inverse(multiply(X1,multiply(inverse(X0),X0))),X2),
inference(superposition,[],[f1382,f714]) ).
fof(f1727,plain,
! [X2,X3,X0,X1,X5] : multiply(inverse(multiply(inverse(multiply(X0,multiply(inverse(X1),multiply(inverse(X1),X1)))),multiply(X0,X2))),multiply(X3,X5)) = multiply(inverse(multiply(inverse(multiply(inverse(X1),X3)),X2)),X5),
inference(forward_demodulation,[],[f1580,f1382]) ).
fof(f1753,plain,
! [X2,X3,X1,X5] : multiply(inverse(multiply(inverse(multiply(inverse(X1),X3)),X2)),X5) = multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(X1),X1))),X2)),multiply(X3,X5)),
inference(forward_demodulation,[],[f1727,f1382]) ).
fof(f1765,plain,
! [X2,X3,X1,X5] : multiply(inverse(multiply(inverse(multiply(inverse(X1),X3)),X2)),X5) = multiply(inverse(multiply(X1,multiply(inverse(multiply(inverse(X1),X1)),X2))),multiply(X3,X5)),
inference(forward_demodulation,[],[f1753,f1591]) ).
fof(f1771,plain,
! [X2,X3,X1,X5] : multiply(inverse(multiply(inverse(multiply(inverse(X1),X3)),X2)),X5) = multiply(inverse(multiply(multiply(inverse(X1),X1),multiply(X1,X2))),multiply(X3,X5)),
inference(forward_demodulation,[],[f1765,f989]) ).
fof(f1775,plain,
! [X2,X3,X1,X5] : multiply(inverse(multiply(inverse(multiply(inverse(X1),X3)),X2)),X5) = multiply(inverse(multiply(X1,X2)),multiply(X3,X5)),
inference(forward_demodulation,[],[f1771,f1304]) ).
fof(f1822,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,multiply(inverse(X2),multiply(inverse(X2),X2)))),multiply(X1,multiply(inverse(multiply(X3,X2)),multiply(X3,inverse(inverse(X0)))))) = X0,
inference(superposition,[],[f147,f1552]) ).
fof(f1837,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))),multiply(X1,X3)) = multiply(X4,multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X0)),X4))),X3)),
inference(superposition,[],[f147,f1552]) ).
fof(f1841,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(X1),X1)),X2) = multiply(inverse(X0),multiply(inverse(inverse(X0)),X2)),
inference(superposition,[],[f1382,f1552]) ).
fof(f1843,plain,
! [X2,X0] : multiply(inverse(X0),multiply(inverse(inverse(X0)),X2)) = X2,
inference(forward_demodulation,[],[f1841,f1334]) ).
fof(f1847,plain,
! [X2,X3,X0,X4] : multiply(X4,multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X0)),X4))),X3)) = multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))),X3),
inference(forward_demodulation,[],[f1837,f1382]) ).
fof(f1860,plain,
! [X2,X3,X0] : multiply(inverse(multiply(inverse(X2),multiply(inverse(X2),X2))),multiply(inverse(multiply(X3,X2)),multiply(X3,inverse(inverse(X0))))) = X0,
inference(forward_demodulation,[],[f1822,f1382]) ).
fof(f1892,plain,
! [X2,X3,X0,X4] : multiply(X4,multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X0)),X4))),X3)) = multiply(inverse(multiply(X2,multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))),multiply(X2,X3)),
inference(forward_demodulation,[],[f1847,f1775]) ).
fof(f1902,plain,
! [X2,X3,X0] : multiply(inverse(multiply(X3,multiply(inverse(X2),X2))),multiply(X3,inverse(inverse(X0)))) = X0,
inference(forward_demodulation,[],[f1860,f1572]) ).
fof(f1910,plain,
! [X2,X3,X0,X4] : multiply(X4,multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X0)),X4))),X3)) = multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),X3),
inference(forward_demodulation,[],[f1892,f1382]) ).
fof(f1915,plain,
! [X2,X0] : multiply(inverse(multiply(inverse(X2),X2)),inverse(inverse(X0))) = X0,
inference(forward_demodulation,[],[f1902,f1382]) ).
fof(f1920,plain,
! [X2,X3,X0,X4] : multiply(X4,multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X0)),X4))),X3)) = multiply(inverse(multiply(X2,multiply(inverse(X2),X2))),multiply(X2,X3)),
inference(forward_demodulation,[],[f1910,f1775]) ).
fof(f1923,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[],[f1915,f1334]) ).
fof(f1926,plain,
! [X2,X3,X0,X4] : multiply(inverse(multiply(inverse(X2),X2)),X3) = multiply(X4,multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X0)),X4))),X3)),
inference(forward_demodulation,[],[f1920,f1382]) ).
fof(f1927,plain,
! [X2,X3,X4] : multiply(inverse(multiply(inverse(X2),X2)),X3) = multiply(X4,multiply(inverse(X4),X3)),
inference(forward_demodulation,[],[f1926,f1843]) ).
fof(f1928,plain,
! [X3,X4] : multiply(X4,multiply(inverse(X4),X3)) = X3,
inference(forward_demodulation,[],[f1927,f1334]) ).
fof(f1956,plain,
! [X0,X1] : multiply(inverse(X1),X1) = multiply(X0,inverse(X0)),
inference(superposition,[],[f476,f1923]) ).
fof(f1962,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = inverse(multiply(X1,multiply(inverse(X1),multiply(X0,inverse(X0))))),
inference(superposition,[],[f771,f1923]) ).
fof(f1967,plain,
! [X0,X1] : multiply(multiply(X0,inverse(X0)),X1) = X1,
inference(superposition,[],[f1304,f1923]) ).
fof(f1969,plain,
! [X0,X1] : multiply(inverse(inverse(X1)),multiply(X0,inverse(X0))) = X1,
inference(superposition,[],[f1552,f1923]) ).
fof(f1971,plain,
! [X0,X1] : multiply(X1,multiply(X0,inverse(X0))) = X1,
inference(forward_demodulation,[],[f1969,f1923]) ).
fof(f1974,plain,
! [X0] : multiply(X0,inverse(X0)) = inverse(multiply(X0,inverse(X0))),
inference(forward_demodulation,[],[f1962,f1928]) ).
fof(f2081,plain,
! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(inverse(X3),multiply(inverse(X2),multiply(inverse(X2),X2))))) = inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X0))),X3)),multiply(inverse(multiply(X1,X2)),multiply(X0,inverse(X0))))),
inference(superposition,[],[f18,f1956]) ).
fof(f2118,plain,
! [X2,X0,X1] : multiply(inverse(X2),X1) = multiply(inverse(multiply(inverse(X1),X2)),multiply(X0,inverse(X0))),
inference(superposition,[],[f1382,f1956]) ).
fof(f2194,plain,
! [X2,X1] : inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(forward_demodulation,[],[f2118,f1971]) ).
fof(f2225,plain,
! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(inverse(X3),multiply(inverse(X2),multiply(inverse(X2),X2))))) = inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X0))),X3)),inverse(multiply(X1,X2)))),
inference(forward_demodulation,[],[f2081,f1971]) ).
fof(f2320,plain,
! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(inverse(X3),multiply(inverse(X2),multiply(inverse(X2),X2))))) = multiply(inverse(inverse(multiply(X1,X2))),multiply(inverse(multiply(X0,inverse(X0))),X3)),
inference(forward_demodulation,[],[f2225,f2194]) ).
fof(f2394,plain,
! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(inverse(X3),multiply(inverse(X2),multiply(inverse(X2),X2))))) = multiply(inverse(inverse(multiply(X1,X2))),multiply(multiply(X0,inverse(X0)),X3)),
inference(forward_demodulation,[],[f2320,f1974]) ).
fof(f2448,plain,
! [X2,X3,X1] : multiply(X1,inverse(multiply(inverse(X3),multiply(inverse(X2),multiply(inverse(X2),X2))))) = multiply(inverse(inverse(multiply(X1,X2))),X3),
inference(forward_demodulation,[],[f2394,f1967]) ).
fof(f2483,plain,
! [X2,X3,X1] : multiply(X1,inverse(multiply(inverse(X3),multiply(inverse(X2),multiply(inverse(X2),X2))))) = multiply(multiply(X1,X2),X3),
inference(forward_demodulation,[],[f2448,f1923]) ).
fof(f2504,plain,
! [X2,X3,X1] : multiply(multiply(X1,X2),X3) = multiply(X1,multiply(inverse(multiply(inverse(X2),multiply(inverse(X2),X2))),X3)),
inference(forward_demodulation,[],[f2483,f2194]) ).
fof(f2515,plain,
! [X2,X3,X1] : multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,multiply(inverse(multiply(inverse(X2),X2)),X3))),
inference(forward_demodulation,[],[f2504,f1591]) ).
fof(f2521,plain,
! [X2,X3,X1] : multiply(multiply(X1,X2),X3) = multiply(X1,multiply(multiply(inverse(X2),X2),multiply(X2,X3))),
inference(forward_demodulation,[],[f2515,f989]) ).
fof(f2525,plain,
! [X2,X3,X1] : multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(forward_demodulation,[],[f2521,f1304]) ).
fof(f2860,plain,
( multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3))
| spl0_1 ),
inference(superposition,[],[f7,f2525]) ).
fof(f2895,plain,
( $false
| spl0_1 ),
inference(trivial_inequality_removal,[],[f2860]) ).
fof(f2896,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f2895]) ).
fof(f3178,plain,
( $false
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f11,f1304]) ).
fof(f3179,plain,
spl0_2,
inference(avatar_contradiction_clause,[],[f3178]) ).
fof(f3180,plain,
( $false
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f15,f476]) ).
fof(f3181,plain,
spl0_3,
inference(avatar_contradiction_clause,[],[f3180]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f16]) ).
cnf(s2,plain,
spl0_1,
inference(sat_conversion,[],[f2896]) ).
cnf(s3,plain,
spl0_2,
inference(sat_conversion,[],[f3179]) ).
cnf(s4,plain,
spl0_3,
inference(sat_conversion,[],[f3181]) ).
cnf(s5,plain,
$false,
inference(rat,[],[s1,s4,s3,s2]) ).
fof(f3182,plain,
$false,
inference(avatar_sat_refutation,[],[s5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP050-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Sun Sep 27 09:16:34 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.30 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.32 Running first-order theorem proving
% 0.04/0.32 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.19/1.55 % (2103174)Input is clausal, will run a generic CNF schedule.
% 6.19/1.55 % (2103182)lrs+10_1_sil=8000:sp=occurrence:random_seed=270454717:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.19/1.55 % (2103181)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2353541114:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.19/1.55 % (2103185)dis-21_1_sil=8000:lcm=predicate:random_seed=3471650491:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 6.19/1.55 % (2103183)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3729842574:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.19/1.55 % (2103184)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3096413646:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.19/1.55 % (2103179)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2160222126:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.19/1.55 % (2103180)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2330272842:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.19/1.55 % (2103185)Refutation not found, incomplete strategy
% 6.19/1.55 % (2103185)------------------------------
% 6.19/1.55 % (2103185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.19/1.55 % (2103185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.19/1.55 % (2103185)CaDiCaL version: 2.1.3
% 6.19/1.55 % (2103185)Termination reason: Refutation not found, incomplete strategy
% 6.19/1.55 % (2103185)Time elapsed: 0.0000 s
% 6.19/1.55 % (2103185)Peak memory usage: 88 MB
% 6.19/1.55 % (2103182)Instruction limit reached!
% 6.19/1.55 % (2103182)------------------------------
% 6.19/1.55 % (2103182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.19/1.55 % (2103182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.19/1.55 % (2103182)CaDiCaL version: 2.1.3
% 6.19/1.55 % (2103182)Termination reason: Instruction limit
% 6.19/1.55 % (2103182)Termination phase: Saturation
% 6.19/1.55 % (2103182)Time elapsed: 0.034 s
% 6.19/1.55 % (2103182)Peak memory usage: 89 MB
% 6.19/1.55 % (2103182)Instructions burned: 107 (million)
% 6.19/1.55 % (2103183)Instruction limit reached!
% 6.19/1.55 % (2103183)------------------------------
% 6.19/1.55 % (2103183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.19/1.55 % (2103183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.19/1.55 % (2103183)CaDiCaL version: 2.1.3
% 6.19/1.55 % (2103183)Termination reason: Instruction limit
% 6.19/1.55 % (2103183)Termination phase: Saturation
% 6.19/1.55 % (2103183)Time elapsed: 0.037 s
% 6.19/1.55 % (2103183)Peak memory usage: 89 MB
% 6.19/1.55 % (2103183)Instructions burned: 114 (million)
% 6.19/1.55 % (2103184)Instruction limit reached!
% 6.19/1.55 % (2103184)------------------------------
% 6.19/1.55 % (2103184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.19/1.55 % (2103184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.19/1.55 % (2103184)CaDiCaL version: 2.1.3
% 6.19/1.55 % (2103184)Termination reason: Instruction limit
% 6.19/1.55 % (2103184)Termination phase: Saturation
% 6.19/1.55 % (2103184)Time elapsed: 0.052 s
% 6.19/1.55 % (2103184)Peak memory usage: 89 MB
% 6.19/1.55 % (2103184)Instructions burned: 181 (million)
% 6.19/1.55 % (2103194)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3053786108:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 6.19/1.55 % (2103193)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2960275398:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 6.19/1.55 % (2103193)Refutation not found, incomplete strategy
% 6.19/1.55 % (2103193)------------------------------
% 6.19/1.55 % (2103193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.19/1.55 % (2103194)Refutation not found, incomplete strategy
% 6.19/1.55 % (2103194)------------------------------
% 6.19/1.55 % (2103194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2103193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2103194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2103194)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2103193)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2103193)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.71 % (2103193)Time elapsed: 0.001 s
% 6.96/1.71 % (2103194)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.71 % (2103194)Time elapsed: 0.001 s
% 6.96/1.71 % (2103193)Peak memory usage: 88 MB
% 6.96/1.71 % (2103194)Peak memory usage: 88 MB
% 6.96/1.71 % (2103185)------------------------------
% 6.96/1.71 % (2103185)------------------------------
% 6.96/1.71 % (2103195)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2093818245:st=4:i=219:sd=3:ss=axioms_2998 on theBenchmark for (2998ds/219Mi)
% 6.96/1.71 % (2103195)Refutation not found, incomplete strategy
% 6.96/1.71 % (2103195)------------------------------
% 6.96/1.71 % (2103195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2103195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2103195)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2103195)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.71 % (2103195)Time elapsed: 0.0000 s
% 6.96/1.71 % (2103195)Peak memory usage: 88 MB
% 6.96/1.71 % (2103199)lrs+10_64_to=lpo:sil=8000:random_seed=685041452:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 6.96/1.71 % (2103199)Instruction limit reached!
% 6.96/1.71 % (2103199)------------------------------
% 6.96/1.71 % (2103199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2103199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2103199)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2103199)Termination reason: Instruction limit
% 6.96/1.71 % (2103199)Termination phase: Saturation
% 6.96/1.71 % (2103199)Time elapsed: 0.041 s
% 6.96/1.71 % (2103199)Peak memory usage: 89 MB
% 6.96/1.71 % (2103199)Instructions burned: 127 (million)
% 6.96/1.71 % (2103193)------------------------------
% 6.96/1.71 % (2103193)------------------------------
% 6.96/1.71 % (2103194)------------------------------
% 6.96/1.71 % (2103194)------------------------------
% 6.96/1.71 % (2103195)------------------------------
% 6.96/1.71 % (2103195)------------------------------
% 6.96/1.71 % (2103201)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2627049491:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 6.96/1.71 % (2103202)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3293767173:i=157:gtg=all_2996 on theBenchmark for (2996ds/157Mi)
% 6.96/1.71 % (2103203)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3636923884:i=3394:sd=4:ss=included:sgt=64_2996 on theBenchmark for (2996ds/3394Mi)
% 6.96/1.71 % (2103204)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=731755039:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 6.96/1.71 % (2103202)Instruction limit reached!
% 6.96/1.71 % (2103202)------------------------------
% 6.96/1.71 % (2103202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2103202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2103202)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2103202)Termination reason: Instruction limit
% 6.96/1.71 % (2103202)Termination phase: Saturation
% 6.96/1.71 % (2103202)Time elapsed: 0.050 s
% 6.96/1.71 % (2103202)Peak memory usage: 91 MB
% 6.96/1.71 % (2103202)Instructions burned: 160 (million)
% 6.96/1.71 % (2103201)Instruction limit reached!
% 6.96/1.71 % (2103201)------------------------------
% 6.96/1.71 % (2103201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2103201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2103201)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2103201)Termination reason: Instruction limit
% 6.96/1.71 % (2103201)Termination phase: Saturation
% 6.96/1.71 % (2103201)Time elapsed: 0.063 s
% 6.96/1.71 % (2103201)Peak memory usage: 90 MB
% 6.96/1.71 % (2103201)Instructions burned: 194 (million)
% 6.96/1.71 % (2103204)Instruction limit reached!
% 6.96/1.71 % (2103204)------------------------------
% 6.96/1.71 % (2103204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2103204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2103204)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2103204)Termination reason: Instruction limit
% 6.96/1.71 % (2103204)Termination phase: Saturation
% 6.96/1.71 % (2103204)Time elapsed: 0.033 s
% 6.96/1.71 % (2103204)Peak memory usage: 89 MB
% 6.96/1.71 % (2103204)Instructions burned: 108 (million)
% 6.96/1.71 % (2103209)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3835680697:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 6.96/1.71 % (2103210)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3609529061:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2994 on theBenchmark for (2994ds/242Mi)
% 6.96/1.71 % (2103209)Refutation not found, incomplete strategy
% 6.96/1.71 % (2103209)------------------------------
% 6.96/1.71 % (2103209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2103209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2103209)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2103209)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.71 % (2103209)Time elapsed: 0.0000 s
% 6.96/1.71 % (2103209)Peak memory usage: 87 MB
% 6.96/1.71 % (2103211)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3077677015:cond=fast:i=5208:av=off_2994 on theBenchmark for (2994ds/5208Mi)
% 6.96/1.71 % (2103210)Instruction limit reached!
% 6.96/1.71 % (2103210)------------------------------
% 6.96/1.71 % (2103210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2103210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2103210)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2103210)Termination reason: Instruction limit
% 6.96/1.71 % (2103210)Termination phase: Saturation
% 6.96/1.71 % (2103210)Time elapsed: 0.071 s
% 6.96/1.71 % (2103210)Peak memory usage: 90 MB
% 6.96/1.71 % (2103210)Instructions burned: 243 (million)
% 6.96/1.71 % (2103209)------------------------------
% 6.96/1.71 % (2103209)------------------------------
% 6.96/1.71 % (2103215)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3762058733:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi)
% 6.96/1.71 % (2103215)Instruction limit reached!
% 6.96/1.71 % (2103215)------------------------------
% 6.96/1.71 % (2103215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2103215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2103215)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2103215)Termination reason: Instruction limit
% 6.96/1.71 % (2103215)Termination phase: Saturation
% 6.96/1.71 % (2103215)Time elapsed: 0.043 s
% 6.96/1.71 % (2103215)Peak memory usage: 89 MB
% 6.96/1.71 % (2103215)Instructions burned: 135 (million)
% 6.96/1.71 % (2103216)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3693474513:i=499:bd=all_2992 on theBenchmark for (2992ds/499Mi)
% 6.96/1.71 % (2103218)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4123848351:i=191:fgj=on:bd=all_2991 on theBenchmark for (2991ds/191Mi)
% 6.96/1.71 % (2103218)Instruction limit reached!
% 6.96/1.71 % (2103218)------------------------------
% 6.96/1.71 % (2103218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2103218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2103218)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2103218)Termination reason: Instruction limit
% 6.96/1.71 % (2103218)Termination phase: Saturation
% 6.96/1.71 % (2103218)Time elapsed: 0.062 s
% 6.96/1.71 % (2103218)Peak memory usage: 90 MB
% 6.96/1.71 % (2103218)Instructions burned: 192 (million)
% 6.96/1.71 % (2103216)Instruction limit reached!
% 6.96/1.71 % (2103216)------------------------------
% 6.96/1.71 % (2103216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2103216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2103216)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2103216)Termination reason: Instruction limit
% 6.96/1.71 % (2103216)Termination phase: Saturation
% 6.96/1.71 % (2103216)Time elapsed: 0.150 s
% 6.96/1.71 % (2103216)Peak memory usage: 94 MB
% 6.96/1.71 % (2103216)Instructions burned: 499 (million)
% 6.96/1.71 % (2103203)First to succeed.
% 6.96/1.71 % (2103203)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2103174"
% 6.96/1.71 % (2103221)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1536939656:i=264:kws=precedence:fsr=off_2990 on theBenchmark for (2990ds/264Mi)
% 6.96/1.71 % (2103222)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3890854498:cond=on:i=156:bs=on:gtg=exists_all:er=known_2989 on theBenchmark for (2989ds/156Mi)
% 6.96/1.71 % (2103221)Instruction limit reached!
% 6.96/1.71 % (2103221)------------------------------
% 6.96/1.71 % (2103221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2103221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2103221)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2103221)Termination reason: Instruction limit
% 6.96/1.71 % (2103221)Termination phase: Saturation
% 6.96/1.71 % (2103221)Time elapsed: 0.086 s
% 6.96/1.71 % (2103221)Peak memory usage: 91 MB
% 6.96/1.71 % (2103221)Instructions burned: 265 (million)
% 6.96/1.71 % (2103222)Instruction limit reached!
% 6.96/1.71 % (2103222)------------------------------
% 6.96/1.71 % (2103222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2103222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2103222)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2103222)Termination reason: Instruction limit
% 6.96/1.71 % (2103222)Termination phase: Saturation
% 6.96/1.71 % (2103222)Time elapsed: 0.055 s
% 6.96/1.71 % (2103222)Peak memory usage: 89 MB
% 6.96/1.71 % (2103222)Instructions burned: 158 (million)
% 6.96/1.71 % (2103203)Refutation found. Thanks to Tanya!
% 6.96/1.71 % SZS status Unsatisfiable for theBenchmark
% 6.96/1.71 % SZS output start Proof for theBenchmark
% See solution above
% 8.58/1.81 % (2103203)------------------------------
% 8.58/1.81 % (2103203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.58/1.81 % (2103203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.58/1.81 % (2103203)CaDiCaL version: 2.1.3
% 8.58/1.81 % (2103203)Termination reason: Refutation
% 8.58/1.81 % (2103203)Time elapsed: 0.540 s
% 8.58/1.81 % (2103203)Peak memory usage: 135 MB
% 8.58/1.81 % (2103203)Instructions burned: 1563 (million)
% 8.58/1.81 % (2103203)------------------------------
% 8.58/1.81 % (2103203)------------------------------
% 8.58/1.81 % (2103174)Success in time 1.191 s
% 8.58/1.81 % Vampire exiting
%------------------------------------------------------------------------------