%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COL108-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:37:59 AM UTC 2026
% Result : Unsatisfiable 15.31s 2.87s
% Output : Refutation 16.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 34
% Syntax : Number of formulae : 155 ( 20 unt; 11 def)
% Number of atoms : 449 ( 107 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 474 ( 180 ~; 283 |; 0 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 12 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 9 con; 0-4 aty)
% Number of variables : 97 ( 0 sgn 97 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| X2 = c_Comb_Ocomb_Oop_A_D_D(X0,X1)
| X0 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2)
| X0 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(X0,X1,X2)),v_sko__uTG(X0,X1,X2))
| X2 = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(X0,X1,X2),v_sko__uTH(X0,X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_OAp__parcontractE_0) ).
fof(f2,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(X0,X1) = X2
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2) = X0
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(X0,X1,X2)),v_sko__uTG(X0,X1,X2)) = X0
| c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(X0,X1,X2),v_sko__uTH(X0,X1,X2)) = X2 ),
inference(reorient_equations,[],[f1]) ).
fof(f3,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(X1,v_sko__uTH(X0,X1,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| X2 = c_Comb_Ocomb_Oop_A_D_D(X0,X1)
| X0 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2)
| X0 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(X0,X1,X2)),v_sko__uTG(X0,X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_OAp__parcontractE_1) ).
fof(f4,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,v_sko__uTH(X0,X1,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(X0,X1) = X2
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2) = X0
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(X0,X1,X2)),v_sko__uTG(X0,X1,X2)) = X0 ),
inference(reorient_equations,[],[f3]) ).
fof(f5,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(X0,v_sko__uTI(X0,X1,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| X2 = c_Comb_Ocomb_Oop_A_D_D(X0,X1)
| X0 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2)
| X0 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(X0,X1,X2)),v_sko__uTG(X0,X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_OAp__parcontractE_2) ).
fof(f6,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X0,v_sko__uTI(X0,X1,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(X0,X1) = X2
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2) = X0
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(X0,X1,X2)),v_sko__uTG(X0,X1,X2)) = X0 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| X2 = c_Comb_Ocomb_Oop_A_D_D(X0,X1)
| X0 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2)
| X2 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(X0,X1,X2),X1),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(X0,X1,X2),X1))
| X2 = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(X0,X1,X2),v_sko__uTH(X0,X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_OAp__parcontractE_3) ).
fof(f8,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(X0,X1) = X2
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2) = X0
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(X0,X1,X2),X1),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(X0,X1,X2),X1)) = X2
| c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(X0,X1,X2),v_sko__uTH(X0,X1,X2)) = X2 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(X1,v_sko__uTH(X0,X1,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| X2 = c_Comb_Ocomb_Oop_A_D_D(X0,X1)
| X0 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2)
| X2 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(X0,X1,X2),X1),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(X0,X1,X2),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_OAp__parcontractE_4) ).
fof(f10,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,v_sko__uTH(X0,X1,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(X0,X1) = X2
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2) = X0
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(X0,X1,X2),X1),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(X0,X1,X2),X1)) = X2 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(X0,v_sko__uTI(X0,X1,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| X2 = c_Comb_Ocomb_Oop_A_D_D(X0,X1)
| X0 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2)
| X2 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(X0,X1,X2),X1),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(X0,X1,X2),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_OAp__parcontractE_5) ).
fof(f12,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X0,v_sko__uTI(X0,X1,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(X0,X1) = X2
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2) = X0
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(X0,X1,X2),X1),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(X0,X1,X2),X1)) = X2 ),
inference(reorient_equations,[],[f11]) ).
fof(f15,axiom,
! [X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| X1 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_OK1__parcontractD__dest_0) ).
fof(f16,plain,
! [X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(X0,X1)) = X1 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,axiom,
! [X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(X0,v_sko__uTE(X0,X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_OK1__parcontractD__dest_1) ).
fof(f23,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| X2 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(X0,X1,X2)),v_sko__uTC(X0,X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_OS2__parcontractD__dest_0) ).
fof(f24,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(X0,X1,X2)),v_sko__uTC(X0,X1,X2)) = X2 ),
inference(reorient_equations,[],[f23]) ).
fof(f25,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(X0,v_sko__uTB(X0,X1,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_OS2__parcontractD__dest_1) ).
fof(f26,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(X1,v_sko__uTC(X0,X1,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_OS2__parcontractD__dest_2) ).
fof(f29,axiom,
! [X0] : c_in(c_Pair(X0,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_Oparcontract_Ointros__1_0) ).
fof(f30,axiom,
! [X0,X1] : c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0),X1),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_Oparcontract_Ointros__2_0) ).
fof(f31,axiom,
! [X2,X0,X1] : c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(X0,X2),c_Comb_Ocomb_Oop_A_D_D(X1,X2)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_Oparcontract_Ointros__3_0) ).
fof(f32,axiom,
! [X2,X3,X0,X1] :
( c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X2,X0),c_Comb_Ocomb_Oop_A_D_D(X3,X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(X2,X3,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(X0,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_Oparcontract_Ointros__4_0) ).
fof(f1503,negated_conjecture,
c_in(c_Pair(v_x,v_ya,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1504,negated_conjecture,
c_in(c_Pair(v_z,v_w,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1505,negated_conjecture,
c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),v_xba,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f1506,negated_conjecture,
! [X0] :
( c_in(c_Pair(v_ya,v_xb(X0),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_x,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f1507,negated_conjecture,
! [X0] :
( c_in(c_Pair(X0,v_xb(X0),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_x,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f1508,negated_conjecture,
! [X0] :
( c_in(c_Pair(v_w,v_xaa(X0),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_z,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f1509,negated_conjecture,
! [X0] :
( c_in(c_Pair(X0,v_xaa(X0),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_z,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f1510,negated_conjecture,
! [X0] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,v_w),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_xba,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_7) ).
fof(f1512,plain,
~ c_in(c_Pair(v_xba,c_Comb_Ocomb_Oop_A_D_D(v_ya,v_w),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(resolution,[],[f29,f1510]) ).
fof(f1513,plain,
! [X0,X1] :
( ~ c_in(c_Pair(v_xba,c_Comb_Ocomb_Oop_A_D_D(X0,X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_w,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_ya,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(resolution,[],[f32,f1510]) ).
fof(f1710,plain,
( c_Comb_Ocomb_Oop_A_D_D(v_x,v_z) = v_xba
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(v_x,v_z,v_xba)),v_sko__uTG(v_x,v_z,v_xba))
| v_xba = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(v_x,v_z,v_xba),v_sko__uTH(v_x,v_z,v_xba)) ),
inference(resolution,[],[f2,f1505]) ).
fof(f1730,definition,
( spl0_13
<=> v_xba = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(v_x,v_z,v_xba),v_sko__uTH(v_x,v_z,v_xba)) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f1731,plain,
( v_xba != c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(v_x,v_z,v_xba),v_sko__uTH(v_x,v_z,v_xba))
| spl0_13 ),
inference(avatar_component_clause,[],[f1730]) ).
fof(f1732,plain,
( v_xba = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(v_x,v_z,v_xba),v_sko__uTH(v_x,v_z,v_xba))
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f1730]) ).
fof(f1734,definition,
( spl0_14
<=> v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(v_x,v_z,v_xba)),v_sko__uTG(v_x,v_z,v_xba)) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f1735,plain,
( v_x != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(v_x,v_z,v_xba)),v_sko__uTG(v_x,v_z,v_xba))
| spl0_14 ),
inference(avatar_component_clause,[],[f1734]) ).
fof(f1736,plain,
( v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(v_x,v_z,v_xba)),v_sko__uTG(v_x,v_z,v_xba))
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f1734]) ).
fof(f1738,definition,
( spl0_15
<=> v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f1739,plain,
( v_x != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| spl0_15 ),
inference(avatar_component_clause,[],[f1738]) ).
fof(f1740,plain,
( v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f1738]) ).
fof(f1742,definition,
( spl0_16
<=> c_Comb_Ocomb_Oop_A_D_D(v_x,v_z) = v_xba ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f1743,plain,
( c_Comb_Ocomb_Oop_A_D_D(v_x,v_z) != v_xba
| spl0_16 ),
inference(avatar_component_clause,[],[f1742]) ).
fof(f1744,plain,
( c_Comb_Ocomb_Oop_A_D_D(v_x,v_z) = v_xba
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f1742]) ).
fof(f1745,plain,
( spl0_13
| spl0_14
| spl0_15
| spl0_16 ),
inference(avatar_split_clause,[],[f1710,f1742,f1738,f1734,f1730]) ).
fof(f1753,plain,
( ! [X0,X1] :
( ~ c_in(c_Pair(v_sko__uTH(v_x,v_z,v_xba),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_sko__uTI(v_x,v_z,v_xba),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(v_xba,c_Comb_Ocomb_Oop_A_D_D(X0,X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )
| ~ spl0_13 ),
inference(superposition,[],[f32,f1732]) ).
fof(f1780,plain,
( ! [X0] :
( ~ c_in(c_Pair(v_sko__uTI(v_x,v_z,v_xba),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(v_xba,c_Comb_Ocomb_Oop_A_D_D(X0,v_xaa(v_sko__uTH(v_x,v_z,v_xba))),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_z,v_sko__uTH(v_x,v_z,v_xba),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )
| ~ spl0_13 ),
inference(resolution,[],[f1753,f1509]) ).
fof(f1782,definition,
( spl0_19
<=> c_in(c_Pair(v_z,v_sko__uTH(v_x,v_z,v_xba),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f1783,plain,
( c_in(c_Pair(v_z,v_sko__uTH(v_x,v_z,v_xba),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f1782]) ).
fof(f1784,plain,
( ~ c_in(c_Pair(v_z,v_sko__uTH(v_x,v_z,v_xba),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| spl0_19 ),
inference(avatar_component_clause,[],[f1782]) ).
fof(f1786,definition,
( spl0_20
<=> ! [X0] :
( ~ c_in(c_Pair(v_sko__uTI(v_x,v_z,v_xba),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(v_xba,c_Comb_Ocomb_Oop_A_D_D(X0,v_xaa(v_sko__uTH(v_x,v_z,v_xba))),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f1787,plain,
( ! [X0] :
( c_in(c_Pair(v_xba,c_Comb_Ocomb_Oop_A_D_D(X0,v_xaa(v_sko__uTH(v_x,v_z,v_xba))),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_sko__uTI(v_x,v_z,v_xba),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f1786]) ).
fof(f1788,plain,
( ~ spl0_19
| spl0_20
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1780,f1730,f1786,f1782]) ).
fof(f1829,plain,
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),v_xba,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(v_x,v_z) = v_xba
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| v_xba = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(v_x,v_z,v_xba),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(v_x,v_z,v_xba),v_z))
| spl0_19 ),
inference(resolution,[],[f1784,f10]) ).
fof(f1830,plain,
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),v_xba,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(v_x,v_z) = v_xba
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(v_x,v_z,v_xba)),v_sko__uTG(v_x,v_z,v_xba))
| spl0_19 ),
inference(resolution,[],[f1784,f4]) ).
fof(f1831,plain,
( c_Comb_Ocomb_Oop_A_D_D(v_x,v_z) = v_xba
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(v_x,v_z,v_xba)),v_sko__uTG(v_x,v_z,v_xba))
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1830,f1505]) ).
fof(f1832,plain,
( c_Comb_Ocomb_Oop_A_D_D(v_x,v_z) = v_xba
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| v_xba = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(v_x,v_z,v_xba),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(v_x,v_z,v_xba),v_z))
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1829,f1505]) ).
fof(f1833,plain,
( spl0_14
| spl0_15
| spl0_16
| spl0_19 ),
inference(avatar_split_clause,[],[f1831,f1782,f1742,f1738,f1734]) ).
fof(f1835,definition,
( spl0_31
<=> v_xba = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(v_x,v_z,v_xba),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(v_x,v_z,v_xba),v_z)) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f1836,plain,
( v_xba != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(v_x,v_z,v_xba),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(v_x,v_z,v_xba),v_z))
| spl0_31 ),
inference(avatar_component_clause,[],[f1835]) ).
fof(f1837,plain,
( v_xba = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(v_x,v_z,v_xba),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(v_x,v_z,v_xba),v_z))
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f1835]) ).
fof(f1838,plain,
( spl0_31
| spl0_15
| spl0_16
| spl0_19 ),
inference(avatar_split_clause,[],[f1832,f1782,f1742,f1738,f1835]) ).
fof(f1891,definition,
( spl0_38
<=> ! [X0] :
( ~ c_in(c_Pair(v_sko__uTI(v_x,v_z,v_xba),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_ya,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f1892,plain,
( ! [X0] :
( ~ c_in(c_Pair(v_sko__uTI(v_x,v_z,v_xba),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_ya,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f1891]) ).
fof(f2000,plain,
( ! [X0,X1] :
( c_in(c_Pair(v_xba,c_Comb_Ocomb_Oop_A_D_D(X0,X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_x,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_z,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )
| ~ spl0_16 ),
inference(superposition,[],[f32,f1744]) ).
fof(f2013,plain,
( ~ c_in(c_Pair(v_x,v_ya,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_z,v_w,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_16 ),
inference(resolution,[],[f2000,f1512]) ).
fof(f2024,plain,
( ~ c_in(c_Pair(v_z,v_w,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2013,f1503]) ).
fof(f2025,plain,
( $false
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2024,f1504]) ).
fof(f2026,plain,
~ spl0_16,
inference(avatar_contradiction_clause,[],[f2025]) ).
fof(f2239,plain,
( ! [X0] :
( ~ c_in(c_Pair(v_sko__uTI(v_x,v_z,v_xba),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_w,v_xaa(v_sko__uTH(v_x,v_z,v_xba)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_ya,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )
| ~ spl0_20 ),
inference(resolution,[],[f1787,f1513]) ).
fof(f2241,definition,
( spl0_82
<=> c_in(c_Pair(v_w,v_xaa(v_sko__uTH(v_x,v_z,v_xba)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f2243,plain,
( ~ c_in(c_Pair(v_w,v_xaa(v_sko__uTH(v_x,v_z,v_xba)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| spl0_82 ),
inference(avatar_component_clause,[],[f2241]) ).
fof(f2244,plain,
( ~ spl0_82
| spl0_38
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f2239,f1786,f1891,f2241]) ).
fof(f2245,plain,
( ~ c_in(c_Pair(v_z,v_sko__uTH(v_x,v_z,v_xba),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| spl0_82 ),
inference(resolution,[],[f2243,f1508]) ).
fof(f2246,plain,
( $false
| ~ spl0_19
| spl0_82 ),
inference(forward_subsumption_resolution,[],[f2245,f1783]) ).
fof(f2247,plain,
( ~ spl0_19
| spl0_82 ),
inference(avatar_contradiction_clause,[],[f2246]) ).
fof(f2250,plain,
( ! [X0] :
( ~ c_in(c_Pair(v_x,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(v_xba,X0)) = X0 )
| ~ spl0_15 ),
inference(superposition,[],[f16,f1740]) ).
fof(f2251,plain,
( ! [X0] :
( c_in(c_Pair(v_xba,v_sko__uTE(v_xba,X0),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_x,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )
| ~ spl0_15 ),
inference(superposition,[],[f17,f1740]) ).
fof(f2322,plain,
( v_ya = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(v_xba,v_ya))
| ~ spl0_15 ),
inference(resolution,[],[f2250,f1503]) ).
fof(f2358,plain,
( ~ c_in(c_Pair(v_ya,v_xb(v_sko__uTI(v_x,v_z,v_xba)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_x,v_sko__uTI(v_x,v_z,v_xba),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_38 ),
inference(resolution,[],[f1892,f1507]) ).
fof(f2369,plain,
( ~ c_in(c_Pair(v_x,v_sko__uTI(v_x,v_z,v_xba),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2358,f1506]) ).
fof(f2406,plain,
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),v_xba,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(v_x,v_z) = v_xba
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| v_xba = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(v_x,v_z,v_xba),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(v_x,v_z,v_xba),v_z))
| ~ spl0_38 ),
inference(resolution,[],[f2369,f12]) ).
fof(f2474,plain,
( ! [X0] : c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,X0),v_sko__uTE(v_xba,v_ya),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_15 ),
inference(superposition,[],[f30,f2322]) ).
fof(f2494,plain,
( ~ c_in(c_Pair(v_xba,v_sko__uTE(v_xba,v_ya),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_15 ),
inference(resolution,[],[f2474,f1510]) ).
fof(f2496,plain,
( ~ c_in(c_Pair(v_x,v_ya,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_15 ),
inference(resolution,[],[f2494,f2251]) ).
fof(f2497,plain,
( $false
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f2496,f1503]) ).
fof(f2498,plain,
~ spl0_15,
inference(avatar_contradiction_clause,[],[f2497]) ).
fof(f2978,plain,
( c_Comb_Ocomb_Oop_A_D_D(v_x,v_z) = v_xba
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| v_xba = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(v_x,v_z,v_xba),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(v_x,v_z,v_xba),v_z))
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2406,f1505]) ).
fof(f2980,plain,
( v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| v_xba = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(v_x,v_z,v_xba),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(v_x,v_z,v_xba),v_z))
| spl0_16
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2978,f1743]) ).
fof(f2982,plain,
( v_xba = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(v_x,v_z,v_xba),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(v_x,v_z,v_xba),v_z))
| spl0_15
| spl0_16
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2980,f1739]) ).
fof(f2984,plain,
( $false
| spl0_15
| spl0_16
| spl0_31
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2982,f1836]) ).
fof(f2985,plain,
( spl0_15
| spl0_16
| spl0_31
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f2984]) ).
fof(f3284,plain,
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),v_xba,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(v_x,v_z) = v_xba
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(v_x,v_z,v_xba)),v_sko__uTG(v_x,v_z,v_xba))
| ~ spl0_38 ),
inference(resolution,[],[f2369,f6]) ).
fof(f3285,plain,
( c_Comb_Ocomb_Oop_A_D_D(v_x,v_z) = v_xba
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(v_x,v_z,v_xba)),v_sko__uTG(v_x,v_z,v_xba))
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f3284,f1505]) ).
fof(f3286,plain,
( v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(v_x,v_z,v_xba)),v_sko__uTG(v_x,v_z,v_xba))
| spl0_16
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f3285,f1743]) ).
fof(f3287,plain,
( v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(v_x,v_z,v_xba)),v_sko__uTG(v_x,v_z,v_xba))
| spl0_15
| spl0_16
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f3286,f1739]) ).
fof(f3288,plain,
( $false
| spl0_14
| spl0_15
| spl0_16
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f3287,f1735]) ).
fof(f3289,plain,
( spl0_14
| spl0_15
| spl0_16
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f3288]) ).
fof(f3368,plain,
( ! [X0] :
( ~ c_in(c_Pair(v_x,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),X0)),v_sko__uTC(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),X0)) = X0 )
| ~ spl0_14 ),
inference(superposition,[],[f24,f1736]) ).
fof(f3369,plain,
( ! [X0] :
( c_in(c_Pair(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTB(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),X0),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_x,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )
| ~ spl0_14 ),
inference(superposition,[],[f25,f1736]) ).
fof(f3370,plain,
( ! [X0] :
( c_in(c_Pair(v_sko__uTG(v_x,v_z,v_xba),v_sko__uTC(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),X0),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_x,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )
| ~ spl0_14 ),
inference(superposition,[],[f26,f1736]) ).
fof(f3424,plain,
( ! [X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(v_x,v_z,v_xba),v_z),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(v_x,v_z,v_xba),v_z),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(v_xba,c_Comb_Ocomb_Oop_A_D_D(X0,X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )
| ~ spl0_31 ),
inference(superposition,[],[f32,f1837]) ).
fof(f3488,plain,
( v_ya = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya)),v_sko__uTC(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya))
| ~ spl0_14 ),
inference(resolution,[],[f3368,f1503]) ).
fof(f3511,plain,
( ! [X0] : c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,X0),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTB(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya),X0),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTC(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya),X0)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_14 ),
inference(superposition,[],[f31,f3488]) ).
fof(f3562,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(v_x,v_z,v_xba),v_z),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(v_xba,c_Comb_Ocomb_Oop_A_D_D(X0,c_Comb_Ocomb_Oop_A_D_D(X1,X2)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_sko__uTG(v_x,v_z,v_xba),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_z,X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )
| ~ spl0_31 ),
inference(resolution,[],[f3424,f32]) ).
fof(f3578,plain,
( ! [X2,X3,X0,X1] :
( c_in(c_Pair(v_xba,c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(X0,X1),c_Comb_Ocomb_Oop_A_D_D(X2,X3)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_sko__uTG(v_x,v_z,v_xba),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_z,X3,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_sko__uTF(v_x,v_z,v_xba),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_z,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )
| ~ spl0_31 ),
inference(resolution,[],[f3562,f32]) ).
fof(f3596,plain,
( ~ c_in(c_Pair(v_xba,c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTB(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya),v_w),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTC(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya),v_w)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_14 ),
inference(resolution,[],[f3511,f1510]) ).
fof(f3742,plain,
( ~ c_in(c_Pair(v_sko__uTG(v_x,v_z,v_xba),v_sko__uTC(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_z,v_w,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTB(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_z,v_w,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_14
| ~ spl0_31 ),
inference(resolution,[],[f3578,f3596]) ).
fof(f3760,plain,
( ~ c_in(c_Pair(v_sko__uTG(v_x,v_z,v_xba),v_sko__uTC(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_z,v_w,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTB(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_14
| ~ spl0_31 ),
inference(duplicate_literal_removal,[],[f3742]) ).
fof(f3787,plain,
( ~ c_in(c_Pair(v_sko__uTG(v_x,v_z,v_xba),v_sko__uTC(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTB(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_14
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f3760,f1504]) ).
fof(f3799,definition,
( spl0_244
<=> c_in(c_Pair(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTB(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
introduced(definition,[new_symbols(definition,[spl0_244])],[avatar_definition]) ).
fof(f3801,plain,
( ~ c_in(c_Pair(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTB(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| spl0_244 ),
inference(avatar_component_clause,[],[f3799]) ).
fof(f3803,definition,
( spl0_245
<=> c_in(c_Pair(v_sko__uTG(v_x,v_z,v_xba),v_sko__uTC(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
introduced(definition,[new_symbols(definition,[spl0_245])],[avatar_definition]) ).
fof(f3805,plain,
( ~ c_in(c_Pair(v_sko__uTG(v_x,v_z,v_xba),v_sko__uTC(v_sko__uTF(v_x,v_z,v_xba),v_sko__uTG(v_x,v_z,v_xba),v_ya),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| spl0_245 ),
inference(avatar_component_clause,[],[f3803]) ).
fof(f3806,plain,
( ~ spl0_244
| ~ spl0_245
| ~ spl0_14
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f3787,f1835,f1734,f3803,f3799]) ).
fof(f3815,plain,
( ~ c_in(c_Pair(v_x,v_ya,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_14
| spl0_245 ),
inference(resolution,[],[f3805,f3370]) ).
fof(f3816,plain,
( $false
| ~ spl0_14
| spl0_245 ),
inference(forward_subsumption_resolution,[],[f3815,f1503]) ).
fof(f3817,plain,
( ~ spl0_14
| spl0_245 ),
inference(avatar_contradiction_clause,[],[f3816]) ).
fof(f3818,plain,
( ~ c_in(c_Pair(v_x,v_ya,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_14
| spl0_244 ),
inference(resolution,[],[f3801,f3369]) ).
fof(f3819,plain,
( $false
| ~ spl0_14
| spl0_244 ),
inference(forward_subsumption_resolution,[],[f3818,f1503]) ).
fof(f3820,plain,
( ~ spl0_14
| spl0_244 ),
inference(avatar_contradiction_clause,[],[f3819]) ).
fof(f4287,plain,
( c_Comb_Ocomb_Oop_A_D_D(v_x,v_z) = v_xba
| v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| v_xba = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(v_x,v_z,v_xba),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(v_x,v_z,v_xba),v_z))
| v_xba = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(v_x,v_z,v_xba),v_sko__uTH(v_x,v_z,v_xba)) ),
inference(resolution,[],[f8,f1505]) ).
fof(f4317,plain,
( v_x = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xba)
| v_xba = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(v_x,v_z,v_xba),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(v_x,v_z,v_xba),v_z))
| v_xba = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(v_x,v_z,v_xba),v_sko__uTH(v_x,v_z,v_xba))
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f4287,f1743]) ).
fof(f4320,plain,
( v_xba = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(v_x,v_z,v_xba),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(v_x,v_z,v_xba),v_z))
| v_xba = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(v_x,v_z,v_xba),v_sko__uTH(v_x,v_z,v_xba))
| spl0_15
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f4317,f1739]) ).
fof(f4323,plain,
( v_xba = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(v_x,v_z,v_xba),v_sko__uTH(v_x,v_z,v_xba))
| spl0_15
| spl0_16
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f4320,f1836]) ).
fof(f4326,plain,
( $false
| spl0_13
| spl0_15
| spl0_16
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f4323,f1731]) ).
fof(f4327,plain,
( spl0_13
| spl0_15
| spl0_16
| spl0_31 ),
inference(avatar_contradiction_clause,[],[f4326]) ).
cnf(s7,plain,
( spl0_13
| spl0_14
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f1745]) ).
cnf(s9,plain,
( ~ spl0_13
| ~ spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f1788]) ).
cnf(s15,plain,
( spl0_14
| spl0_15
| spl0_16
| spl0_19 ),
inference(sat_conversion,[],[f1833]) ).
cnf(s16,plain,
( spl0_15
| spl0_16
| spl0_19
| spl0_31 ),
inference(sat_conversion,[],[f1838]) ).
cnf(s34,plain,
~ spl0_16,
inference(sat_conversion,[],[f2026]) ).
cnf(s52,plain,
( ~ spl0_20
| spl0_38
| ~ spl0_82 ),
inference(sat_conversion,[],[f2244]) ).
cnf(s53,plain,
( ~ spl0_19
| spl0_82 ),
inference(sat_conversion,[],[f2247]) ).
cnf(s66,plain,
~ spl0_15,
inference(sat_conversion,[],[f2498]) ).
cnf(s98,plain,
( spl0_15
| spl0_16
| spl0_31
| ~ spl0_38 ),
inference(sat_conversion,[],[f2985]) ).
cnf(s119,plain,
( spl0_14
| spl0_15
| spl0_16
| ~ spl0_38 ),
inference(sat_conversion,[],[f3289]) ).
cnf(s134,plain,
( ~ spl0_14
| ~ spl0_31
| ~ spl0_244
| ~ spl0_245 ),
inference(sat_conversion,[],[f3806]) ).
cnf(s135,plain,
( ~ spl0_14
| spl0_245 ),
inference(sat_conversion,[],[f3817]) ).
cnf(s136,plain,
( ~ spl0_14
| spl0_244 ),
inference(sat_conversion,[],[f3820]) ).
cnf(s167,plain,
( spl0_13
| spl0_15
| spl0_16
| spl0_31 ),
inference(sat_conversion,[],[f4327]) ).
cnf(s171,plain,
( spl0_19
| spl0_31 ),
inference(rat,[],[s16,s34,s66]) ).
cnf(s172,plain,
( spl0_14
| spl0_19 ),
inference(rat,[],[s15,s34,s66]) ).
cnf(s173,plain,
( spl0_13
| spl0_14 ),
inference(rat,[],[s7,s34,s66]) ).
cnf(s174,plain,
spl0_13,
inference(rat,[],[s134,s135,s136,s173,s167,s66,s34]) ).
cnf(s175,plain,
spl0_31,
inference(rat,[],[s52,s9,s53,s171,s98,s174,s66,s34]) ).
cnf(s176,plain,
~ spl0_14,
inference(rat,[],[s134,s135,s136,s175]) ).
cnf(s177,plain,
~ spl0_38,
inference(rat,[],[s119,s34,s66,s176]) ).
cnf(s178,plain,
spl0_19,
inference(rat,[],[s172,s176]) ).
cnf(s181,plain,
spl0_82,
inference(rat,[],[s53,s178]) ).
cnf(s182,plain,
spl0_20,
inference(rat,[],[s9,s174,s178]) ).
cnf(s183,plain,
$false,
inference(rat,[],[s52,s177,s181,s182]) ).
fof(f4339,plain,
$false,
inference(avatar_sat_refutation,[],[s183]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COL108-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n019.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 21:40:03 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.25 Running first-order theorem proving
% 0.08/0.25 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
% 12.41/2.42 % (303455)Input is clausal, will run a generic CNF schedule.
% 12.41/2.42 % (303462)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=329546502:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.41/2.42 % (303460)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=1608520497:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.41/2.42 % (303464)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2743339828:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.41/2.42 % (303463)lrs+10_1_sil=8000:sp=occurrence:random_seed=3276688939:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.41/2.42 % (303461)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4124417626:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.41/2.42 % (303466)dis-21_1_sil=8000:lcm=predicate:random_seed=515882121: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)
% 12.41/2.42 % (303465)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3703684906:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.41/2.42 % (303463)Refutation not found, incomplete strategy
% 12.41/2.42 % (303463)------------------------------
% 12.41/2.42 % (303463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.41/2.42 % (303463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.41/2.42 % (303463)CaDiCaL version: 2.1.3
% 12.41/2.42 % (303463)Termination reason: Refutation not found, incomplete strategy
% 12.41/2.42 % (303463)Time elapsed: 0.004 s
% 12.41/2.42 % (303463)Peak memory usage: 89 MB
% 12.41/2.42 % (303463)Instructions burned: 4 (million)
% 12.41/2.42 % (303464)Refutation not found, incomplete strategy
% 12.41/2.42 % (303464)------------------------------
% 12.41/2.42 % (303464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.41/2.42 % (303464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.41/2.42 % (303464)CaDiCaL version: 2.1.3
% 12.41/2.42 % (303464)Termination reason: Refutation not found, incomplete strategy
% 12.41/2.42 % (303464)Time elapsed: 0.005 s
% 12.41/2.42 % (303464)Peak memory usage: 89 MB
% 12.41/2.42 % (303464)Instructions burned: 7 (million)
% 12.41/2.42 % (303466)Instruction limit reached!
% 12.41/2.42 % (303466)------------------------------
% 12.41/2.42 % (303466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.41/2.42 % (303466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.41/2.42 % (303466)CaDiCaL version: 2.1.3
% 12.41/2.42 % (303466)Termination reason: Instruction limit
% 12.41/2.42 % (303466)Termination phase: Saturation
% 12.41/2.42 % (303466)Time elapsed: 0.067 s
% 12.41/2.42 % (303466)Peak memory usage: 89 MB
% 12.41/2.42 % (303466)Instructions burned: 119 (million)
% 12.41/2.42 % (303465)Instruction limit reached!
% 12.41/2.42 % (303465)------------------------------
% 12.41/2.42 % (303465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.41/2.42 % (303465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.41/2.42 % (303465)CaDiCaL version: 2.1.3
% 12.41/2.42 % (303465)Termination reason: Instruction limit
% 12.41/2.42 % (303465)Termination phase: Saturation
% 12.41/2.42 % (303465)Time elapsed: 0.099 s
% 12.41/2.42 % (303465)Peak memory usage: 90 MB
% 12.41/2.42 % (303465)Instructions burned: 180 (million)
% 12.41/2.42 % (303474)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=1599340506:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 12.41/2.42 % (303474)Refutation not found, incomplete strategy
% 12.41/2.42 % (303474)------------------------------
% 12.41/2.42 % (303474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.41/2.42 % (303474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.41/2.42 % (303474)CaDiCaL version: 2.1.3
% 12.41/2.42 % (303474)Termination reason: Refutation not found, incomplete strategy
% 12.41/2.42 % (303474)Time elapsed: 0.004 s
% 12.41/2.42 % (303474)Peak memory usage: 89 MB
% 12.41/2.42 % (303474)Instructions burned: 4 (million)
% 12.41/2.42 % (303464)------------------------------
% 12.41/2.42 % (303464)------------------------------
% 15.31/2.87 % (303463)------------------------------
% 15.31/2.87 % (303463)------------------------------
% 15.31/2.87 % (303475)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3493121405:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 15.31/2.87 % (303475)Instruction limit reached!
% 15.31/2.87 % (303475)------------------------------
% 15.31/2.87 % (303475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.31/2.87 % (303475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.31/2.87 % (303475)CaDiCaL version: 2.1.3
% 15.31/2.87 % (303475)Termination reason: Instruction limit
% 15.31/2.87 % (303475)Termination phase: Saturation
% 15.31/2.87 % (303475)Time elapsed: 0.103 s
% 15.31/2.87 % (303475)Peak memory usage: 91 MB
% 15.31/2.87 % (303475)Instructions burned: 191 (million)
% 15.31/2.87 % (303479)lrs+10_64_to=lpo:sil=8000:random_seed=1439233749:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 15.31/2.87 % (303478)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3066867122:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 15.31/2.87 % (303478)Refutation not found, incomplete strategy
% 15.31/2.87 % (303478)------------------------------
% 15.31/2.87 % (303478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.31/2.87 % (303478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.31/2.87 % (303478)CaDiCaL version: 2.1.3
% 15.31/2.87 % (303478)Termination reason: Refutation not found, incomplete strategy
% 15.31/2.87 % (303478)Time elapsed: 0.006 s
% 15.31/2.87 % (303478)Peak memory usage: 88 MB
% 15.31/2.87 % (303478)Instructions burned: 10 (million)
% 15.31/2.87 % (303474)------------------------------
% 15.31/2.87 % (303474)------------------------------
% 15.31/2.87 % (303479)Instruction limit reached!
% 15.31/2.87 % (303479)------------------------------
% 15.31/2.87 % (303479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.31/2.87 % (303479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.31/2.87 % (303479)CaDiCaL version: 2.1.3
% 15.31/2.87 % (303479)Termination reason: Instruction limit
% 15.31/2.87 % (303479)Termination phase: Saturation
% 15.31/2.87 % (303479)Time elapsed: 0.079 s
% 15.31/2.87 % (303479)Peak memory usage: 89 MB
% 15.31/2.87 % (303479)Instructions burned: 126 (million)
% 15.31/2.87 % (303480)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3782715644:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 15.31/2.87 % (303483)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4240457995:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 15.31/2.87 % (303484)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1765821488:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 15.31/2.87 % (303478)------------------------------
% 15.31/2.87 % (303478)------------------------------
% 15.31/2.87 % (303480)Instruction limit reached!
% 15.31/2.87 % (303480)------------------------------
% 15.31/2.87 % (303480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.31/2.87 % (303480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.31/2.87 % (303480)CaDiCaL version: 2.1.3
% 15.31/2.87 % (303480)Termination reason: Instruction limit
% 15.31/2.87 % (303480)Termination phase: Saturation
% 15.31/2.87 % (303480)Time elapsed: 0.127 s
% 15.31/2.87 % (303480)Peak memory usage: 90 MB
% 15.31/2.87 % (303480)Instructions burned: 194 (million)
% 15.31/2.87 % (303483)Instruction limit reached!
% 15.31/2.87 % (303483)------------------------------
% 15.31/2.87 % (303483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.31/2.87 % (303483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.31/2.87 % (303483)CaDiCaL version: 2.1.3
% 15.31/2.87 % (303483)Termination reason: Instruction limit
% 15.31/2.87 % (303483)Termination phase: Saturation
% 15.31/2.87 % (303483)Time elapsed: 0.091 s
% 15.31/2.87 % (303483)Peak memory usage: 91 MB
% 15.31/2.87 % (303483)Instructions burned: 157 (million)
% 15.31/2.87 % (303489)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1584207671:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 15.31/2.87 % (303488)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=2883049025:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 15.31/2.87 % (303488)Instruction limit reached!
% 15.31/2.87 % (303488)------------------------------
% 15.31/2.87 % (303488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.31/2.87 % (303488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.31/2.87 % (303488)CaDiCaL version: 2.1.3
% 15.31/2.87 % (303488)Termination reason: Instruction limit
% 15.31/2.87 % (303488)Termination phase: Saturation
% 15.31/2.87 % (303488)Time elapsed: 0.053 s
% 15.31/2.87 % (303488)Peak memory usage: 89 MB
% 15.31/2.87 % (303488)Instructions burned: 106 (million)
% 15.31/2.87 % (303489)Instruction limit reached!
% 15.31/2.87 % (303489)------------------------------
% 15.31/2.87 % (303489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.31/2.87 % (303489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.31/2.87 % (303489)CaDiCaL version: 2.1.3
% 15.31/2.87 % (303489)Termination reason: Instruction limit
% 15.31/2.87 % (303489)Termination phase: Saturation
% 15.31/2.87 % (303489)Time elapsed: 0.069 s
% 15.31/2.87 % (303489)Peak memory usage: 90 MB
% 15.31/2.87 % (303489)Instructions burned: 109 (million)
% 15.31/2.87 % (303490)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=753456206:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 15.31/2.87 % (303490)Instruction limit reached!
% 15.31/2.87 % (303490)------------------------------
% 15.31/2.87 % (303490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.31/2.87 % (303490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.31/2.87 % (303490)CaDiCaL version: 2.1.3
% 15.31/2.87 % (303490)Termination reason: Instruction limit
% 15.31/2.87 % (303490)Termination phase: Saturation
% 15.31/2.87 % (303490)Time elapsed: 0.128 s
% 15.31/2.87 % (303490)Peak memory usage: 89 MB
% 15.31/2.87 % (303490)Instructions burned: 244 (million)
% 15.31/2.87 % (303493)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3592233461:cond=fast:i=5208:av=off_2989 on theBenchmark for (2989ds/5208Mi)
% 15.31/2.87 % (303495)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1397977226:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 15.31/2.87 % (303495)Refutation not found, incomplete strategy
% 15.31/2.87 % (303495)------------------------------
% 15.31/2.87 % (303495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.31/2.87 % (303495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.31/2.87 % (303495)CaDiCaL version: 2.1.3
% 15.31/2.87 % (303495)Termination reason: Refutation not found, incomplete strategy
% 15.31/2.87 % (303495)Time elapsed: 0.004 s
% 15.31/2.87 % (303495)Peak memory usage: 89 MB
% 15.31/2.87 % (303495)Instructions burned: 4 (million)
% 15.31/2.87 % (303497)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=16564151:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 15.31/2.87 % (303495)------------------------------
% 15.31/2.87 % (303495)------------------------------
% 15.31/2.87 % (303497)Instruction limit reached!
% 15.31/2.87 % (303497)------------------------------
% 15.31/2.87 % (303497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.31/2.87 % (303497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.31/2.87 % (303497)CaDiCaL version: 2.1.3
% 15.31/2.87 % (303497)Termination reason: Instruction limit
% 15.31/2.87 % (303497)Termination phase: Saturation
% 15.31/2.87 % (303497)Time elapsed: 0.259 s
% 15.31/2.87 % (303497)Peak memory usage: 98 MB
% 15.31/2.87 % (303497)Instructions burned: 499 (million)
% 15.31/2.87 % (303500)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=357873623:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 15.31/2.87 % (303500)Instruction limit reached!
% 15.31/2.87 % (303500)------------------------------
% 15.31/2.87 % (303500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.31/2.87 % (303500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.31/2.87 % (303500)CaDiCaL version: 2.1.3
% 15.31/2.87 % (303500)Termination reason: Instruction limit
% 15.31/2.87 % (303500)Termination phase: Saturation
% 15.31/2.87 % (303500)Time elapsed: 0.134 s
% 15.31/2.87 % (303500)Peak memory usage: 92 MB
% 15.31/2.87 % (303500)Instructions burned: 191 (million)
% 15.31/2.87 % (303501)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1511975020:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 15.31/2.87 % (303501)Instruction limit reached!
% 15.31/2.87 % (303501)------------------------------
% 15.31/2.87 % (303501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.31/2.87 % (303501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.31/2.87 % (303501)CaDiCaL version: 2.1.3
% 15.31/2.87 % (303501)Termination reason: Instruction limit
% 15.31/2.87 % (303501)Termination phase: Saturation
% 15.31/2.87 % (303501)Time elapsed: 0.147 s
% 15.31/2.87 % (303501)Peak memory usage: 92 MB
% 15.31/2.87 % (303501)Instructions burned: 264 (million)
% 15.31/2.87 % (303504)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1415634483:cond=on:i=156:bs=on:gtg=exists_all:er=known_2982 on theBenchmark for (2982ds/156Mi)
% 15.31/2.87 % (303484)First to succeed.
% 15.31/2.87 % (303484)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-303455"
% 15.31/2.87 % (303504)Instruction limit reached!
% 15.31/2.87 % (303504)------------------------------
% 15.31/2.87 % (303504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.31/2.87 % (303504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.31/2.87 % (303504)CaDiCaL version: 2.1.3
% 15.31/2.87 % (303504)Termination reason: Instruction limit
% 15.31/2.87 % (303504)Termination phase: Saturation
% 15.31/2.87 % (303504)Time elapsed: 0.095 s
% 15.31/2.87 % (303504)Peak memory usage: 90 MB
% 15.31/2.87 % (303504)Instructions burned: 156 (million)
% 15.31/2.87 % (303505)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3276352086:i=3256:kws=precedence:bd=preordered:av=off_2980 on theBenchmark for (2980ds/3256Mi)
% 15.31/2.87 % (303507)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=969471988:i=537:av=off:ss=included_2979 on theBenchmark for (2979ds/537Mi)
% 15.31/2.87 % (303484)Refutation found. Thanks to Tanya!
% 15.31/2.87 % SZS status Unsatisfiable for theBenchmark
% 15.31/2.87 % SZS output start Proof for theBenchmark
% See solution above
% 16.30/3.06 % (303484)------------------------------
% 16.30/3.06 % (303484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.30/3.06 % (303484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.30/3.06 % (303484)CaDiCaL version: 2.1.3
% 16.30/3.06 % (303484)Termination reason: Refutation
% 16.30/3.06 % (303484)Time elapsed: 1.136 s
% 16.30/3.06 % (303484)Peak memory usage: 137 MB
% 16.30/3.06 % (303484)Instructions burned: 1792 (million)
% 16.30/3.06 % (303484)------------------------------
% 16.30/3.06 % (303484)------------------------------
% 16.30/3.06 % (303455)Success in time 2.247 s
% 16.30/3.06 % Vampire exiting
%------------------------------------------------------------------------------