%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COL107-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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 66.67s 10.12s
% Output : Refutation 67.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 29
% Syntax : Number of formulae : 177 ( 16 unt; 12 def)
% Number of atoms : 538 ( 171 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 530 ( 169 ~; 349 |; 0 &)
% ( 12 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 15 ( 13 usr; 13 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 8 con; 0-4 aty)
% Number of variables : 90 ( 0 sgn 90 !; 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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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(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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',cls_Comb_Oparcontract_Ointros__1_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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',cls_Comb_Oparcontract_Ointros__4_0) ).
fof(f58,axiom,
! [X0,X1] : c_Comb_Ocomb_OK != c_Comb_Ocomb_Oop_A_D_D(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Ocomb_Odistinct__3__iff1_0) ).
fof(f59,plain,
! [X0,X1] : c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_OK,
inference(reorient_equations,[],[f58]) ).
fof(f64,axiom,
! [X2,X3,X0,X1] :
( c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_Oop_A_D_D(X2,X3)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Ocomb_Oinject__iff1_0) ).
fof(f65,axiom,
! [X2,X3,X0,X1] :
( c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_Oop_A_D_D(X2,X3)
| X1 = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Ocomb_Oinject__iff1_1) ).
fof(f1503,negated_conjecture,
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,v_x),v_ya),v_z),v_xb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1504,negated_conjecture,
! [X0] :
( ~ c_in(c_Pair(v_xb,X0,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(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z)),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1506,plain,
~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z)),v_xb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(resolution,[],[f1504,f29]) ).
fof(f1533,plain,
! [X2,X3,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),X3,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_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2) = X3
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X3)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2,X3),X2),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2,X3),X2)) = X3
| v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2,X3) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(X0,X1,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2,X3))),v_sko__uTC(X0,X1,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2,X3))) ),
inference(resolution,[],[f12,f24]) ).
fof(f1536,plain,
( 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,v_x),v_ya),v_z) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| v_xb = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)) ),
inference(resolution,[],[f8,f1503]) ).
fof(f1545,definition,
( spl0_1
<=> v_xb = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f1547,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f1545]) ).
fof(f1549,definition,
( spl0_2
<=> v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f1550,plain,
( v_xb != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| spl0_2 ),
inference(avatar_component_clause,[],[f1549]) ).
fof(f1551,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f1549]) ).
fof(f1553,definition,
( spl0_3
<=> c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f1554,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| spl0_3 ),
inference(avatar_component_clause,[],[f1553]) ).
fof(f1555,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f1553]) ).
fof(f1557,definition,
( spl0_4
<=> 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,v_x),v_ya),v_z) = v_xb ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f1558,plain,
( 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,v_x),v_ya),v_z) != v_xb
| spl0_4 ),
inference(avatar_component_clause,[],[f1557]) ).
fof(f1559,plain,
( 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,v_x),v_ya),v_z) = v_xb
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f1557]) ).
fof(f1560,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f1536,f1557,f1553,f1549,f1545]) ).
fof(f1579,definition,
( spl0_6
<=> v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_z,v_xb),v_z)) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f1580,plain,
( v_xb != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_z,v_xb),v_z))
| spl0_6 ),
inference(avatar_component_clause,[],[f1579]) ).
fof(f1581,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_z,v_xb),v_z))
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f1579]) ).
fof(f1815,plain,
! [X2,X3,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),X3,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_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2) = X3
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X3)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2,X3)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2,X3))
| v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2,X3) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(X0,X1,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2,X3))),v_sko__uTC(X0,X1,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,X0),X1),X2,X3))) ),
inference(resolution,[],[f6,f24]) ).
fof(f1844,plain,
( 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,v_x),v_ya),v_z) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))),v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))) ),
inference(resolution,[],[f1815,f1503]) ).
fof(f1858,definition,
( spl0_12
<=> v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))),v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f1860,plain,
( v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))),v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)))
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f1858]) ).
fof(f1862,definition,
( spl0_13
<=> c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f1863,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| spl0_13 ),
inference(avatar_component_clause,[],[f1862]) ).
fof(f1864,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f1862]) ).
fof(f1865,plain,
( spl0_12
| spl0_13
| spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f1844,f1557,f1553,f1862,f1858]) ).
fof(f2466,plain,
( 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,v_x),v_ya),v_z) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| v_xb = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)) ),
inference(resolution,[],[f2,f1503]) ).
fof(f2501,plain,
( 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,v_x),v_ya),v_z) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| v_xb = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f2466,f1863]) ).
fof(f2502,plain,
( spl0_1
| spl0_3
| spl0_4
| spl0_13 ),
inference(avatar_split_clause,[],[f2501,f1862,f1557,f1553,f1545]) ).
fof(f2508,plain,
( c_in(c_Pair(v_xb,c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_4 ),
inference(superposition,[],[f31,f1559]) ).
fof(f2711,plain,
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z)),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_4 ),
inference(resolution,[],[f2508,f1504]) ).
fof(f2712,plain,
( $false
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f2711,f29]) ).
fof(f2713,plain,
~ spl0_4,
inference(avatar_contradiction_clause,[],[f2712]) ).
fof(f3092,plain,
( ! [X0,X1] :
( c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x) = X0 )
| ~ spl0_3 ),
inference(superposition,[],[f64,f1555]) ).
fof(f3094,plain,
( ! [X0,X1] :
( c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| v_ya = X1 )
| ~ spl0_3 ),
inference(superposition,[],[f65,f1555]) ).
fof(f3103,plain,
( v_ya = v_xb
| ~ spl0_3 ),
inference(equality_resolution,[],[f3094]) ).
fof(f3309,plain,
( ! [X0,X1] :
( c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_ya)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x) = X0 )
| ~ spl0_3 ),
inference(backward_demodulation,[],[f3092,f3103]) ).
fof(f3587,plain,
( c_Comb_Ocomb_OK = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x)
| ~ spl0_3 ),
inference(equality_resolution,[],[f3309]) ).
fof(f3588,plain,
( $false
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f3587,f59]) ).
fof(f3589,plain,
~ spl0_3,
inference(avatar_contradiction_clause,[],[f3588]) ).
fof(f3922,plain,
( ! [X0,X1] :
( c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)) = X0 )
| ~ spl0_13 ),
inference(superposition,[],[f64,f1864]) ).
fof(f3924,plain,
( ! [X0,X1] :
( c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya)
| v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb) = X1 )
| ~ spl0_13 ),
inference(superposition,[],[f65,f1864]) ).
fof(f3936,plain,
( v_ya = v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)
| ~ spl0_13 ),
inference(equality_resolution,[],[f3924]) ).
fof(f4175,plain,
( ! [X0] : c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),X0),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),X0),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),X0)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_12 ),
inference(superposition,[],[f31,f1860]) ).
fof(f4307,plain,
( c_in(c_Pair(v_xb,c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_1
| ~ spl0_12 ),
inference(superposition,[],[f4175,f1547]) ).
fof(f4308,plain,
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z)),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_1
| ~ spl0_12 ),
inference(resolution,[],[f4307,f1504]) ).
fof(f4309,plain,
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),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_ya,v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_1
| ~ spl0_12 ),
inference(resolution,[],[f4308,f32]) ).
fof(f4311,definition,
( spl0_40
<=> c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f4313,plain,
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| spl0_40 ),
inference(avatar_component_clause,[],[f4311]) ).
fof(f4315,definition,
( spl0_41
<=> c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f4317,plain,
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| spl0_41 ),
inference(avatar_component_clause,[],[f4315]) ).
fof(f4318,plain,
( ~ spl0_40
| ~ spl0_41
| ~ spl0_1
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f4309,f1858,f1545,f4315,f4311]) ).
fof(f4319,plain,
( ~ c_in(c_Pair(v_ya,v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),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(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| spl0_40 ),
inference(resolution,[],[f4313,f32]) ).
fof(f4321,definition,
( spl0_42
<=> c_in(c_Pair(v_z,v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f4322,plain,
( c_in(c_Pair(v_z,v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f4321]) ).
fof(f4323,plain,
( ~ c_in(c_Pair(v_z,v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| spl0_42 ),
inference(avatar_component_clause,[],[f4321]) ).
fof(f4325,definition,
( spl0_43
<=> c_in(c_Pair(v_ya,v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f4327,plain,
( ~ c_in(c_Pair(v_ya,v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| spl0_43 ),
inference(avatar_component_clause,[],[f4325]) ).
fof(f4328,plain,
( ~ spl0_42
| ~ spl0_43
| spl0_40 ),
inference(avatar_split_clause,[],[f4319,f4311,f4325,f4321]) ).
fof(f4329,plain,
( ~ 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,v_x),v_ya),v_z),v_xb,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_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| spl0_42 ),
inference(resolution,[],[f4323,f4]) ).
fof(f4332,plain,
( 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,v_x),v_ya),v_z) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| spl0_42 ),
inference(forward_subsumption_resolution,[],[f4329,f1503]) ).
fof(f4334,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| spl0_4
| spl0_42 ),
inference(forward_subsumption_resolution,[],[f4332,f1558]) ).
fof(f4336,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| spl0_3
| spl0_4
| spl0_42 ),
inference(forward_subsumption_resolution,[],[f4334,f1554]) ).
fof(f4338,plain,
( $false
| spl0_3
| spl0_4
| spl0_13
| spl0_42 ),
inference(forward_subsumption_resolution,[],[f4336,f1863]) ).
fof(f4339,plain,
( spl0_3
| spl0_4
| spl0_13
| spl0_42 ),
inference(avatar_contradiction_clause,[],[f4338]) ).
fof(f5696,plain,
( 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,v_x),v_ya),v_z) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))),v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))) ),
inference(resolution,[],[f1533,f1503]) ).
fof(f5711,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))),v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)))
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f5696,f1558]) ).
fof(f5713,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))),v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)))
| spl0_3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f5711,f1554]) ).
fof(f6806,definition,
( spl0_68
<=> c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f6807,plain,
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| spl0_68 ),
inference(avatar_component_clause,[],[f6806]) ).
fof(f6808,plain,
( c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f6806]) ).
fof(f6813,plain,
( c_in(c_Pair(v_ya,v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_68 ),
inference(resolution,[],[f6808,f26]) ).
fof(f6814,plain,
( c_in(c_Pair(v_x,v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_68 ),
inference(resolution,[],[f6808,f25]) ).
fof(f6851,plain,
( ~ c_in(c_Pair(v_x,v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),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(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| spl0_41 ),
inference(resolution,[],[f4317,f32]) ).
fof(f6852,plain,
( ~ c_in(c_Pair(v_z,v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| spl0_41
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f6851,f6814]) ).
fof(f6853,plain,
( $false
| spl0_41
| ~ spl0_42
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f6852,f4322]) ).
fof(f6854,plain,
( spl0_41
| ~ spl0_42
| ~ spl0_68 ),
inference(avatar_contradiction_clause,[],[f6853]) ).
fof(f8076,plain,
( ~ 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,v_x),v_ya),v_z),v_xb,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_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| spl0_68 ),
inference(resolution,[],[f6807,f6]) ).
fof(f8077,plain,
( ~ 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,v_x),v_ya),v_z),v_xb,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_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| spl0_68 ),
inference(resolution,[],[f6807,f12]) ).
fof(f8078,plain,
( 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,v_x),v_ya),v_z) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| spl0_68 ),
inference(forward_subsumption_resolution,[],[f8077,f1503]) ).
fof(f8079,plain,
( 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,v_x),v_ya),v_z) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| spl0_68 ),
inference(forward_subsumption_resolution,[],[f8076,f1503]) ).
fof(f8080,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| spl0_4
| spl0_68 ),
inference(forward_subsumption_resolution,[],[f8078,f1558]) ).
fof(f8081,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| spl0_4
| spl0_68 ),
inference(forward_subsumption_resolution,[],[f8079,f1558]) ).
fof(f8082,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| spl0_3
| spl0_4
| spl0_68 ),
inference(forward_subsumption_resolution,[],[f8080,f1554]) ).
fof(f8083,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| spl0_3
| spl0_4
| spl0_68 ),
inference(forward_subsumption_resolution,[],[f8081,f1554]) ).
fof(f8084,plain,
( $false
| spl0_2
| spl0_3
| spl0_4
| spl0_68 ),
inference(forward_subsumption_resolution,[],[f8082,f1550]) ).
fof(f8085,plain,
( spl0_2
| spl0_3
| spl0_4
| spl0_68 ),
inference(avatar_contradiction_clause,[],[f8084]) ).
fof(f8086,plain,
( $false
| spl0_3
| spl0_4
| spl0_13
| spl0_68 ),
inference(forward_subsumption_resolution,[],[f8083,f1863]) ).
fof(f8087,plain,
( spl0_3
| spl0_4
| spl0_13
| spl0_68 ),
inference(avatar_contradiction_clause,[],[f8086]) ).
fof(f8340,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z))
| v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))),v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)))
| spl0_3
| spl0_4
| ~ spl0_13 ),
inference(forward_demodulation,[],[f5713,f3936]) ).
fof(f8784,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))
| ~ spl0_13 ),
inference(equality_resolution,[],[f3922]) ).
fof(f8881,plain,
( ! [X0,X1] :
( c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x)
| v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb) = X1 )
| ~ spl0_13 ),
inference(superposition,[],[f65,f8784]) ).
fof(f8906,plain,
( v_x = v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)
| ~ spl0_13 ),
inference(equality_resolution,[],[f8881]) ).
fof(f9487,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z))
| v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))),v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)))
| spl0_3
| spl0_4
| ~ spl0_13 ),
inference(forward_demodulation,[],[f8340,f8906]) ).
fof(f10014,plain,
( v_xb != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z))
| spl0_2
| ~ spl0_13 ),
inference(forward_demodulation,[],[f1550,f3936]) ).
fof(f10024,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_ya),v_z,v_xb),v_z))
| ~ spl0_6
| ~ spl0_13 ),
inference(forward_demodulation,[],[f1581,f3936]) ).
fof(f10043,plain,
( v_xb != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z))
| spl0_2
| ~ spl0_13 ),
inference(forward_demodulation,[],[f10014,f8906]) ).
fof(f10051,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| ~ spl0_6
| ~ spl0_13 ),
inference(forward_demodulation,[],[f10024,f8906]) ).
fof(f10073,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z))
| ~ spl0_6
| ~ spl0_13 ),
inference(forward_demodulation,[],[f10051,f3936]) ).
fof(f10091,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z))
| ~ spl0_6
| ~ spl0_13 ),
inference(forward_demodulation,[],[f10073,f8906]) ).
fof(f10111,plain,
( v_xb != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)),v_ya),v_z,v_xb),v_z))
| spl0_6
| ~ spl0_13 ),
inference(forward_demodulation,[],[f1580,f3936]) ).
fof(f10122,plain,
( v_xb != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| spl0_6
| ~ spl0_13 ),
inference(forward_demodulation,[],[f10111,f8906]) ).
fof(f10127,plain,
( v_xb != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z))
| spl0_6
| ~ spl0_13 ),
inference(forward_demodulation,[],[f10122,f3936]) ).
fof(f10129,plain,
( v_xb != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z))
| spl0_6
| ~ spl0_13 ),
inference(forward_demodulation,[],[f10127,f8906]) ).
fof(f10196,plain,
( ~ 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,v_x),v_ya),v_z),v_xb,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_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| spl0_42 ),
inference(resolution,[],[f4323,f10]) ).
fof(f10197,plain,
( 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,v_x),v_ya),v_z) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| spl0_42 ),
inference(forward_subsumption_resolution,[],[f10196,f1503]) ).
fof(f10199,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| spl0_4
| spl0_42 ),
inference(forward_subsumption_resolution,[],[f10197,f1558]) ).
fof(f10201,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z))
| spl0_3
| spl0_4
| spl0_42 ),
inference(forward_subsumption_resolution,[],[f10199,f1554]) ).
fof(f10203,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z))
| spl0_3
| spl0_4
| ~ spl0_13
| spl0_42 ),
inference(forward_demodulation,[],[f10201,f3936]) ).
fof(f10205,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z))
| spl0_3
| spl0_4
| ~ spl0_13
| spl0_42 ),
inference(forward_demodulation,[],[f10203,f8906]) ).
fof(f10206,plain,
( $false
| spl0_2
| spl0_3
| spl0_4
| ~ spl0_13
| spl0_42 ),
inference(forward_subsumption_resolution,[],[f10205,f10043]) ).
fof(f10207,plain,
( spl0_2
| spl0_3
| spl0_4
| ~ spl0_13
| spl0_42 ),
inference(avatar_contradiction_clause,[],[f10206]) ).
fof(f10265,plain,
( v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTB(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb))),v_sko__uTC(v_x,v_ya,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb)))
| spl0_2
| spl0_3
| spl0_4
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f9487,f10043]) ).
fof(f10266,plain,
( $false
| spl0_43
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f6813,f4327]) ).
fof(f10267,plain,
( spl0_43
| ~ spl0_68 ),
inference(avatar_contradiction_clause,[],[f10266]) ).
fof(f10288,plain,
( spl0_12
| spl0_2
| spl0_3
| spl0_4
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f10265,f1862,f1557,f1553,f1549,f1858]) ).
fof(f10291,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_x),v_ya),v_z,v_xb),v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z))
| ~ spl0_2
| ~ spl0_13 ),
inference(forward_demodulation,[],[f1551,f3936]) ).
fof(f10311,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_x,v_z),c_Comb_Ocomb_Oop_A_D_D(v_ya,v_z))
| ~ spl0_2
| ~ spl0_13 ),
inference(forward_demodulation,[],[f10291,f8906]) ).
fof(f10318,plain,
( $false
| ~ spl0_2
| spl0_6
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f10311,f10129]) ).
fof(f10319,plain,
( ~ spl0_2
| spl0_6
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f10318]) ).
fof(f10336,plain,
( ~ c_in(c_Pair(v_xb,v_xb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_6
| ~ spl0_13 ),
inference(backward_demodulation,[],[f1506,f10091]) ).
fof(f10363,plain,
( $false
| ~ spl0_6
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f10336,f29]) ).
fof(f10364,plain,
( ~ spl0_6
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f10363]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f1560]) ).
cnf(s5,plain,
( spl0_3
| spl0_4
| spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f1865]) ).
cnf(s22,plain,
( spl0_1
| spl0_3
| spl0_4
| spl0_13 ),
inference(sat_conversion,[],[f2502]) ).
cnf(s23,plain,
~ spl0_4,
inference(sat_conversion,[],[f2713]) ).
cnf(s24,plain,
~ spl0_3,
inference(sat_conversion,[],[f3589]) ).
cnf(s32,plain,
( ~ spl0_1
| ~ spl0_12
| ~ spl0_40
| ~ spl0_41 ),
inference(sat_conversion,[],[f4318]) ).
cnf(s33,plain,
( spl0_40
| ~ spl0_42
| ~ spl0_43 ),
inference(sat_conversion,[],[f4328]) ).
cnf(s34,plain,
( spl0_3
| spl0_4
| spl0_13
| spl0_42 ),
inference(sat_conversion,[],[f4339]) ).
cnf(s55,plain,
( spl0_41
| ~ spl0_42
| ~ spl0_68 ),
inference(sat_conversion,[],[f6854]) ).
cnf(s63,plain,
( spl0_2
| spl0_3
| spl0_4
| spl0_68 ),
inference(sat_conversion,[],[f8085]) ).
cnf(s64,plain,
( spl0_3
| spl0_4
| spl0_13
| spl0_68 ),
inference(sat_conversion,[],[f8087]) ).
cnf(s96,plain,
( spl0_2
| spl0_3
| spl0_4
| ~ spl0_13
| spl0_42 ),
inference(sat_conversion,[],[f10207]) ).
cnf(s101,plain,
( spl0_43
| ~ spl0_68 ),
inference(sat_conversion,[],[f10267]) ).
cnf(s106,plain,
( spl0_2
| spl0_3
| spl0_4
| spl0_12
| ~ spl0_13 ),
inference(sat_conversion,[],[f10288]) ).
cnf(s108,plain,
( ~ spl0_2
| spl0_6
| ~ spl0_13 ),
inference(sat_conversion,[],[f10319]) ).
cnf(s112,plain,
( ~ spl0_6
| ~ spl0_13 ),
inference(sat_conversion,[],[f10364]) ).
cnf(s113,plain,
( spl0_1
| spl0_13 ),
inference(rat,[],[s22,s23,s24]) ).
cnf(s115,plain,
( spl0_12
| spl0_13 ),
inference(rat,[],[s5,s23,s24]) ).
cnf(s116,plain,
( spl0_1
| spl0_2 ),
inference(rat,[],[s1,s23,s24]) ).
cnf(s117,plain,
spl0_1,
inference(rat,[],[s108,s112,s116,s113]) ).
cnf(s119,plain,
( ~ spl0_42
| ~ spl0_12
| ~ spl0_68 ),
inference(rat,[],[s32,s33,s55,s101,s117]) ).
cnf(s120,plain,
( spl0_42
| spl0_2 ),
inference(rat,[],[s96,s34,s24,s23]) ).
cnf(s121,plain,
( spl0_12
| spl0_2 ),
inference(rat,[],[s115,s106,s23,s24]) ).
cnf(s122,plain,
spl0_2,
inference(rat,[],[s121,s119,s120,s63,s24,s23]) ).
cnf(s124,plain,
( spl0_13
| ~ spl0_12 ),
inference(rat,[],[s119,s34,s64,s24,s23]) ).
cnf(s125,plain,
~ spl0_13,
inference(rat,[],[s108,s112,s122]) ).
cnf(s128,plain,
spl0_12,
inference(rat,[],[s115,s125]) ).
cnf(s129,plain,
$false,
inference(rat,[],[s124,s128,s125]) ).
fof(f10381,plain,
$false,
inference(avatar_sat_refutation,[],[s129]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COL107-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.19 % Computer : n003.cluster.edu
% 0.12/0.19 % Model : x86_64 x86_64
% 0.12/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.19 % Memory : 8046.5625MB
% 0.12/0.19 % OS : Linux 6.8.0-71-generic
% 0.12/0.19 % CPULimit : 300
% 0.12/0.19 % WCLimit : 300
% 0.12/0.19 % DateTime : Mon Sep 28 21:41:28 UTC 2026
% 0.12/0.19 % CPUTime :
% 0.12/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.21 Running first-order theorem proving
% 0.12/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.88/1.97 % (2059547)Input is clausal, will run a generic CNF schedule.
% 7.88/1.97 % (2059555)lrs+10_1_sil=8000:sp=occurrence:random_seed=641472307:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.88/1.97 % (2059555)Refutation not found, incomplete strategy
% 7.88/1.97 % (2059555)------------------------------
% 7.88/1.97 % (2059555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.88/1.97 % (2059555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.88/1.97 % (2059555)CaDiCaL version: 2.1.3
% 7.88/1.97 % (2059555)Termination reason: Refutation not found, incomplete strategy
% 7.88/1.97 % (2059555)Time elapsed: 0.002 s
% 7.88/1.97 % (2059555)Peak memory usage: 88 MB
% 7.88/1.97 % (2059555)Instructions burned: 4 (million)
% 7.88/1.97 % (2059557)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3698687784:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.88/1.97 % (2059553)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2524373580:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.88/1.97 % (2059558)dis-21_1_sil=8000:lcm=predicate:random_seed=892864777: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)
% 7.88/1.97 % (2059552)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=2023751538:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.88/1.97 % (2059556)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1305669178:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.88/1.97 % (2059554)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=10285393:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.88/1.97 % (2059556)Refutation not found, incomplete strategy
% 7.88/1.97 % (2059556)------------------------------
% 7.88/1.97 % (2059556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.88/1.97 % (2059556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.88/1.97 % (2059556)CaDiCaL version: 2.1.3
% 7.88/1.97 % (2059556)Termination reason: Refutation not found, incomplete strategy
% 7.88/1.97 % (2059556)Time elapsed: 0.005 s
% 7.88/1.97 % (2059556)Peak memory usage: 88 MB
% 7.88/1.97 % (2059556)Instructions burned: 6 (million)
% 7.88/1.97 % (2059558)Instruction limit reached!
% 7.88/1.97 % (2059558)------------------------------
% 7.88/1.97 % (2059558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.88/1.97 % (2059558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.88/1.97 % (2059558)CaDiCaL version: 2.1.3
% 7.88/1.97 % (2059558)Termination reason: Instruction limit
% 7.88/1.97 % (2059558)Termination phase: Saturation
% 7.88/1.97 % (2059558)Time elapsed: 0.065 s
% 7.88/1.97 % (2059558)Peak memory usage: 89 MB
% 7.88/1.97 % (2059558)Instructions burned: 117 (million)
% 7.88/1.97 % (2059557)Instruction limit reached!
% 7.88/1.97 % (2059557)------------------------------
% 7.88/1.97 % (2059557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.88/1.97 % (2059557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.88/1.97 % (2059557)CaDiCaL version: 2.1.3
% 7.88/1.97 % (2059557)Termination reason: Instruction limit
% 7.88/1.97 % (2059557)Termination phase: Saturation
% 7.88/1.97 % (2059557)Time elapsed: 0.097 s
% 7.88/1.97 % (2059557)Peak memory usage: 90 MB
% 7.88/1.97 % (2059557)Instructions burned: 182 (million)
% 7.88/1.97 % (2059555)------------------------------
% 7.88/1.97 % (2059555)------------------------------
% 7.88/1.97 % (2059568)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=528227665:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 7.88/1.97 % (2059568)Refutation not found, incomplete strategy
% 7.88/1.97 % (2059568)------------------------------
% 7.88/1.97 % (2059568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.88/1.97 % (2059568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.88/1.97 % (2059568)CaDiCaL version: 2.1.3
% 7.88/1.97 % (2059568)Termination reason: Refutation not found, incomplete strategy
% 7.88/1.97 % (2059568)Time elapsed: 0.005 s
% 7.88/1.97 % (2059568)Peak memory usage: 89 MB
% 7.88/1.97 % (2059568)Instructions burned: 13 (million)
% 18.98/3.36 % (2059566)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=452840127:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 18.98/3.36 % (2059566)Refutation not found, incomplete strategy
% 18.98/3.36 % (2059566)------------------------------
% 18.98/3.36 % (2059566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/3.36 % (2059566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/3.36 % (2059566)CaDiCaL version: 2.1.3
% 18.98/3.36 % (2059566)Termination reason: Refutation not found, incomplete strategy
% 18.98/3.36 % (2059566)Time elapsed: 0.004 s
% 18.98/3.36 % (2059566)Peak memory usage: 88 MB
% 18.98/3.36 % (2059566)Instructions burned: 4 (million)
% 18.98/3.36 % (2059567)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3185964650: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)
% 18.98/3.36 % (2059556)------------------------------
% 18.98/3.36 % (2059556)------------------------------
% 18.98/3.36 % (2059567)Instruction limit reached!
% 18.98/3.36 % (2059567)------------------------------
% 18.98/3.36 % (2059567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/3.36 % (2059567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/3.36 % (2059567)CaDiCaL version: 2.1.3
% 18.98/3.36 % (2059567)Termination reason: Instruction limit
% 18.98/3.36 % (2059567)Termination phase: Saturation
% 18.98/3.36 % (2059567)Time elapsed: 0.103 s
% 18.98/3.36 % (2059567)Peak memory usage: 90 MB
% 18.98/3.36 % (2059567)Instructions burned: 190 (million)
% 18.98/3.36 % (2059568)------------------------------
% 18.98/3.36 % (2059568)------------------------------
% 18.98/3.36 % (2059572)lrs+10_64_to=lpo:sil=8000:random_seed=3171754837:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 18.98/3.36 % (2059574)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2923787113:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 18.98/3.36 % (2059566)------------------------------
% 18.98/3.36 % (2059566)------------------------------
% 18.98/3.36 % (2059572)Instruction limit reached!
% 18.98/3.36 % (2059572)------------------------------
% 18.98/3.36 % (2059572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/3.36 % (2059572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/3.36 % (2059572)CaDiCaL version: 2.1.3
% 18.98/3.36 % (2059572)Termination reason: Instruction limit
% 18.98/3.36 % (2059572)Termination phase: Saturation
% 18.98/3.36 % (2059572)Time elapsed: 0.080 s
% 18.98/3.36 % (2059572)Peak memory usage: 89 MB
% 18.98/3.36 % (2059572)Instructions burned: 127 (million)
% 18.98/3.36 % (2059573)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1069158106:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 18.98/3.36 % (2059574)Instruction limit reached!
% 18.98/3.36 % (2059574)------------------------------
% 18.98/3.36 % (2059574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/3.36 % (2059574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/3.36 % (2059574)CaDiCaL version: 2.1.3
% 18.98/3.36 % (2059574)Termination reason: Instruction limit
% 18.98/3.36 % (2059574)Termination phase: Saturation
% 18.98/3.36 % (2059574)Time elapsed: 0.049 s
% 18.98/3.36 % (2059574)Peak memory usage: 91 MB
% 18.98/3.36 % (2059574)Instructions burned: 158 (million)
% 18.98/3.36 % (2059580)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3557653865:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 18.98/3.36 % (2059577)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2082236007:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 18.98/3.36 % (2059580)Instruction limit reached!
% 18.98/3.36 % (2059580)------------------------------
% 18.98/3.36 % (2059580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/3.36 % (2059580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/3.36 % (2059580)CaDiCaL version: 2.1.3
% 18.98/3.36 % (2059580)Termination reason: Instruction limit
% 18.98/3.36 % (2059580)Termination phase: Saturation
% 18.98/3.36 % (2059580)Time elapsed: 0.036 s
% 18.98/3.36 % (2059580)Peak memory usage: 90 MB
% 18.98/3.36 % (2059580)Instructions burned: 108 (million)
% 18.98/3.36 % (2059573)Instruction limit reached!
% 18.98/3.36 % (2059573)------------------------------
% 27.22/4.59 % (2059573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.22/4.59 % (2059573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.22/4.59 % (2059573)CaDiCaL version: 2.1.3
% 27.22/4.59 % (2059573)Termination reason: Instruction limit
% 27.22/4.59 % (2059573)Termination phase: Saturation
% 27.22/4.59 % (2059573)Time elapsed: 0.129 s
% 27.22/4.59 % (2059573)Peak memory usage: 90 MB
% 27.22/4.59 % (2059573)Instructions burned: 195 (million)
% 27.22/4.59 % (2059578)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=2574236729:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 27.22/4.59 % (2059578)Instruction limit reached!
% 27.22/4.59 % (2059578)------------------------------
% 27.22/4.59 % (2059578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.22/4.59 % (2059578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.22/4.59 % (2059578)CaDiCaL version: 2.1.3
% 27.22/4.59 % (2059578)Termination reason: Instruction limit
% 27.22/4.59 % (2059578)Termination phase: Saturation
% 27.22/4.59 % (2059578)Time elapsed: 0.060 s
% 27.22/4.59 % (2059578)Peak memory usage: 90 MB
% 27.22/4.59 % (2059578)Instructions burned: 107 (million)
% 27.22/4.59 % (2059583)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3480261170:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 27.22/4.59 % (2059585)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1438760525:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 27.22/4.59 % (2059583)Instruction limit reached!
% 27.22/4.59 % (2059583)------------------------------
% 27.22/4.59 % (2059583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.22/4.59 % (2059583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.22/4.59 % (2059583)CaDiCaL version: 2.1.3
% 27.22/4.59 % (2059583)Termination reason: Instruction limit
% 27.22/4.59 % (2059583)Termination phase: Saturation
% 27.22/4.59 % (2059583)Time elapsed: 0.068 s
% 27.22/4.59 % (2059583)Peak memory usage: 89 MB
% 27.22/4.59 % (2059583)Instructions burned: 242 (million)
% 27.22/4.59 % (2059586)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1885068457:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 27.22/4.59 % (2059586)Refutation not found, incomplete strategy
% 27.22/4.59 % (2059586)------------------------------
% 27.22/4.59 % (2059586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.22/4.59 % (2059586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.22/4.59 % (2059586)CaDiCaL version: 2.1.3
% 27.22/4.59 % (2059586)Termination reason: Refutation not found, incomplete strategy
% 27.22/4.59 % (2059586)Time elapsed: 0.004 s
% 27.22/4.59 % (2059586)Peak memory usage: 89 MB
% 27.22/4.59 % (2059586)Instructions burned: 4 (million)
% 27.22/4.59 % (2059589)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1484154275:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 27.22/4.59 % (2059589)Instruction limit reached!
% 27.22/4.59 % (2059589)------------------------------
% 27.22/4.59 % (2059589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.22/4.59 % (2059589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.22/4.59 % (2059589)CaDiCaL version: 2.1.3
% 27.22/4.59 % (2059589)Termination reason: Instruction limit
% 27.22/4.59 % (2059589)Termination phase: Saturation
% 27.22/4.59 % (2059589)Time elapsed: 0.138 s
% 27.22/4.59 % (2059589)Peak memory usage: 98 MB
% 27.22/4.59 % (2059589)Instructions burned: 500 (million)
% 27.22/4.59 % (2059586)------------------------------
% 27.22/4.59 % (2059586)------------------------------
% 27.22/4.59 % (2059592)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=449402310:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 27.22/4.59 % (2059592)Instruction limit reached!
% 27.22/4.59 % (2059592)------------------------------
% 27.22/4.59 % (2059592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.22/4.59 % (2059592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.22/4.59 % (2059592)CaDiCaL version: 2.1.3
% 27.22/4.59 % (2059592)Termination reason: Instruction limit
% 47.32/7.35 % (2059592)Termination phase: Saturation
% 47.32/7.35 % (2059592)Time elapsed: 0.072 s
% 47.32/7.35 % (2059592)Peak memory usage: 92 MB
% 47.32/7.35 % (2059592)Instructions burned: 191 (million)
% 47.32/7.35 % (2059593)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=492594748:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 47.32/7.35 % (2059595)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=452113593:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 47.32/7.35 % (2059595)Instruction limit reached!
% 47.32/7.35 % (2059595)------------------------------
% 47.32/7.35 % (2059595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.32/7.35 % (2059595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.32/7.35 % (2059595)CaDiCaL version: 2.1.3
% 47.32/7.35 % (2059595)Termination reason: Instruction limit
% 47.32/7.35 % (2059595)Termination phase: Saturation
% 47.32/7.35 % (2059595)Time elapsed: 0.051 s
% 47.32/7.35 % (2059595)Peak memory usage: 90 MB
% 47.32/7.35 % (2059595)Instructions burned: 159 (million)
% 47.32/7.36 % (2059593)Instruction limit reached!
% 47.32/7.36 % (2059593)------------------------------
% 47.32/7.36 % (2059593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.32/7.36 % (2059593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.32/7.36 % (2059593)CaDiCaL version: 2.1.3
% 47.32/7.36 % (2059593)Termination reason: Instruction limit
% 47.32/7.36 % (2059593)Termination phase: Saturation
% 47.32/7.36 % (2059593)Time elapsed: 0.147 s
% 47.32/7.36 % (2059593)Peak memory usage: 92 MB
% 47.32/7.36 % (2059593)Instructions burned: 265 (million)
% 47.32/7.36 % (2059598)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=1032482989:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi)
% 47.32/7.36 % (2059599)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2211314190:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi)
% 47.32/7.36 % (2059599)Instruction limit reached!
% 47.32/7.36 % (2059599)------------------------------
% 47.32/7.36 % (2059599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.32/7.36 % (2059599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.32/7.36 % (2059599)CaDiCaL version: 2.1.3
% 47.32/7.36 % (2059599)Termination reason: Instruction limit
% 47.32/7.36 % (2059599)Termination phase: Saturation
% 47.32/7.36 % (2059599)Time elapsed: 0.282 s
% 47.32/7.36 % (2059599)Peak memory usage: 95 MB
% 47.32/7.36 % (2059599)Instructions burned: 538 (million)
% 47.32/7.36 % (2059602)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1687991930:i=180:bd=preordered:av=off_2980 on theBenchmark for (2980ds/180Mi)
% 47.32/7.36 % (2059602)Instruction limit reached!
% 47.32/7.36 % (2059602)------------------------------
% 47.32/7.36 % (2059602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.32/7.36 % (2059602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.32/7.36 % (2059602)CaDiCaL version: 2.1.3
% 47.32/7.36 % (2059602)Termination reason: Instruction limit
% 47.32/7.36 % (2059602)Termination phase: Saturation
% 47.32/7.36 % (2059602)Time elapsed: 0.100 s
% 47.32/7.36 % (2059602)Peak memory usage: 95 MB
% 47.32/7.36 % (2059602)Instructions burned: 181 (million)
% 47.32/7.36 % (2059604)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=470708235:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2978 on theBenchmark for (2978ds/10307Mi)
% 47.32/7.36 % (2059598)Instruction limit reached!
% 47.32/7.36 % (2059598)------------------------------
% 47.32/7.36 % (2059598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.32/7.36 % (2059598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.32/7.36 % (2059598)CaDiCaL version: 2.1.3
% 47.32/7.36 % (2059598)Termination reason: Instruction limit
% 47.32/7.36 % (2059598)Termination phase: Saturation
% 47.32/7.36 % (2059598)Time elapsed: 1.077 s
% 47.32/7.36 % (2059598)Peak memory usage: 151 MB
% 47.32/7.36 % (2059598)Instructions burned: 3258 (million)
% 47.32/7.36 % (2059606)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=747773040:i=412:gtgl=4:gtg=exists_all_2973 on theBenchmark for (2973ds/412Mi)
% 65.75/10.02 % (2059606)Instruction limit reached!
% 65.75/10.02 % (2059606)------------------------------
% 65.75/10.02 % (2059606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.75/10.02 % (2059606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.75/10.02 % (2059606)CaDiCaL version: 2.1.3
% 65.75/10.02 % (2059606)Termination reason: Instruction limit
% 65.75/10.02 % (2059606)Termination phase: Saturation
% 65.75/10.02 % (2059606)Time elapsed: 0.115 s
% 65.75/10.02 % (2059606)Peak memory usage: 96 MB
% 65.75/10.02 % (2059606)Instructions burned: 412 (million)
% 65.75/10.02 % (2059577)Instruction limit reached!
% 65.75/10.02 % (2059577)------------------------------
% 65.75/10.02 % (2059577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.75/10.02 % (2059577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.75/10.02 % (2059577)CaDiCaL version: 2.1.3
% 65.75/10.02 % (2059577)Termination reason: Instruction limit
% 65.75/10.02 % (2059577)Termination phase: Saturation
% 65.75/10.02 % (2059577)Time elapsed: 2.100 s
% 65.75/10.02 % (2059577)Peak memory usage: 151 MB
% 65.75/10.02 % (2059577)Instructions burned: 3395 (million)
% 65.75/10.02 % (2059608)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=2569339239:s2pl=no:i=8478:s2at=4:nm=6_2971 on theBenchmark for (2971ds/8478Mi)
% 65.75/10.02 % (2059609)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=2900629722:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2971 on theBenchmark for (2971ds/303Mi)
% 65.75/10.02 % (2059609)Instruction limit reached!
% 65.75/10.02 % (2059609)------------------------------
% 65.75/10.02 % (2059609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.75/10.02 % (2059609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.75/10.02 % (2059609)CaDiCaL version: 2.1.3
% 65.75/10.02 % (2059609)Termination reason: Instruction limit
% 65.75/10.02 % (2059609)Termination phase: Saturation
% 65.75/10.02 % (2059609)Time elapsed: 0.083 s
% 65.75/10.02 % (2059609)Peak memory usage: 94 MB
% 65.75/10.02 % (2059609)Instructions burned: 306 (million)
% 65.75/10.02 % (2059612)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3694176701:st=4:i=720:sd=3:fsr=off:ss=axioms_2969 on theBenchmark for (2969ds/720Mi)
% 65.75/10.02 % (2059612)Instruction limit reached!
% 65.75/10.02 % (2059612)------------------------------
% 65.75/10.02 % (2059612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.75/10.02 % (2059612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.75/10.02 % (2059612)CaDiCaL version: 2.1.3
% 65.75/10.02 % (2059612)Termination reason: Instruction limit
% 65.75/10.02 % (2059612)Termination phase: Saturation
% 65.75/10.02 % (2059612)Time elapsed: 0.202 s
% 65.75/10.02 % (2059612)Peak memory usage: 98 MB
% 65.75/10.02 % (2059612)Instructions burned: 720 (million)
% 65.75/10.02 % (2059614)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=769724311:i=598:bs=on:bd=preordered:av=off:ss=axioms_2966 on theBenchmark for (2966ds/598Mi)
% 65.75/10.02 % (2059614)Instruction limit reached!
% 65.75/10.02 % (2059614)------------------------------
% 65.75/10.02 % (2059614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.75/10.02 % (2059614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.75/10.02 % (2059614)CaDiCaL version: 2.1.3
% 65.75/10.02 % (2059614)Termination reason: Instruction limit
% 65.75/10.02 % (2059614)Termination phase: Saturation
% 65.75/10.02 % (2059614)Time elapsed: 0.182 s
% 65.75/10.02 % (2059614)Peak memory usage: 96 MB
% 65.75/10.02 % (2059614)Instructions burned: 600 (million)
% 65.75/10.02 % (2059616)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3768018433:i=2989:sd=3:ss=axioms:sgt=60_2963 on theBenchmark for (2963ds/2989Mi)
% 65.75/10.02 % (2059585)Instruction limit reached!
% 65.75/10.02 % (2059585)------------------------------
% 65.75/10.02 % (2059585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.75/10.02 % (2059585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.75/10.02 % (2059585)CaDiCaL version: 2.1.3
% 65.75/10.02 % (2059585)Termination reason: Instruction limit
% 65.75/10.02 % (2059585)Termination phase: Saturation
% 65.75/10.02 % (2059585)Time elapsed: 3.031 s
% 65.75/10.02 % (2059585)Peak memory usage: 160 MB
% 66.67/10.12 % (2059585)Instructions burned: 5208 (million)
% 66.67/10.12 % (2059618)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=680157958:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2960 on theBenchmark for (2960ds/1997Mi)
% 66.67/10.12 % (2059616)Instruction limit reached!
% 66.67/10.12 % (2059616)------------------------------
% 66.67/10.12 % (2059616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.67/10.12 % (2059616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.67/10.12 % (2059616)CaDiCaL version: 2.1.3
% 66.67/10.12 % (2059616)Termination reason: Instruction limit
% 66.67/10.12 % (2059616)Termination phase: Saturation
% 66.67/10.12 % (2059616)Time elapsed: 0.917 s
% 66.67/10.12 % (2059616)Peak memory usage: 146 MB
% 66.67/10.12 % (2059616)Instructions burned: 2990 (million)
% 66.67/10.12 % (2059620)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=3447516267:i=2088:bd=preordered:av=off_2953 on theBenchmark for (2953ds/2088Mi)
% 66.67/10.12 % (2059618)Instruction limit reached!
% 66.67/10.12 % (2059618)------------------------------
% 66.67/10.12 % (2059618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.67/10.12 % (2059618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.67/10.12 % (2059618)CaDiCaL version: 2.1.3
% 66.67/10.12 % (2059618)Termination reason: Instruction limit
% 66.67/10.12 % (2059618)Termination phase: Saturation
% 66.67/10.12 % (2059618)Time elapsed: 1.282 s
% 66.67/10.12 % (2059618)Peak memory usage: 138 MB
% 66.67/10.12 % (2059618)Instructions burned: 1998 (million)
% 66.67/10.12 % (2059620)Instruction limit reached!
% 66.67/10.12 % (2059620)------------------------------
% 66.67/10.12 % (2059620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.67/10.12 % (2059620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.67/10.12 % (2059620)CaDiCaL version: 2.1.3
% 66.67/10.12 % (2059620)Termination reason: Instruction limit
% 66.67/10.12 % (2059620)Termination phase: Saturation
% 66.67/10.12 % (2059620)Time elapsed: 0.703 s
% 66.67/10.12 % (2059620)Peak memory usage: 140 MB
% 66.67/10.12 % (2059620)Instructions burned: 2090 (million)
% 66.67/10.12 % (2059623)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2191601444:i=433:bd=preordered_2945 on theBenchmark for (2945ds/433Mi)
% 66.67/10.12 % (2059622)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3323699451:i=1098:nicw=on_2946 on theBenchmark for (2946ds/1098Mi)
% 66.67/10.12 % (2059623)Instruction limit reached!
% 66.67/10.12 % (2059623)------------------------------
% 66.67/10.12 % (2059623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.67/10.12 % (2059623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.67/10.12 % (2059623)CaDiCaL version: 2.1.3
% 66.67/10.12 % (2059623)Termination reason: Instruction limit
% 66.67/10.12 % (2059623)Termination phase: Saturation
% 66.67/10.12 % (2059623)Time elapsed: 0.138 s
% 66.67/10.12 % (2059623)Peak memory usage: 94 MB
% 66.67/10.12 % (2059623)Instructions burned: 435 (million)
% 66.67/10.12 % (2059626)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2817592159:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2943 on theBenchmark for (2943ds/2942Mi)
% 66.67/10.12 % (2059622)Instruction limit reached!
% 66.67/10.12 % (2059622)------------------------------
% 66.67/10.12 % (2059622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.67/10.12 % (2059622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.67/10.12 % (2059622)CaDiCaL version: 2.1.3
% 66.67/10.12 % (2059622)Termination reason: Instruction limit
% 66.67/10.12 % (2059622)Termination phase: Saturation
% 66.67/10.12 % (2059622)Time elapsed: 0.597 s
% 66.67/10.12 % (2059622)Peak memory usage: 105 MB
% 66.67/10.12 % (2059622)Instructions burned: 1098 (million)
% 66.67/10.12 % (2059628)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3151474234:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2939 on theBenchmark for (2939ds/6922Mi)
% 66.67/10.12 % (2059626)Instruction limit reached!
% 66.67/10.12 % (2059626)------------------------------
% 66.67/10.12 % (2059626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.67/10.12 % (2059626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.67/10.12 % (2059626)CaDiCaL version: 2.1.3
% 66.67/10.12 % (2059626)Termination reason: Instruction limit
% 66.67/10.12 % (2059626)Termination phase: Saturation
% 66.67/10.12 % (2059626)Time elapsed: 0.979 s
% 66.67/10.12 % (2059626)Peak memory usage: 143 MB
% 66.67/10.12 % (2059626)Instructions burned: 2944 (million)
% 66.67/10.12 % (2059630)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=2498599141:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2932 on theBenchmark for (2932ds/596Mi)
% 66.67/10.12 % (2059630)Instruction limit reached!
% 66.67/10.12 % (2059630)------------------------------
% 66.67/10.12 % (2059630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.67/10.12 % (2059630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.67/10.12 % (2059630)CaDiCaL version: 2.1.3
% 66.67/10.12 % (2059630)Termination reason: Instruction limit
% 66.67/10.12 % (2059630)Termination phase: Saturation
% 66.67/10.12 % (2059630)Time elapsed: 0.174 s
% 66.67/10.12 % (2059630)Peak memory usage: 97 MB
% 66.67/10.12 % (2059630)Instructions burned: 596 (million)
% 66.67/10.12 % (2059632)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2738608417:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2930 on theBenchmark for (2930ds/4123Mi)
% 66.67/10.12 % (2059608)Instruction limit reached!
% 66.67/10.12 % (2059608)------------------------------
% 66.67/10.12 % (2059608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.67/10.12 % (2059608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.67/10.12 % (2059608)CaDiCaL version: 2.1.3
% 66.67/10.12 % (2059608)Termination reason: Instruction limit
% 66.67/10.12 % (2059608)Termination phase: Saturation
% 66.67/10.12 % (2059608)Time elapsed: 4.541 s
% 66.67/10.12 % (2059608)Peak memory usage: 201 MB
% 66.67/10.12 % (2059608)Instructions burned: 8478 (million)
% 66.67/10.12 % (2059634)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1345859272:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2924 on theBenchmark for (2924ds/16411Mi)
% 66.67/10.12 % (2059604)Instruction limit reached!
% 66.67/10.12 % (2059604)------------------------------
% 66.67/10.12 % (2059604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.67/10.12 % (2059604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.67/10.12 % (2059604)CaDiCaL version: 2.1.3
% 66.67/10.12 % (2059604)Termination reason: Instruction limit
% 66.67/10.12 % (2059604)Termination phase: Saturation
% 66.67/10.12 % (2059604)Time elapsed: 5.866 s
% 66.67/10.12 % (2059604)Peak memory usage: 164 MB
% 66.67/10.12 % (2059604)Instructions burned: 10309 (million)
% 66.67/10.12 % (2059636)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1178886795:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2918 on theBenchmark for (2918ds/1670Mi)
% 66.67/10.12 % (2059632)Instruction limit reached!
% 66.67/10.12 % (2059632)------------------------------
% 66.67/10.12 % (2059632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.67/10.12 % (2059632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.67/10.12 % (2059632)CaDiCaL version: 2.1.3
% 66.67/10.12 % (2059632)Termination reason: Instruction limit
% 66.67/10.12 % (2059632)Termination phase: Saturation
% 66.67/10.12 % (2059632)Time elapsed: 2.178 s
% 66.67/10.12 % (2059632)Peak memory usage: 161 MB
% 66.67/10.12 % (2059632)Instructions burned: 4124 (million)
% 66.67/10.12 % (2059634)First to succeed.
% 66.67/10.12 % (2059634)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2059547"
% 66.67/10.12 % (2059636)Instruction limit reached!
% 66.67/10.12 % (2059636)------------------------------
% 66.67/10.12 % (2059636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.67/10.12 % (2059636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.67/10.12 % (2059636)CaDiCaL version: 2.1.3
% 66.67/10.12 % (2059636)Termination reason: Instruction limit
% 66.67/10.12 % (2059636)Termination phase: Saturation
% 66.67/10.12 % (2059636)Time elapsed: 1.022 s
% 66.67/10.12 % (2059636)Peak memory usage: 138 MB
% 66.67/10.12 % (2059636)Instructions burned: 1670 (million)
% 66.67/10.12 % (2059638)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=2218532861:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2907 on theBenchmark for (2907ds/1722Mi)
% 66.67/10.12 % (2059634)Refutation found. Thanks to Tanya!
% 66.67/10.12 % SZS status Unsatisfiable for theBenchmark
% 66.67/10.12 % SZS output start Proof for theBenchmark
% See solution above
% 67.44/10.33 % (2059634)------------------------------
% 67.44/10.33 % (2059634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.44/10.33 % (2059634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.44/10.33 % (2059634)CaDiCaL version: 2.1.3
% 67.44/10.33 % (2059634)Termination reason: Refutation
% 67.44/10.33 % (2059634)Time elapsed: 1.645 s
% 67.44/10.33 % (2059634)Peak memory usage: 151 MB
% 67.44/10.33 % (2059634)Instructions burned: 4665 (million)
% 67.44/10.33 % (2059634)------------------------------
% 67.44/10.33 % (2059634)------------------------------
% 67.44/10.33 % (2059547)Success in time 9.467 s
% 67.44/10.33 % Vampire exiting
%------------------------------------------------------------------------------