%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN076-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 01:49:25 PM UTC 2026
% Result : Unsatisfiable 41.72s 6.54s
% Output : Refutation 42.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
c2 != c1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1) ).
fof(f2,axiom,
! [X0] :
( X0 = c2
| X0 = c1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2) ).
fof(f3,plain,
! [X0] :
( c1 = X0
| c2 = X0 ),
inference(reorient_equations,[],[f2]) ).
fof(f4,negated_conjecture,
! [X2,X3,X0,X1] :
( big_f(X0,f1(X0,X1))
| f1(X0,X1) = X1
| X0 = c3
| big_f(f3(X2,X3),X2)
| f3(X2,X3) = X3
| X2 = c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3) ).
fof(f5,plain,
! [X2,X3,X0,X1] :
( big_f(X0,f1(X0,X1))
| f1(X0,X1) = X1
| c3 = X0
| big_f(f3(X2,X3),X2)
| f3(X2,X3) = X3
| c4 = X2 ),
inference(reorient_equations,[],[f4]) ).
fof(f6,negated_conjecture,
! [X2,X3,X0,X1] :
( big_f(X0,f1(X0,X1))
| f1(X0,X1) = X1
| X0 = c3
| ~ big_f(f3(X2,X3),X2)
| f3(X2,X3) != X3
| X2 = c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4) ).
fof(f7,plain,
! [X2,X3,X0,X1] :
( big_f(X0,f1(X0,X1))
| f1(X0,X1) = X1
| c3 = X0
| ~ big_f(f3(X2,X3),X2)
| f3(X2,X3) != X3
| c4 = X2 ),
inference(reorient_equations,[],[f6]) ).
fof(f8,negated_conjecture,
! [X2,X3,X0,X1] :
( big_f(X0,f1(X0,X1))
| f1(X0,X1) = X1
| X0 = c3
| ~ big_f(X2,X3)
| X2 = f4(X3)
| X3 != c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_5) ).
fof(f9,plain,
! [X2,X3,X0,X1] :
( big_f(X0,f1(X0,X1))
| f1(X0,X1) = X1
| c3 = X0
| ~ big_f(X2,X3)
| f4(X3) = X2
| c4 != X3 ),
inference(reorient_equations,[],[f8]) ).
fof(f10,negated_conjecture,
! [X2,X3,X0,X1] :
( big_f(X0,f1(X0,X1))
| f1(X0,X1) = X1
| X0 = c3
| big_f(X2,X3)
| X2 != f4(X3)
| X3 != c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6) ).
fof(f11,plain,
! [X2,X3,X0,X1] :
( big_f(X0,f1(X0,X1))
| f1(X0,X1) = X1
| c3 = X0
| big_f(X2,X3)
| f4(X3) != X2
| c4 != X3 ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(X0,f1(X0,X1))
| f1(X0,X1) != X1
| X0 = c3
| big_f(f3(X2,X3),X2)
| f3(X2,X3) = X3
| X2 = c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_7) ).
fof(f13,plain,
! [X2,X3,X0,X1] :
( ~ big_f(X0,f1(X0,X1))
| f1(X0,X1) != X1
| c3 = X0
| big_f(f3(X2,X3),X2)
| f3(X2,X3) = X3
| c4 = X2 ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(X0,f1(X0,X1))
| f1(X0,X1) != X1
| X0 = c3
| ~ big_f(f3(X2,X3),X2)
| f3(X2,X3) != X3
| X2 = c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_8) ).
fof(f15,plain,
! [X2,X3,X0,X1] :
( ~ big_f(X0,f1(X0,X1))
| f1(X0,X1) != X1
| c3 = X0
| ~ big_f(f3(X2,X3),X2)
| f3(X2,X3) != X3
| c4 = X2 ),
inference(reorient_equations,[],[f14]) ).
fof(f16,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(X0,f1(X0,X1))
| f1(X0,X1) != X1
| X0 = c3
| ~ big_f(X2,X3)
| X2 = f4(X3)
| X3 != c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_9) ).
fof(f17,plain,
! [X2,X3,X0,X1] :
( ~ big_f(X0,f1(X0,X1))
| f1(X0,X1) != X1
| c3 = X0
| ~ big_f(X2,X3)
| f4(X3) = X2
| c4 != X3 ),
inference(reorient_equations,[],[f16]) ).
fof(f18,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(X0,f1(X0,X1))
| f1(X0,X1) != X1
| X0 = c3
| big_f(X2,X3)
| X2 != f4(X3)
| X3 != c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_10) ).
fof(f19,plain,
! [X2,X3,X0,X1] :
( ~ big_f(X0,f1(X0,X1))
| f1(X0,X1) != X1
| c3 = X0
| big_f(X2,X3)
| f4(X3) != X2
| c4 != X3 ),
inference(reorient_equations,[],[f18]) ).
fof(f20,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(X0,X1)
| X1 = f2(X0)
| X0 != c3
| big_f(f3(X2,X3),X2)
| f3(X2,X3) = X3
| X2 = c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_11) ).
fof(f21,plain,
! [X2,X3,X0,X1] :
( ~ big_f(X0,X1)
| f2(X0) = X1
| c3 != X0
| big_f(f3(X2,X3),X2)
| f3(X2,X3) = X3
| c4 = X2 ),
inference(reorient_equations,[],[f20]) ).
fof(f22,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(X0,X1)
| X1 = f2(X0)
| X0 != c3
| ~ big_f(f3(X2,X3),X2)
| f3(X2,X3) != X3
| X2 = c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_12) ).
fof(f23,plain,
! [X2,X3,X0,X1] :
( ~ big_f(X0,X1)
| f2(X0) = X1
| c3 != X0
| ~ big_f(f3(X2,X3),X2)
| f3(X2,X3) != X3
| c4 = X2 ),
inference(reorient_equations,[],[f22]) ).
fof(f24,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(X0,X1)
| X1 = f2(X0)
| X0 != c3
| ~ big_f(X2,X3)
| X2 = f4(X3)
| X3 != c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_13) ).
fof(f25,plain,
! [X2,X3,X0,X1] :
( ~ big_f(X0,X1)
| f2(X0) = X1
| c3 != X0
| ~ big_f(X2,X3)
| f4(X3) = X2
| c4 != X3 ),
inference(reorient_equations,[],[f24]) ).
fof(f26,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(X0,X1)
| X1 = f2(X0)
| X0 != c3
| big_f(X2,X3)
| X2 != f4(X3)
| X3 != c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_14) ).
fof(f27,plain,
! [X2,X3,X0,X1] :
( ~ big_f(X0,X1)
| f2(X0) = X1
| c3 != X0
| big_f(X2,X3)
| f4(X3) != X2
| c4 != X3 ),
inference(reorient_equations,[],[f26]) ).
fof(f28,negated_conjecture,
! [X2,X3,X0,X1] :
( big_f(X0,X1)
| X1 != f2(X0)
| X0 != c3
| big_f(f3(X2,X3),X2)
| f3(X2,X3) = X3
| X2 = c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_15) ).
fof(f29,plain,
! [X2,X3,X0,X1] :
( big_f(X0,X1)
| f2(X0) != X1
| c3 != X0
| big_f(f3(X2,X3),X2)
| f3(X2,X3) = X3
| c4 = X2 ),
inference(reorient_equations,[],[f28]) ).
fof(f30,negated_conjecture,
! [X2,X3,X0,X1] :
( big_f(X0,X1)
| X1 != f2(X0)
| X0 != c3
| ~ big_f(f3(X2,X3),X2)
| f3(X2,X3) != X3
| X2 = c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16) ).
fof(f31,plain,
! [X2,X3,X0,X1] :
( big_f(X0,X1)
| f2(X0) != X1
| c3 != X0
| ~ big_f(f3(X2,X3),X2)
| f3(X2,X3) != X3
| c4 = X2 ),
inference(reorient_equations,[],[f30]) ).
fof(f34,negated_conjecture,
! [X2,X3,X0,X1] :
( big_f(X0,X1)
| X1 != f2(X0)
| X0 != c3
| big_f(X2,X3)
| X2 != f4(X3)
| X3 != c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_18) ).
fof(f35,plain,
! [X2,X3,X0,X1] :
( big_f(X0,X1)
| f2(X0) != X1
| c3 != X0
| big_f(X2,X3)
| f4(X3) != X2
| c4 != X3 ),
inference(reorient_equations,[],[f34]) ).
fof(f36,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(f7(X0),X1)
| X1 = f5(X0)
| f7(X0) = X0
| ~ big_f(X2,f10(X3))
| X2 = f8(X3)
| f10(X3) = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_19) ).
fof(f37,plain,
! [X2,X3,X0,X1] :
( ~ big_f(f7(X0),X1)
| f5(X0) = X1
| f7(X0) = X0
| ~ big_f(X2,f10(X3))
| f8(X3) = X2
| f10(X3) = X3 ),
inference(reorient_equations,[],[f36]) ).
fof(f40,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(f7(X0),X1)
| X1 = f5(X0)
| f7(X0) = X0
| big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) = X3
| f10(X2) != X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_21) ).
fof(f41,plain,
! [X2,X3,X0,X1] :
( ~ big_f(f7(X0),X1)
| f5(X0) = X1
| f7(X0) = X0
| big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) = X3
| f10(X2) != X2 ),
inference(reorient_equations,[],[f40]) ).
fof(f42,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(f7(X0),X1)
| X1 = f5(X0)
| f7(X0) = X0
| ~ big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) != X3
| f10(X2) != X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_22) ).
fof(f43,plain,
! [X2,X3,X0,X1] :
( ~ big_f(f7(X0),X1)
| f5(X0) = X1
| f7(X0) = X0
| ~ big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) != X3
| f10(X2) != X2 ),
inference(reorient_equations,[],[f42]) ).
fof(f46,negated_conjecture,
! [X2,X3,X0,X1] :
( big_f(f7(X0),X1)
| X1 != f5(X0)
| f7(X0) = X0
| big_f(X2,f10(X3))
| X2 != f8(X3)
| f10(X3) = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_24) ).
fof(f47,plain,
! [X2,X3,X0,X1] :
( big_f(f7(X0),X1)
| f5(X0) != X1
| f7(X0) = X0
| big_f(X2,f10(X3))
| f8(X3) != X2
| f10(X3) = X3 ),
inference(reorient_equations,[],[f46]) ).
fof(f48,negated_conjecture,
! [X2,X3,X0,X1] :
( big_f(f7(X0),X1)
| X1 != f5(X0)
| f7(X0) = X0
| big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) = X3
| f10(X2) != X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_25) ).
fof(f49,plain,
! [X2,X3,X0,X1] :
( big_f(f7(X0),X1)
| f5(X0) != X1
| f7(X0) = X0
| big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) = X3
| f10(X2) != X2 ),
inference(reorient_equations,[],[f48]) ).
fof(f50,negated_conjecture,
! [X2,X3,X0,X1] :
( big_f(f7(X0),X1)
| X1 != f5(X0)
| f7(X0) = X0
| ~ big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) != X3
| f10(X2) != X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_26) ).
fof(f51,plain,
! [X2,X3,X0,X1] :
( big_f(f7(X0),X1)
| f5(X0) != X1
| f7(X0) = X0
| ~ big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) != X3
| f10(X2) != X2 ),
inference(reorient_equations,[],[f50]) ).
fof(f52,negated_conjecture,
! [X2,X3,X0,X1] :
( big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) = X1
| f7(X0) != X0
| ~ big_f(X2,f10(X3))
| X2 = f8(X3)
| f10(X3) = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_27) ).
fof(f53,plain,
! [X2,X3,X0,X1] :
( big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) = X1
| f7(X0) != X0
| ~ big_f(X2,f10(X3))
| f8(X3) = X2
| f10(X3) = X3 ),
inference(reorient_equations,[],[f52]) ).
fof(f54,negated_conjecture,
! [X2,X3,X0,X1] :
( big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) = X1
| f7(X0) != X0
| big_f(X2,f10(X3))
| X2 != f8(X3)
| f10(X3) = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_28) ).
fof(f55,plain,
! [X2,X3,X0,X1] :
( big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) = X1
| f7(X0) != X0
| big_f(X2,f10(X3))
| f8(X3) != X2
| f10(X3) = X3 ),
inference(reorient_equations,[],[f54]) ).
fof(f56,negated_conjecture,
! [X2,X3,X0,X1] :
( big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) = X1
| f7(X0) != X0
| big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) = X3
| f10(X2) != X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_29) ).
fof(f57,negated_conjecture,
! [X2,X3,X0,X1] :
( big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) = X1
| f7(X0) != X0
| ~ big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) != X3
| f10(X2) != X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_30) ).
fof(f58,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) != X1
| f7(X0) != X0
| ~ big_f(X2,f10(X3))
| X2 = f8(X3)
| f10(X3) = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_31) ).
fof(f59,plain,
! [X2,X3,X0,X1] :
( ~ big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) != X1
| f7(X0) != X0
| ~ big_f(X2,f10(X3))
| f8(X3) = X2
| f10(X3) = X3 ),
inference(reorient_equations,[],[f58]) ).
fof(f60,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) != X1
| f7(X0) != X0
| big_f(X2,f10(X3))
| X2 != f8(X3)
| f10(X3) = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_32) ).
fof(f61,plain,
! [X2,X3,X0,X1] :
( ~ big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) != X1
| f7(X0) != X0
| big_f(X2,f10(X3))
| f8(X3) != X2
| f10(X3) = X3 ),
inference(reorient_equations,[],[f60]) ).
fof(f62,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) != X1
| f7(X0) != X0
| big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) = X3
| f10(X2) != X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_33) ).
fof(f63,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) != X1
| f7(X0) != X0
| ~ big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) != X3
| f10(X2) != X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_34) ).
fof(f64,plain,
! [X2,X0,X1] :
( big_f(X0,f1(X0,X1))
| f1(X0,X1) = X1
| c3 = X0
| ~ big_f(X2,c4)
| f4(c4) = X2 ),
inference(equality_resolution,[],[f9]) ).
fof(f65,plain,
! [X3,X0,X1] :
( big_f(X0,f1(X0,X1))
| f1(X0,X1) = X1
| c3 = X0
| big_f(f4(X3),X3)
| c4 != X3 ),
inference(equality_resolution,[],[f11]) ).
fof(f66,plain,
! [X0,X1] :
( big_f(X0,f1(X0,X1))
| f1(X0,X1) = X1
| c3 = X0
| big_f(f4(c4),c4) ),
inference(equality_resolution,[],[f65]) ).
fof(f67,plain,
! [X2,X0,X1] :
( ~ big_f(X0,f1(X0,X1))
| f1(X0,X1) != X1
| c3 = X0
| ~ big_f(X2,c4)
| f4(c4) = X2 ),
inference(equality_resolution,[],[f17]) ).
fof(f68,plain,
! [X3,X0,X1] :
( ~ big_f(X0,f1(X0,X1))
| f1(X0,X1) != X1
| c3 = X0
| big_f(f4(X3),X3)
| c4 != X3 ),
inference(equality_resolution,[],[f19]) ).
fof(f69,plain,
! [X0,X1] :
( ~ big_f(X0,f1(X0,X1))
| f1(X0,X1) != X1
| c3 = X0
| big_f(f4(c4),c4) ),
inference(equality_resolution,[],[f68]) ).
fof(f70,plain,
! [X2,X3,X1] :
( ~ big_f(c3,X1)
| f2(c3) = X1
| big_f(f3(X2,X3),X2)
| f3(X2,X3) = X3
| c4 = X2 ),
inference(equality_resolution,[],[f21]) ).
fof(f71,plain,
! [X2,X3,X1] :
( ~ big_f(c3,X1)
| f2(c3) = X1
| ~ big_f(f3(X2,X3),X2)
| f3(X2,X3) != X3
| c4 = X2 ),
inference(equality_resolution,[],[f23]) ).
fof(f72,plain,
! [X2,X3,X1] :
( ~ big_f(c3,X1)
| f2(c3) = X1
| ~ big_f(X2,X3)
| f4(X3) = X2
| c4 != X3 ),
inference(equality_resolution,[],[f25]) ).
fof(f73,plain,
! [X2,X1] :
( ~ big_f(c3,X1)
| f2(c3) = X1
| ~ big_f(X2,c4)
| f4(c4) = X2 ),
inference(equality_resolution,[],[f72]) ).
fof(f74,plain,
! [X2,X3,X1] :
( ~ big_f(c3,X1)
| f2(c3) = X1
| big_f(X2,X3)
| f4(X3) != X2
| c4 != X3 ),
inference(equality_resolution,[],[f27]) ).
fof(f75,plain,
! [X3,X1] :
( ~ big_f(c3,X1)
| f2(c3) = X1
| big_f(f4(X3),X3)
| c4 != X3 ),
inference(equality_resolution,[],[f74]) ).
fof(f76,plain,
! [X1] :
( ~ big_f(c3,X1)
| f2(c3) = X1
| big_f(f4(c4),c4) ),
inference(equality_resolution,[],[f75]) ).
fof(f77,plain,
! [X2,X3,X0] :
( big_f(X0,f2(X0))
| c3 != X0
| big_f(f3(X2,X3),X2)
| f3(X2,X3) = X3
| c4 = X2 ),
inference(equality_resolution,[],[f29]) ).
fof(f78,plain,
! [X2,X3] :
( big_f(c3,f2(c3))
| big_f(f3(X2,X3),X2)
| f3(X2,X3) = X3
| c4 = X2 ),
inference(equality_resolution,[],[f77]) ).
fof(f79,plain,
! [X2,X3,X0] :
( big_f(X0,f2(X0))
| c3 != X0
| ~ big_f(f3(X2,X3),X2)
| f3(X2,X3) != X3
| c4 = X2 ),
inference(equality_resolution,[],[f31]) ).
fof(f80,plain,
! [X2,X3] :
( big_f(c3,f2(c3))
| ~ big_f(f3(X2,X3),X2)
| f3(X2,X3) != X3
| c4 = X2 ),
inference(equality_resolution,[],[f79]) ).
fof(f84,plain,
! [X2,X3,X0] :
( big_f(X0,f2(X0))
| c3 != X0
| big_f(X2,X3)
| f4(X3) != X2
| c4 != X3 ),
inference(equality_resolution,[],[f35]) ).
fof(f85,plain,
! [X2,X3] :
( big_f(c3,f2(c3))
| big_f(X2,X3)
| f4(X3) != X2
| c4 != X3 ),
inference(equality_resolution,[],[f84]) ).
fof(f86,plain,
! [X3] :
( big_f(c3,f2(c3))
| big_f(f4(X3),X3)
| c4 != X3 ),
inference(equality_resolution,[],[f85]) ).
fof(f87,plain,
( big_f(c3,f2(c3))
| big_f(f4(c4),c4) ),
inference(equality_resolution,[],[f86]) ).
fof(f90,plain,
! [X2,X3,X0] :
( big_f(f7(X0),f5(X0))
| f7(X0) = X0
| big_f(X2,f10(X3))
| f8(X3) != X2
| f10(X3) = X3 ),
inference(equality_resolution,[],[f47]) ).
fof(f91,plain,
! [X3,X0] :
( big_f(f7(X0),f5(X0))
| f7(X0) = X0
| big_f(f8(X3),f10(X3))
| f10(X3) = X3 ),
inference(equality_resolution,[],[f90]) ).
fof(f92,plain,
! [X2,X3,X0] :
( big_f(f7(X0),f5(X0))
| f7(X0) = X0
| big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) = X3
| f10(X2) != X2 ),
inference(equality_resolution,[],[f49]) ).
fof(f93,plain,
! [X2,X3,X0] :
( big_f(f7(X0),f5(X0))
| f7(X0) = X0
| ~ big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) != X3
| f10(X2) != X2 ),
inference(equality_resolution,[],[f51]) ).
fof(f94,plain,
! [X3,X0,X1] :
( big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) = X1
| f7(X0) != X0
| big_f(f8(X3),f10(X3))
| f10(X3) = X3 ),
inference(equality_resolution,[],[f55]) ).
fof(f95,plain,
! [X3,X0,X1] :
( ~ big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) != X1
| f7(X0) != X0
| big_f(f8(X3),f10(X3))
| f10(X3) = X3 ),
inference(equality_resolution,[],[f61]) ).
fof(f97,definition,
( spl0_1
<=> ! [X2,X3] :
( ~ big_f(f9(X2,X3),f10(X2))
| f10(X2) != X2
| f9(X2,X3) != X3 ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f98,plain,
( ! [X2,X3] :
( f9(X2,X3) != X3
| f10(X2) != X2
| ~ big_f(f9(X2,X3),f10(X2)) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f97]) ).
fof(f100,definition,
( spl0_2
<=> ! [X0,X1] :
( ~ big_f(f7(X0),f6(X0,X1))
| f7(X0) != X0
| f6(X0,X1) != X1 ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f101,plain,
( ! [X0,X1] :
( f6(X0,X1) != X1
| f7(X0) != X0
| ~ big_f(f7(X0),f6(X0,X1)) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f102,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f63,f100,f97]) ).
fof(f104,definition,
( spl0_3
<=> ! [X2,X3] :
( big_f(f9(X2,X3),f10(X2))
| f10(X2) != X2
| f9(X2,X3) = X3 ) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f105,plain,
( ! [X2,X3] :
( f10(X2) != X2
| big_f(f9(X2,X3),f10(X2))
| f9(X2,X3) = X3 )
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f104]) ).
fof(f106,plain,
( spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f62,f100,f104]) ).
fof(f108,definition,
( spl0_4
<=> ! [X3] :
( big_f(f8(X3),f10(X3))
| f10(X3) = X3 ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f109,plain,
( ! [X3] :
( big_f(f8(X3),f10(X3))
| f10(X3) = X3 )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f108]) ).
fof(f110,plain,
( spl0_4
| spl0_2 ),
inference(avatar_split_clause,[],[f95,f100,f108]) ).
fof(f112,definition,
( spl0_5
<=> ! [X2,X3] :
( ~ big_f(X2,f10(X3))
| f10(X3) = X3
| f8(X3) = X2 ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f113,plain,
( ! [X2,X3] :
( ~ big_f(X2,f10(X3))
| f10(X3) = X3
| f8(X3) = X2 )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f112]) ).
fof(f114,plain,
( spl0_5
| spl0_2 ),
inference(avatar_split_clause,[],[f59,f100,f112]) ).
fof(f116,definition,
( spl0_6
<=> ! [X0,X1] :
( big_f(f7(X0),f6(X0,X1))
| f7(X0) != X0
| f6(X0,X1) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f117,plain,
( ! [X0,X1] :
( f7(X0) != X0
| big_f(f7(X0),f6(X0,X1))
| f6(X0,X1) = X1 )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f116]) ).
fof(f118,plain,
( spl0_1
| spl0_6 ),
inference(avatar_split_clause,[],[f57,f116,f97]) ).
fof(f119,plain,
( spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f56,f116,f104]) ).
fof(f120,plain,
( spl0_4
| spl0_6 ),
inference(avatar_split_clause,[],[f94,f116,f108]) ).
fof(f121,plain,
( spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f53,f116,f112]) ).
fof(f123,definition,
( spl0_7
<=> ! [X0] :
( big_f(f7(X0),f5(X0))
| f7(X0) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f124,plain,
( ! [X0] :
( big_f(f7(X0),f5(X0))
| f7(X0) = X0 )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f123]) ).
fof(f125,plain,
( spl0_1
| spl0_7 ),
inference(avatar_split_clause,[],[f93,f123,f97]) ).
fof(f126,plain,
( spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f92,f123,f104]) ).
fof(f127,plain,
( spl0_4
| spl0_7 ),
inference(avatar_split_clause,[],[f91,f123,f108]) ).
fof(f130,definition,
( spl0_8
<=> ! [X0,X1] :
( ~ big_f(f7(X0),X1)
| f7(X0) = X0
| f5(X0) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f131,plain,
( ! [X0,X1] :
( ~ big_f(f7(X0),X1)
| f7(X0) = X0
| f5(X0) = X1 )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f130]) ).
fof(f132,plain,
( spl0_1
| spl0_8 ),
inference(avatar_split_clause,[],[f43,f130,f97]) ).
fof(f133,plain,
( spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f41,f130,f104]) ).
fof(f135,plain,
( spl0_5
| spl0_8 ),
inference(avatar_split_clause,[],[f37,f130,f112]) ).
fof(f137,definition,
( spl0_9
<=> big_f(f4(c4),c4) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f139,plain,
( big_f(f4(c4),c4)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f137]) ).
fof(f141,definition,
( spl0_10
<=> big_f(c3,f2(c3)) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f143,plain,
( big_f(c3,f2(c3))
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f141]) ).
fof(f144,plain,
( spl0_9
| spl0_10 ),
inference(avatar_split_clause,[],[f87,f141,f137]) ).
fof(f146,definition,
( spl0_11
<=> ! [X2] :
( ~ big_f(X2,c4)
| f4(c4) = X2 ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f147,plain,
( ! [X2] :
( f4(c4) = X2
| ~ big_f(X2,c4) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f146]) ).
fof(f150,definition,
( spl0_12
<=> ! [X2,X3] :
( ~ big_f(f3(X2,X3),X2)
| c4 = X2
| f3(X2,X3) != X3 ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f151,plain,
( ! [X2,X3] :
( f3(X2,X3) != X3
| c4 = X2
| ~ big_f(f3(X2,X3),X2) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f150]) ).
fof(f152,plain,
( spl0_12
| spl0_10 ),
inference(avatar_split_clause,[],[f80,f141,f150]) ).
fof(f154,definition,
( spl0_13
<=> ! [X2,X3] :
( big_f(f3(X2,X3),X2)
| c4 = X2
| f3(X2,X3) = X3 ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f155,plain,
( ! [X2,X3] :
( big_f(f3(X2,X3),X2)
| c4 = X2
| f3(X2,X3) = X3 )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f156,plain,
( spl0_13
| spl0_10 ),
inference(avatar_split_clause,[],[f78,f141,f154]) ).
fof(f158,definition,
( spl0_14
<=> ! [X1] :
( ~ big_f(c3,X1)
| f2(c3) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f159,plain,
( ! [X1] :
( f2(c3) = X1
| ~ big_f(c3,X1) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f158]) ).
fof(f160,plain,
( spl0_9
| spl0_14 ),
inference(avatar_split_clause,[],[f76,f158,f137]) ).
fof(f161,plain,
( spl0_11
| spl0_14 ),
inference(avatar_split_clause,[],[f73,f158,f146]) ).
fof(f162,plain,
( spl0_12
| spl0_14 ),
inference(avatar_split_clause,[],[f71,f158,f150]) ).
fof(f163,plain,
( spl0_13
| spl0_14 ),
inference(avatar_split_clause,[],[f70,f158,f154]) ).
fof(f165,definition,
( spl0_15
<=> ! [X0,X1] :
( ~ big_f(X0,f1(X0,X1))
| c3 = X0
| f1(X0,X1) != X1 ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f166,plain,
( ! [X0,X1] :
( f1(X0,X1) != X1
| c3 = X0
| ~ big_f(X0,f1(X0,X1)) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f165]) ).
fof(f167,plain,
( spl0_9
| spl0_15 ),
inference(avatar_split_clause,[],[f69,f165,f137]) ).
fof(f168,plain,
( spl0_11
| spl0_15 ),
inference(avatar_split_clause,[],[f67,f165,f146]) ).
fof(f169,plain,
( spl0_12
| spl0_15 ),
inference(avatar_split_clause,[],[f15,f165,f150]) ).
fof(f170,plain,
( spl0_13
| spl0_15 ),
inference(avatar_split_clause,[],[f13,f165,f154]) ).
fof(f172,definition,
( spl0_16
<=> ! [X0,X1] :
( big_f(X0,f1(X0,X1))
| c3 = X0
| f1(X0,X1) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f173,plain,
( ! [X0,X1] :
( big_f(X0,f1(X0,X1))
| c3 = X0
| f1(X0,X1) = X1 )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f172]) ).
fof(f174,plain,
( spl0_9
| spl0_16 ),
inference(avatar_split_clause,[],[f66,f172,f137]) ).
fof(f175,plain,
( spl0_11
| spl0_16 ),
inference(avatar_split_clause,[],[f64,f172,f146]) ).
fof(f176,plain,
( spl0_12
| spl0_16 ),
inference(avatar_split_clause,[],[f7,f172,f150]) ).
fof(f177,plain,
( spl0_13
| spl0_16 ),
inference(avatar_split_clause,[],[f5,f172,f154]) ).
fof(f183,plain,
( ! [X0,X1] :
( big_f(c1,X0)
| c4 = X0
| c1 = X1
| c2 = f3(X0,X1) )
| ~ spl0_13 ),
inference(superposition,[],[f155,f3]) ).
fof(f190,plain,
( ! [X0,X1] :
( f5(X0) = X1
| c1 = X0
| ~ big_f(c1,X1)
| c2 = f7(X0) )
| ~ spl0_8 ),
inference(superposition,[],[f131,f3]) ).
fof(f192,plain,
( ! [X0] :
( big_f(f7(X0),c1)
| f7(X0) = X0
| c2 = f5(X0) )
| ~ spl0_7 ),
inference(superposition,[],[f124,f3]) ).
fof(f193,plain,
( ! [X0,X1] :
( f7(X0) != X0
| c1 != X1
| ~ big_f(f7(X0),c1)
| c2 = f6(X0,X1) )
| ~ spl0_2 ),
inference(superposition,[],[f101,f3]) ).
fof(f196,definition,
( spl0_17
<=> ! [X0] : c2 = X0 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f197,plain,
( ! [X0] : c2 = X0
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f196]) ).
fof(f199,definition,
( spl0_18
<=> c2 = c1 ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f201,plain,
( c2 != c1
| spl0_18 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f204,definition,
( spl0_19
<=> c2 = f4(c4) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f206,plain,
( c2 = f4(c4)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f208,definition,
( spl0_20
<=> big_f(c1,c4) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f210,plain,
( big_f(c1,c4)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f213,definition,
( spl0_21
<=> ! [X0] :
( c1 = X0
| ~ big_f(X0,c4) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f214,plain,
( ! [X0] :
( ~ big_f(X0,c4)
| c1 = X0 )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f213]) ).
fof(f217,definition,
( spl0_22
<=> c2 = c4 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f219,plain,
( c2 = c4
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f217]) ).
fof(f221,definition,
( spl0_23
<=> big_f(f4(c1),c1) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f223,plain,
( big_f(f4(c1),c1)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f226,definition,
( spl0_24
<=> ! [X0] :
( f4(c1) = X0
| ~ big_f(X0,c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f227,plain,
( ! [X0] :
( f4(c1) = X0
| ~ big_f(X0,c1) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f232,definition,
( spl0_25
<=> c2 = f2(c3) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f234,plain,
( c2 = f2(c3)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f236,definition,
( spl0_26
<=> big_f(c3,c1) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f237,plain,
( ~ big_f(c3,c1)
| spl0_26 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f238,plain,
( big_f(c3,c1)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f241,definition,
( spl0_27
<=> c2 = c3 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f243,plain,
( c2 = c3
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f241]) ).
fof(f267,definition,
( spl0_30
<=> ! [X0] :
( f2(c1) = X0
| ~ big_f(c1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f268,plain,
( ! [X0] :
( f2(c1) = X0
| ~ big_f(c1,X0) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f267]) ).
fof(f270,plain,
( ! [X0,X1] :
( c1 != X1
| c3 = X0
| ~ big_f(X0,c1)
| c2 = f1(X0,X1) )
| ~ spl0_15 ),
inference(superposition,[],[f166,f3]) ).
fof(f273,plain,
( big_f(f4(c2),c2)
| ~ spl0_9
| ~ spl0_22 ),
inference(superposition,[],[f139,f219]) ).
fof(f277,definition,
( spl0_31
<=> c2 = f4(c2) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f279,plain,
( c2 = f4(c2)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f281,definition,
( spl0_32
<=> big_f(c1,c2) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f282,plain,
( ~ big_f(c1,c2)
| spl0_32 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f283,plain,
( big_f(c1,c2)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f289,plain,
( big_f(c2,c4)
| ~ spl0_9
| ~ spl0_19 ),
inference(superposition,[],[f139,f206]) ).
fof(f291,definition,
( spl0_33
<=> c2 = f4(c1) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f293,plain,
( c2 = f4(c1)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f302,plain,
( ! [X0,X1] :
( X0 = X1
| ~ big_f(c3,X1)
| ~ big_f(c3,X0) )
| ~ spl0_14 ),
inference(superposition,[],[f159,f159]) ).
fof(f314,plain,
( big_f(c2,f2(c2))
| ~ spl0_10
| ~ spl0_27 ),
inference(superposition,[],[f143,f243]) ).
fof(f318,definition,
( spl0_34
<=> big_f(c1,c1) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f319,plain,
( ~ big_f(c1,c1)
| spl0_34 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f320,plain,
( big_f(c1,c1)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f322,plain,
( ! [X0] :
( big_f(X0,X0)
| c2 = X0 )
| ~ spl0_34 ),
inference(superposition,[],[f320,f3]) ).
fof(f323,plain,
( ! [X0,X1] :
( big_f(X0,f1(X0,X1))
| c2 = X0
| f1(X0,X1) = X1 )
| ~ spl0_16
| ~ spl0_27 ),
inference(forward_demodulation,[],[f173,f243]) ).
fof(f325,plain,
( c2 = f2(c2)
| ~ spl0_25
| ~ spl0_27 ),
inference(forward_demodulation,[],[f234,f243]) ).
fof(f326,plain,
( ! [X0,X1] :
( c1 != X0
| c1 != X1
| ~ big_f(c1,c1)
| c2 = f6(X0,X1)
| c2 = f7(X0) )
| ~ spl0_2 ),
inference(superposition,[],[f193,f3]) ).
fof(f327,plain,
( ! [X0,X1] :
( c1 != X1
| c1 != X0
| c2 = f6(X0,X1)
| c2 = f7(X0) )
| ~ spl0_2
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f326,f320]) ).
fof(f329,plain,
( ! [X0,X1] :
( ~ big_f(c2,X1)
| X0 = X1
| ~ big_f(c3,X0) )
| ~ spl0_14
| ~ spl0_27 ),
inference(forward_demodulation,[],[f302,f243]) ).
fof(f330,plain,
( ! [X0,X1] :
( ~ big_f(c2,X0)
| ~ big_f(c2,X1)
| X0 = X1 )
| ~ spl0_14
| ~ spl0_27 ),
inference(forward_demodulation,[],[f329,f243]) ).
fof(f334,plain,
( ! [X0,X1] :
( c2 = f1(X0,X1)
| c2 = X0
| c1 = X1
| big_f(X0,c1) )
| ~ spl0_16
| ~ spl0_27 ),
inference(superposition,[],[f323,f3]) ).
fof(f338,plain,
~ spl0_18,
inference(avatar_split_clause,[],[f1,f199]) ).
fof(f346,definition,
( spl0_35
<=> ! [X0] :
( c1 = X0
| ~ big_f(X0,c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f347,plain,
( ! [X0] :
( ~ big_f(X0,c1)
| c1 = X0 )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f383,definition,
( spl0_39
<=> ! [X0] : ~ big_f(X0,c1) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f384,plain,
( ! [X0] : ~ big_f(X0,c1)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f406,plain,
( big_f(c2,c2)
| ~ spl0_10
| ~ spl0_25
| ~ spl0_27 ),
inference(forward_demodulation,[],[f314,f325]) ).
fof(f410,plain,
( big_f(c2,c1)
| ~ spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f238,f243]) ).
fof(f412,plain,
( c2 = c1
| ~ spl0_26
| ~ spl0_27
| ~ spl0_35 ),
inference(resolution,[],[f410,f347]) ).
fof(f414,plain,
( spl0_18
| ~ spl0_26
| ~ spl0_27
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f412,f346,f241,f236,f199]) ).
fof(f431,plain,
( ! [X0] :
( big_f(c1,c1)
| c1 = X0
| c2 = f5(X0)
| c2 = f7(X0) )
| ~ spl0_7 ),
inference(superposition,[],[f192,f3]) ).
fof(f435,plain,
( ! [X0] :
( c1 != X0
| c2 = f6(X0,c1)
| c2 = f7(X0) )
| ~ spl0_2
| ~ spl0_34 ),
inference(equality_resolution,[],[f327]) ).
fof(f437,plain,
( c2 = f6(c1,c1)
| c2 = f7(c1)
| ~ spl0_2
| ~ spl0_34 ),
inference(equality_resolution,[],[f435]) ).
fof(f439,definition,
( spl0_41
<=> c2 = f7(c1) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f440,plain,
( c2 != f7(c1)
| spl0_41 ),
inference(avatar_component_clause,[],[f439]) ).
fof(f441,plain,
( c2 = f7(c1)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f439]) ).
fof(f443,definition,
( spl0_42
<=> c2 = f6(c1,c1) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f445,plain,
( c2 = f6(c1,c1)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f447,plain,
( ! [X0] :
( c2 = f7(X0)
| c2 = X0 )
| ~ spl0_41 ),
inference(superposition,[],[f441,f3]) ).
fof(f453,plain,
( big_f(c2,f5(c1))
| c2 = c1
| ~ spl0_7
| ~ spl0_41 ),
inference(superposition,[],[f124,f441]) ).
fof(f455,definition,
( spl0_43
<=> big_f(c2,f5(c1)) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f457,plain,
( big_f(c2,f5(c1))
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f485,plain,
( ! [X0,X1] :
( ~ big_f(c2,X1)
| c2 = X0
| f5(X0) = X1
| c2 = X0 )
| ~ spl0_8
| ~ spl0_41 ),
inference(superposition,[],[f131,f447]) ).
fof(f486,plain,
( ! [X0] :
( big_f(c2,f5(X0))
| c2 = X0
| c2 = X0 )
| ~ spl0_7
| ~ spl0_41 ),
inference(superposition,[],[f124,f447]) ).
fof(f487,plain,
( ! [X0] :
( big_f(c2,f5(X0))
| c2 = X0 )
| ~ spl0_7
| ~ spl0_41 ),
inference(duplicate_literal_removal,[],[f486]) ).
fof(f488,plain,
( ! [X0,X1] :
( f5(X0) = X1
| c2 = X0
| ~ big_f(c2,X1) )
| ~ spl0_8
| ~ spl0_41 ),
inference(duplicate_literal_removal,[],[f485]) ).
fof(f503,definition,
( spl0_47
<=> ! [X0,X1] :
( X0 = X1
| ~ big_f(c2,X0)
| ~ big_f(c2,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f504,plain,
( ! [X0,X1] :
( ~ big_f(c2,X1)
| ~ big_f(c2,X0)
| X0 = X1 )
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f508,plain,
( spl0_47
| ~ spl0_14
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f330,f241,f158,f503]) ).
fof(f511,plain,
( ! [X0,X1] :
( c2 != X1
| c3 = X0
| ~ big_f(X0,c2)
| c2 = X0
| c1 = X1
| big_f(X0,c1) )
| ~ spl0_15
| ~ spl0_16
| ~ spl0_27 ),
inference(superposition,[],[f166,f334]) ).
fof(f529,plain,
( ! [X0,X1] :
( c1 != X1
| c2 = X0
| ~ big_f(X0,c1)
| c2 = f1(X0,X1) )
| ~ spl0_15
| ~ spl0_27 ),
inference(forward_demodulation,[],[f270,f243]) ).
fof(f564,plain,
( ! [X0] :
( c2 = f1(X0,c1)
| ~ big_f(X0,c1)
| c2 = X0 )
| ~ spl0_15
| ~ spl0_27 ),
inference(equality_resolution,[],[f529]) ).
fof(f567,plain,
( ! [X0] :
( big_f(X0,c2)
| c2 = X0
| c2 = c1
| ~ big_f(X0,c1)
| c2 = X0 )
| ~ spl0_15
| ~ spl0_16
| ~ spl0_27 ),
inference(superposition,[],[f323,f564]) ).
fof(f569,plain,
( ! [X0] :
( big_f(X0,c2)
| c2 = X0
| c2 = c1
| ~ big_f(X0,c1) )
| ~ spl0_15
| ~ spl0_16
| ~ spl0_27 ),
inference(duplicate_literal_removal,[],[f567]) ).
fof(f591,plain,
( ! [X0,X1] :
( c3 = X0
| ~ big_f(X0,c2)
| c2 = X0
| c1 = X1
| big_f(X0,c1) )
| ~ spl0_15
| ~ spl0_16
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f511,f3]) ).
fof(f592,plain,
( ! [X0] :
( big_f(X0,c2)
| c2 = X0
| ~ big_f(X0,c1) )
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f569,f201]) ).
fof(f593,plain,
( ! [X0,X1] :
( c2 = X0
| ~ big_f(X0,c2)
| c2 = X0
| c1 = X1
| big_f(X0,c1) )
| ~ spl0_15
| ~ spl0_16
| ~ spl0_27 ),
inference(forward_demodulation,[],[f591,f243]) ).
fof(f594,plain,
( ! [X0,X1] :
( c2 = X0
| ~ big_f(X0,c2)
| c1 = X1
| big_f(X0,c1) )
| ~ spl0_15
| ~ spl0_16
| ~ spl0_27 ),
inference(duplicate_literal_removal,[],[f593]) ).
fof(f596,definition,
( spl0_48
<=> ! [X1] : c1 = X1 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f597,plain,
( ! [X1] : c1 = X1
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f596]) ).
fof(f599,definition,
( spl0_49
<=> ! [X0] :
( c2 = X0
| big_f(X0,c1)
| ~ big_f(X0,c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f600,plain,
( ! [X0] :
( big_f(X0,c1)
| c2 = X0
| ~ big_f(X0,c2) )
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f599]) ).
fof(f601,plain,
( spl0_48
| spl0_49
| ~ spl0_15
| ~ spl0_16
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f594,f241,f172,f165,f599,f596]) ).
fof(f620,plain,
( ! [X2,X0,X1] :
( X0 = X2
| c1 = X1
| ~ big_f(c1,X2)
| c2 = f7(X1)
| c1 = X1
| ~ big_f(c1,X0)
| c2 = f7(X1) )
| ~ spl0_8 ),
inference(superposition,[],[f190,f190]) ).
fof(f623,plain,
( ! [X0,X1] :
( c1 = X1
| c1 = X0
| ~ big_f(c1,X1)
| c2 = f7(X0)
| c2 = f5(X0) )
| ~ spl0_8 ),
inference(superposition,[],[f190,f3]) ).
fof(f628,plain,
( ! [X2,X0,X1] :
( X0 = X2
| c1 = X1
| ~ big_f(c1,X2)
| c2 = f7(X1)
| ~ big_f(c1,X0) )
| ~ spl0_8 ),
inference(duplicate_literal_removal,[],[f620]) ).
fof(f630,definition,
( spl0_50
<=> ! [X0] :
( c1 = X0
| c2 = f5(X0)
| c2 = f7(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f631,plain,
( ! [X0] :
( c2 = f5(X0)
| c1 = X0
| c2 = f7(X0) )
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f630]) ).
fof(f633,definition,
( spl0_51
<=> ! [X1] :
( c1 = X1
| ~ big_f(c1,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f634,plain,
( ! [X1] :
( ~ big_f(c1,X1)
| c1 = X1 )
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f635,plain,
( spl0_50
| spl0_51
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f623,f130,f633,f630]) ).
fof(f637,definition,
( spl0_52
<=> ! [X1] :
( c1 = X1
| c2 = f7(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f638,plain,
( ! [X1] :
( c2 = f7(X1)
| c1 = X1 )
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f640,definition,
( spl0_53
<=> ! [X2,X0] :
( X0 = X2
| ~ big_f(c1,X0)
| ~ big_f(c1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f641,plain,
( ! [X2,X0] :
( ~ big_f(c1,X2)
| ~ big_f(c1,X0)
| X0 = X2 )
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f640]) ).
fof(f642,plain,
( spl0_52
| spl0_53
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f628,f130,f640,f637]) ).
fof(f643,plain,
( ! [X0] :
( ~ big_f(c1,X0)
| c1 = X0 )
| ~ spl0_34
| ~ spl0_53 ),
inference(resolution,[],[f641,f320]) ).
fof(f644,plain,
( ! [X0] :
( ~ big_f(c1,X0)
| c1 = X0
| c2 = c1 )
| ~ spl0_34
| ~ spl0_53 ),
inference(resolution,[],[f641,f322]) ).
fof(f645,plain,
( ! [X0] :
( ~ big_f(c1,X0)
| c2 = X0
| c2 = c1
| ~ big_f(c1,c1) )
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_27
| ~ spl0_53 ),
inference(resolution,[],[f641,f592]) ).
fof(f646,plain,
( ! [X0] :
( ~ big_f(c1,X0)
| c1 = X0
| c2 = c1
| ~ big_f(c1,c2) )
| ~ spl0_49
| ~ spl0_53 ),
inference(resolution,[],[f641,f600]) ).
fof(f651,plain,
( ! [X0] :
( ~ big_f(c1,X0)
| c1 = X0
| ~ big_f(c1,c2) )
| spl0_18
| ~ spl0_49
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f646,f201]) ).
fof(f653,plain,
( ! [X0] :
( ~ big_f(c1,X0)
| c1 = X0 )
| spl0_18
| ~ spl0_34
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f644,f201]) ).
fof(f654,plain,
( spl0_51
| ~ spl0_34
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f643,f640,f318,f633]) ).
fof(f655,plain,
( ~ spl0_32
| spl0_51
| spl0_18
| ~ spl0_49
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f651,f640,f599,f199,f633,f281]) ).
fof(f657,plain,
( spl0_51
| spl0_18
| ~ spl0_34
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f653,f640,f318,f199,f633]) ).
fof(f675,definition,
( spl0_55
<=> big_f(c2,c1) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f676,plain,
( ~ big_f(c2,c1)
| spl0_55 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f677,plain,
( big_f(c2,c1)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f680,definition,
( spl0_56
<=> ! [X0] :
( c1 = X0
| ~ big_f(c2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f681,plain,
( ! [X0] :
( ~ big_f(c2,X0)
| c1 = X0 )
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f680]) ).
fof(f684,definition,
( spl0_57
<=> ! [X0] :
( c2 = X0
| c2 = f5(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f685,plain,
( ! [X0] :
( c2 = f5(X0)
| c2 = X0 )
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f684]) ).
fof(f690,plain,
( ! [X0] :
( ~ big_f(c2,X0)
| c1 = X0 )
| ~ spl0_47
| ~ spl0_55 ),
inference(resolution,[],[f677,f504]) ).
fof(f692,plain,
( spl0_56
| ~ spl0_47
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f690,f675,f503,f680]) ).
fof(f693,plain,
( big_f(c1,c1)
| c2 = c3
| ~ spl0_26 ),
inference(superposition,[],[f238,f3]) ).
fof(f704,definition,
( spl0_59
<=> c1 = c3 ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f705,plain,
( c1 != c3
| spl0_59 ),
inference(avatar_component_clause,[],[f704]) ).
fof(f706,plain,
( c1 = c3
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f704]) ).
fof(f716,plain,
( big_f(c1,c1)
| ~ spl0_26
| ~ spl0_59 ),
inference(superposition,[],[f238,f706]) ).
fof(f734,plain,
( c1 = f5(c1)
| ~ spl0_43
| ~ spl0_56 ),
inference(resolution,[],[f681,f457]) ).
fof(f738,plain,
( ! [X0] :
( c1 = f1(c2,X0)
| c2 = c3
| f1(c2,X0) = X0 )
| ~ spl0_16
| ~ spl0_56 ),
inference(resolution,[],[f681,f173]) ).
fof(f739,plain,
( ! [X0] :
( c2 = c1
| c1 = f1(c2,X0)
| f1(c2,X0) = X0 )
| ~ spl0_16
| ~ spl0_56
| ~ spl0_59 ),
inference(forward_demodulation,[],[f738,f706]) ).
fof(f740,plain,
( ! [X0] :
( f1(c2,X0) = X0
| c1 = f1(c2,X0) )
| ~ spl0_16
| spl0_18
| ~ spl0_56
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f739,f201]) ).
fof(f741,plain,
( ! [X0] :
( f5(X0) = X0
| c2 = X0 )
| ~ spl0_43
| ~ spl0_56 ),
inference(superposition,[],[f734,f3]) ).
fof(f745,plain,
( big_f(c2,c1)
| ~ spl0_43
| ~ spl0_56 ),
inference(superposition,[],[f457,f734]) ).
fof(f763,plain,
( ! [X0,X1] :
( c2 = X0
| c1 = X1
| c2 = f7(X1)
| c1 = X1
| ~ big_f(c1,X0)
| c2 = f7(X1) )
| ~ spl0_8
| ~ spl0_50 ),
inference(superposition,[],[f631,f190]) ).
fof(f771,plain,
( ! [X0,X1] :
( c2 = X0
| c1 = X1
| c2 = f7(X1)
| ~ big_f(c1,X0) )
| ~ spl0_8
| ~ spl0_50 ),
inference(duplicate_literal_removal,[],[f763]) ).
fof(f773,definition,
( spl0_62
<=> ! [X1] :
( c2 = X1
| ~ big_f(c1,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f774,plain,
( ! [X1] :
( ~ big_f(c1,X1)
| c2 = X1 )
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f773]) ).
fof(f776,plain,
( spl0_52
| spl0_62
| ~ spl0_8
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f771,f630,f130,f773,f637]) ).
fof(f777,plain,
( c2 = c1
| ~ spl0_34
| ~ spl0_62 ),
inference(resolution,[],[f774,f320]) ).
fof(f780,plain,
( c2 = c1
| c2 = c1
| ~ big_f(c1,c2)
| ~ spl0_49
| ~ spl0_62 ),
inference(resolution,[],[f774,f600]) ).
fof(f787,plain,
( $false
| spl0_18
| ~ spl0_34
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f777,f201]) ).
fof(f788,plain,
( spl0_18
| ~ spl0_34
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f787]) ).
fof(f795,plain,
( c2 = c1
| big_f(c1,c1)
| ~ spl0_26
| ~ spl0_59 ),
inference(forward_demodulation,[],[f693,f706]) ).
fof(f796,plain,
( spl0_34
| ~ spl0_26
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f716,f704,f236,f318]) ).
fof(f820,plain,
( big_f(c1,c1)
| spl0_18
| ~ spl0_26
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f795,f201]) ).
fof(f823,plain,
( spl0_50
| spl0_34
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f431,f123,f318,f630]) ).
fof(f826,plain,
( spl0_34
| spl0_18
| ~ spl0_26
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f820,f704,f236,f199,f318]) ).
fof(f830,plain,
( ! [X0] :
( big_f(X0,X0)
| c2 = X0 )
| ~ spl0_34 ),
inference(superposition,[],[f320,f3]) ).
fof(f850,plain,
( big_f(c2,c1)
| c2 = c1
| ~ spl0_43
| ~ spl0_56 ),
inference(superposition,[],[f457,f741]) ).
fof(f855,plain,
( ! [X0] :
( X0 != X0
| c2 = c3
| ~ big_f(c2,X0)
| c1 = f1(c2,X0) )
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_56
| ~ spl0_59 ),
inference(superposition,[],[f166,f740]) ).
fof(f857,plain,
( ! [X0] :
( c2 = c3
| ~ big_f(c2,X0)
| c1 = f1(c2,X0) )
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_56
| ~ spl0_59 ),
inference(trivial_inequality_removal,[],[f855]) ).
fof(f858,plain,
( ! [X0] :
( c2 = c1
| ~ big_f(c2,X0)
| c1 = f1(c2,X0) )
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_56
| ~ spl0_59 ),
inference(forward_demodulation,[],[f857,f706]) ).
fof(f859,plain,
( ! [X0] :
( c1 = f1(c2,X0)
| ~ big_f(c2,X0) )
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_56
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f858,f201]) ).
fof(f862,plain,
( ! [X0] :
( c1 != X0
| c2 = c3
| ~ big_f(c2,c1)
| ~ big_f(c2,X0) )
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_56
| ~ spl0_59 ),
inference(superposition,[],[f166,f859]) ).
fof(f863,plain,
( ! [X0] :
( c2 = c3
| ~ big_f(c2,c1)
| ~ big_f(c2,X0) )
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_47
| ~ spl0_56
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f862,f504]) ).
fof(f864,plain,
( ! [X0] :
( c2 = c3
| ~ big_f(c2,X0) )
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_47
| ~ spl0_55
| ~ spl0_56
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f863,f677]) ).
fof(f865,plain,
( ! [X0] :
( c2 = c1
| ~ big_f(c2,X0) )
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_47
| ~ spl0_55
| ~ spl0_56
| ~ spl0_59 ),
inference(forward_demodulation,[],[f864,f706]) ).
fof(f866,plain,
( ! [X0] : ~ big_f(c2,X0)
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_47
| ~ spl0_55
| ~ spl0_56
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f865,f201]) ).
fof(f870,plain,
( ! [X0] : c2 = X0
| ~ spl0_7
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_41
| ~ spl0_47
| ~ spl0_55
| ~ spl0_56
| ~ spl0_59 ),
inference(resolution,[],[f866,f487]) ).
fof(f877,plain,
( spl0_17
| ~ spl0_7
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_41
| ~ spl0_47
| ~ spl0_55
| ~ spl0_56
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f870,f704,f680,f675,f503,f439,f199,f172,f165,f123,f196]) ).
fof(f921,plain,
( spl0_55
| ~ spl0_43
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f745,f680,f455,f675]) ).
fof(f923,plain,
( big_f(c2,c1)
| spl0_18
| ~ spl0_43
| ~ spl0_56 ),
inference(forward_subsumption_resolution,[],[f850,f201]) ).
fof(f928,plain,
( spl0_55
| spl0_18
| ~ spl0_43
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f923,f680,f455,f199,f675]) ).
fof(f930,definition,
( spl0_69
<=> c1 = f7(c1) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f931,plain,
( c1 != f7(c1)
| spl0_69 ),
inference(avatar_component_clause,[],[f930]) ).
fof(f932,plain,
( c1 = f7(c1)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f930]) ).
fof(f999,definition,
( spl0_73
<=> big_f(f7(c1),c2) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f1000,plain,
( ~ big_f(f7(c1),c2)
| spl0_73 ),
inference(avatar_component_clause,[],[f999]) ).
fof(f1001,plain,
( big_f(f7(c1),c2)
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f999]) ).
fof(f1008,plain,
( c1 != c1
| c2 = f7(c1)
| spl0_69 ),
inference(superposition,[],[f931,f3]) ).
fof(f1009,plain,
( c2 = f7(c1)
| spl0_69 ),
inference(trivial_inequality_removal,[],[f1008]) ).
fof(f1010,plain,
( $false
| spl0_41
| spl0_69 ),
inference(forward_subsumption_resolution,[],[f1009,f440]) ).
fof(f1011,plain,
( spl0_41
| spl0_69 ),
inference(avatar_contradiction_clause,[],[f1010]) ).
fof(f1016,plain,
( ! [X0] :
( f7(X0) = X0
| c2 = X0 )
| ~ spl0_69 ),
inference(superposition,[],[f932,f3]) ).
fof(f1018,plain,
( ! [X0] :
( c1 != c1
| big_f(c1,f6(c1,X0))
| f6(c1,X0) = X0 )
| ~ spl0_6
| ~ spl0_69 ),
inference(superposition,[],[f117,f932]) ).
fof(f1021,plain,
( ! [X0] :
( big_f(c1,f6(c1,X0))
| f6(c1,X0) = X0 )
| ~ spl0_6
| ~ spl0_69 ),
inference(trivial_inequality_removal,[],[f1018]) ).
fof(f1025,plain,
( ! [X0,X1] :
( ~ big_f(c1,X1)
| X0 = X1
| ~ big_f(c3,X0) )
| ~ spl0_14
| ~ spl0_59 ),
inference(forward_demodulation,[],[f302,f706]) ).
fof(f1026,plain,
( ! [X0,X1] :
( ~ big_f(c1,X0)
| ~ big_f(c1,X1)
| X0 = X1 )
| ~ spl0_14
| ~ spl0_59 ),
inference(forward_demodulation,[],[f1025,f706]) ).
fof(f1030,plain,
( big_f(c1,c2)
| c2 = c1
| ~ spl0_6
| ~ spl0_42
| ~ spl0_69 ),
inference(superposition,[],[f1021,f445]) ).
fof(f1031,plain,
( ! [X0] :
( big_f(c1,c1)
| c1 = X0
| c2 = f6(c1,X0) )
| ~ spl0_6
| ~ spl0_69 ),
inference(superposition,[],[f1021,f3]) ).
fof(f1035,plain,
( ! [X0,X1] :
( f10(X0) != X0
| c1 != X1
| ~ big_f(c1,f10(X0))
| c2 = f9(X0,X1) )
| ~ spl0_1 ),
inference(superposition,[],[f98,f3]) ).
fof(f1044,plain,
( ! [X0,X1] :
( c1 != X0
| big_f(f9(X0,X1),c1)
| f9(X0,X1) = X1
| c2 = f10(X0) )
| ~ spl0_3 ),
inference(superposition,[],[f105,f3]) ).
fof(f1045,plain,
( ! [X0,X1] :
( c1 != X0
| c1 != X1
| ~ big_f(c1,c1)
| c2 = f9(X0,X1)
| c2 = f10(X0) )
| ~ spl0_1 ),
inference(superposition,[],[f1035,f3]) ).
fof(f1046,plain,
( ! [X0,X1] :
( c1 != X1
| c1 != X0
| c2 = f9(X0,X1)
| c2 = f10(X0) )
| ~ spl0_1
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f1045,f320]) ).
fof(f1048,plain,
( ! [X0,X1] :
( X0 != X0
| c1 != X1
| ~ big_f(X0,c1)
| c2 = f6(X0,X1)
| c2 = X0 )
| ~ spl0_2
| ~ spl0_69 ),
inference(superposition,[],[f193,f1016]) ).
fof(f1050,plain,
( ! [X0,X1] :
( c1 != X1
| ~ big_f(X0,c1)
| c2 = f6(X0,X1)
| c2 = X0 )
| ~ spl0_2
| ~ spl0_69 ),
inference(trivial_inequality_removal,[],[f1048]) ).
fof(f1072,plain,
( ! [X0] :
( c2 = f6(X0,c1)
| ~ big_f(X0,c1)
| c2 = X0 )
| ~ spl0_2
| ~ spl0_69 ),
inference(equality_resolution,[],[f1050]) ).
fof(f1096,plain,
( ! [X0] :
( c1 != X0
| c2 = f9(X0,c1)
| c2 = f10(X0) )
| ~ spl0_1
| ~ spl0_34 ),
inference(equality_resolution,[],[f1046]) ).
fof(f1100,definition,
( spl0_75
<=> c2 = f10(c1) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f1101,plain,
( c2 != f10(c1)
| spl0_75 ),
inference(avatar_component_clause,[],[f1100]) ).
fof(f1102,plain,
( c2 = f10(c1)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f1100]) ).
fof(f1104,definition,
( spl0_76
<=> c2 = f9(c1,c1) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f1106,plain,
( c2 = f9(c1,c1)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f1104]) ).
fof(f1113,plain,
( big_f(f8(c1),c2)
| c2 = c1
| ~ spl0_4
| ~ spl0_75 ),
inference(superposition,[],[f109,f1102]) ).
fof(f1114,plain,
( big_f(f8(c1),c2)
| ~ spl0_4
| spl0_18
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f1113,f201]) ).
fof(f1119,definition,
( spl0_77
<=> c2 = f8(c1) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f1121,plain,
( c2 = f8(c1)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f1119]) ).
fof(f1125,plain,
( big_f(c2,c2)
| ~ spl0_4
| spl0_18
| ~ spl0_75
| ~ spl0_77 ),
inference(superposition,[],[f1114,f1121]) ).
fof(f1126,plain,
( big_f(c2,f10(c1))
| c1 = f10(c1)
| ~ spl0_4
| ~ spl0_77 ),
inference(superposition,[],[f109,f1121]) ).
fof(f1127,plain,
( c1 = f10(c1)
| ~ spl0_4
| ~ spl0_56
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f1126,f681]) ).
fof(f1192,plain,
( ! [X0] :
( big_f(f9(c1,X0),c1)
| f9(c1,X0) = X0
| c2 = f10(c1) )
| ~ spl0_3 ),
inference(equality_resolution,[],[f1044]) ).
fof(f1193,plain,
( ! [X0] :
( big_f(f9(c1,X0),c1)
| f9(c1,X0) = X0 )
| ~ spl0_3
| spl0_75 ),
inference(forward_subsumption_resolution,[],[f1192,f1101]) ).
fof(f1194,plain,
( big_f(c2,c1)
| c2 = c1
| ~ spl0_3
| spl0_75
| ~ spl0_76 ),
inference(superposition,[],[f1193,f1106]) ).
fof(f1196,plain,
( ! [X0] :
( big_f(c1,c1)
| c1 = X0
| c2 = f9(c1,X0) )
| ~ spl0_3
| spl0_75 ),
inference(superposition,[],[f1193,f3]) ).
fof(f1209,plain,
( c2 = f6(c1,c1)
| ~ spl0_2
| ~ spl0_34
| spl0_41 ),
inference(forward_subsumption_resolution,[],[f437,f440]) ).
fof(f1216,plain,
( big_f(c1,c2)
| ~ spl0_6
| spl0_18
| ~ spl0_42
| ~ spl0_69 ),
inference(forward_subsumption_resolution,[],[f1030,f201]) ).
fof(f1218,plain,
( spl0_53
| ~ spl0_14
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f1026,f704,f158,f640]) ).
fof(f1232,plain,
( spl0_42
| ~ spl0_2
| ~ spl0_34
| spl0_41 ),
inference(avatar_split_clause,[],[f1209,f439,f318,f100,f443]) ).
fof(f1233,plain,
( spl0_32
| ~ spl0_6
| spl0_18
| ~ spl0_42
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f1216,f930,f443,f199,f116,f281]) ).
fof(f1238,plain,
( big_f(f4(c2),c2)
| ~ spl0_9
| ~ spl0_22 ),
inference(forward_demodulation,[],[f139,f219]) ).
fof(f1239,plain,
( big_f(c2,c2)
| ~ spl0_9
| ~ spl0_22
| ~ spl0_31 ),
inference(forward_demodulation,[],[f273,f279]) ).
fof(f1242,plain,
( ! [X2] :
( ~ big_f(X2,c4)
| c2 = X2 )
| ~ spl0_11
| ~ spl0_19 ),
inference(forward_demodulation,[],[f147,f206]) ).
fof(f1247,plain,
( ! [X2,X3] :
( f3(X2,X3) != X3
| c2 = X2
| ~ big_f(f3(X2,X3),X2) )
| ~ spl0_12
| ~ spl0_22 ),
inference(forward_demodulation,[],[f151,f219]) ).
fof(f1252,plain,
( ! [X2] :
( ~ big_f(X2,c2)
| c2 = X2 )
| ~ spl0_11
| ~ spl0_19
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1242,f219]) ).
fof(f1260,definition,
( spl0_80
<=> c1 = c4 ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f1261,plain,
( c1 != c4
| spl0_80 ),
inference(avatar_component_clause,[],[f1260]) ).
fof(f1262,plain,
( c1 = c4
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f1260]) ).
fof(f1277,plain,
( ! [X0,X1] :
( f7(X0) != X0
| c1 != X1
| ~ big_f(f7(X0),c1)
| c2 = f6(X0,X1) )
| ~ spl0_2 ),
inference(superposition,[],[f101,f3]) ).
fof(f1279,plain,
( ! [X0,X1] :
( X0 = X1
| ~ big_f(X1,c4)
| ~ big_f(X0,c4) )
| ~ spl0_11 ),
inference(superposition,[],[f147,f147]) ).
fof(f1288,plain,
( ! [X0,X1] :
( c1 != X1
| c4 = X0
| ~ big_f(c1,X0)
| c2 = f3(X0,X1) )
| ~ spl0_12 ),
inference(superposition,[],[f151,f3]) ).
fof(f1290,plain,
( ! [X0] :
( f4(c1) = X0
| ~ big_f(X0,c1) )
| ~ spl0_11
| ~ spl0_80 ),
inference(superposition,[],[f147,f1262]) ).
fof(f1292,plain,
( spl0_24
| ~ spl0_11
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f1290,f1260,f146,f226]) ).
fof(f1296,plain,
( ! [X0,X1] :
( X0 != X0
| big_f(X0,f6(X0,X1))
| f6(X0,X1) = X1
| c2 = X0 )
| ~ spl0_6
| ~ spl0_69 ),
inference(superposition,[],[f117,f1016]) ).
fof(f1298,plain,
( ! [X0,X1] :
( big_f(X0,f6(X0,X1))
| f6(X0,X1) = X1
| c2 = X0 )
| ~ spl0_6
| ~ spl0_69 ),
inference(trivial_inequality_removal,[],[f1296]) ).
fof(f1302,plain,
( ! [X0,X1] :
( c2 != X0
| big_f(c2,f6(X0,X1))
| f6(X0,X1) = X1
| c1 = X0 )
| ~ spl0_6
| ~ spl0_52 ),
inference(superposition,[],[f117,f638]) ).
fof(f1311,plain,
( ! [X0,X1] :
( big_f(c2,f6(X0,X1))
| f6(X0,X1) = X1
| c1 = X0 )
| ~ spl0_6
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f1302,f3]) ).
fof(f1313,plain,
( big_f(c1,c1)
| ~ spl0_20
| ~ spl0_80 ),
inference(forward_demodulation,[],[f210,f1262]) ).
fof(f1382,plain,
( ! [X0] :
( big_f(X0,c2)
| c2 = c1
| c2 = X0
| ~ big_f(X0,c1)
| c2 = X0 )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_69 ),
inference(superposition,[],[f1298,f1072]) ).
fof(f1392,plain,
( ! [X0,X1] :
( X0 = X1
| ~ big_f(c1,X1)
| ~ big_f(c1,X0) )
| ~ spl0_30 ),
inference(superposition,[],[f268,f268]) ).
fof(f1396,definition,
( spl0_82
<=> c2 = f2(c1) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f1398,plain,
( c2 = f2(c1)
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f1396]) ).
fof(f1400,plain,
( spl0_53
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f1392,f267,f640]) ).
fof(f1416,plain,
( ! [X0,X1] :
( ~ big_f(X1,c1)
| X0 = X1
| ~ big_f(X0,c4) )
| ~ spl0_11
| ~ spl0_80 ),
inference(forward_demodulation,[],[f1279,f1262]) ).
fof(f1417,plain,
( ! [X0,X1] :
( ~ big_f(X1,c1)
| ~ big_f(X0,c1)
| X0 = X1 )
| ~ spl0_11
| ~ spl0_80 ),
inference(forward_demodulation,[],[f1416,f1262]) ).
fof(f1420,plain,
( ! [X0] :
( ~ big_f(X0,c1)
| c1 = X0 )
| ~ spl0_11
| ~ spl0_34
| ~ spl0_80 ),
inference(resolution,[],[f1417,f320]) ).
fof(f1422,plain,
( ! [X0] :
( ~ big_f(X0,c1)
| c3 = X0 )
| ~ spl0_11
| ~ spl0_26
| ~ spl0_80 ),
inference(resolution,[],[f1417,f238]) ).
fof(f1437,plain,
( ! [X0,X1] :
( c1 != X1
| c1 = X0
| ~ big_f(c1,X0)
| c2 = f3(X0,X1) )
| ~ spl0_12
| ~ spl0_80 ),
inference(forward_demodulation,[],[f1288,f1262]) ).
fof(f1467,plain,
( ! [X0] :
( c2 = f3(X0,c1)
| ~ big_f(c1,X0)
| c1 = X0 )
| ~ spl0_12
| ~ spl0_80 ),
inference(equality_resolution,[],[f1437]) ).
fof(f1479,plain,
( big_f(c2,c1)
| ~ spl0_23
| ~ spl0_33 ),
inference(superposition,[],[f223,f293]) ).
fof(f1491,plain,
( ! [X0,X1] :
( c1 != X1
| c2 = X0
| ~ big_f(c1,X0)
| c2 = f3(X0,X1) )
| ~ spl0_12
| ~ spl0_22 ),
inference(superposition,[],[f1247,f3]) ).
fof(f1493,plain,
( ! [X0] :
( ~ big_f(X0,c2)
| c1 = X0 )
| ~ spl0_21
| ~ spl0_22 ),
inference(forward_demodulation,[],[f214,f219]) ).
fof(f1508,plain,
( ~ big_f(c1,c1)
| spl0_26
| ~ spl0_59 ),
inference(forward_demodulation,[],[f237,f706]) ).
fof(f1536,plain,
( c2 != c2
| ~ spl0_17
| spl0_18 ),
inference(superposition,[],[f201,f197]) ).
fof(f1617,plain,
( $false
| ~ spl0_17
| spl0_18 ),
inference(trivial_inequality_removal,[],[f1536]) ).
fof(f1618,plain,
( ~ spl0_17
| spl0_18 ),
inference(avatar_contradiction_clause,[],[f1617]) ).
fof(f1670,plain,
( ! [X0] :
( big_f(c3,X0)
| c2 = X0 )
| ~ spl0_26 ),
inference(superposition,[],[f238,f3]) ).
fof(f1676,plain,
( ! [X0] :
( big_f(c1,X0)
| c2 = X0
| c2 = c3 )
| ~ spl0_26 ),
inference(superposition,[],[f1670,f3]) ).
fof(f1678,definition,
( spl0_84
<=> ! [X0] :
( big_f(c1,X0)
| c2 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f1679,plain,
( ! [X0] :
( big_f(c1,X0)
| c2 = X0 )
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f1678]) ).
fof(f1680,plain,
( spl0_27
| spl0_84
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1676,f236,f1678,f241]) ).
fof(f1694,plain,
( c1 != c1
| c2 = c3
| spl0_59 ),
inference(superposition,[],[f705,f3]) ).
fof(f1695,plain,
( c2 = c3
| spl0_59 ),
inference(trivial_inequality_removal,[],[f1694]) ).
fof(f1696,plain,
( spl0_27
| spl0_59 ),
inference(avatar_split_clause,[],[f1695,f704,f241]) ).
fof(f1716,plain,
( ~ big_f(c2,c1)
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f237,f243]) ).
fof(f1734,plain,
( ! [X0] :
( c2 = f3(X0,c1)
| ~ big_f(c1,X0)
| c2 = X0 )
| ~ spl0_12
| ~ spl0_22 ),
inference(equality_resolution,[],[f1491]) ).
fof(f1739,plain,
( ! [X0] :
( big_f(c2,X0)
| c4 = X0
| c2 = c1
| ~ big_f(c1,X0)
| c2 = X0 )
| ~ spl0_12
| ~ spl0_13
| ~ spl0_22 ),
inference(superposition,[],[f155,f1734]) ).
fof(f1741,plain,
( ! [X0] :
( big_f(c2,X0)
| c4 = X0
| ~ big_f(c1,X0)
| c2 = X0 )
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1739,f201]) ).
fof(f1754,plain,
( spl0_35
| ~ spl0_11
| ~ spl0_34
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f1420,f1260,f318,f146,f346]) ).
fof(f1796,plain,
( ! [X0] :
( big_f(c2,X0)
| c4 = X0
| c2 = c1
| ~ big_f(c1,X0)
| c1 = X0 )
| ~ spl0_12
| ~ spl0_13
| ~ spl0_80 ),
inference(superposition,[],[f155,f1467]) ).
fof(f1797,plain,
( ! [X0] :
( big_f(c2,X0)
| c4 = X0
| ~ big_f(c1,X0)
| c1 = X0 )
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f1796,f201]) ).
fof(f1807,plain,
( spl0_41
| spl0_69 ),
inference(avatar_split_clause,[],[f1009,f930,f439]) ).
fof(f1811,plain,
( ! [X0,X1] :
( f10(X0) != X0
| c1 != X1
| ~ big_f(c1,f10(X0))
| c2 = f9(X0,X1) )
| ~ spl0_1 ),
inference(superposition,[],[f98,f3]) ).
fof(f1812,plain,
( ! [X0] :
( c2 = f10(X0)
| c2 = X0 )
| ~ spl0_75 ),
inference(superposition,[],[f1102,f3]) ).
fof(f1825,plain,
( big_f(c1,c2)
| c2 = f8(c1)
| ~ spl0_4
| spl0_18
| ~ spl0_75 ),
inference(superposition,[],[f1114,f3]) ).
fof(f1836,plain,
( c2 = c1
| ~ spl0_32
| ~ spl0_51 ),
inference(resolution,[],[f634,f283]) ).
fof(f1846,plain,
( $false
| spl0_18
| ~ spl0_32
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f1836,f201]) ).
fof(f1847,plain,
( spl0_18
| ~ spl0_32
| ~ spl0_51 ),
inference(avatar_contradiction_clause,[],[f1846]) ).
fof(f1852,plain,
( spl0_77
| spl0_32
| ~ spl0_4
| spl0_18
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f1825,f1100,f199,f108,f281,f1119]) ).
fof(f1857,plain,
( big_f(c2,f5(c1))
| ~ spl0_7
| spl0_18
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f453,f201]) ).
fof(f1867,plain,
( ~ spl0_55
| spl0_26
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f1716,f241,f236,f675]) ).
fof(f1872,definition,
( spl0_86
<=> ! [X0,X1] :
( c1 != X1
| c1 = X0
| c2 = f6(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f1873,plain,
( ! [X0,X1] :
( c1 != X1
| c1 = X0
| c2 = f6(X0,X1) )
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f1872]) ).
fof(f1883,plain,
( ! [X0] :
( big_f(f7(X0),c2)
| f7(X0) = X0
| c2 = X0 )
| ~ spl0_7
| ~ spl0_57 ),
inference(superposition,[],[f124,f685]) ).
fof(f1908,plain,
( ! [X0] :
( ~ big_f(X0,c2)
| c2 = X0 )
| spl0_32 ),
inference(superposition,[],[f282,f3]) ).
fof(f1910,plain,
( c2 = f9(c1,c1)
| c2 = f10(c1)
| ~ spl0_1
| ~ spl0_34 ),
inference(equality_resolution,[],[f1096]) ).
fof(f1957,plain,
( ! [X0] :
( ~ big_f(c2,X0)
| c2 = X0 )
| spl0_55 ),
inference(superposition,[],[f676,f3]) ).
fof(f1982,plain,
( big_f(c2,c2)
| c2 = c1
| c2 = c1
| ~ spl0_7
| ~ spl0_41
| ~ spl0_57 ),
inference(superposition,[],[f1883,f441]) ).
fof(f1984,plain,
( big_f(c2,c2)
| c2 = c1
| ~ spl0_7
| ~ spl0_41
| ~ spl0_57 ),
inference(duplicate_literal_removal,[],[f1982]) ).
fof(f1991,plain,
( ! [X0,X1] :
( ~ big_f(X0,c2)
| c2 = X1
| f8(X1) = X0
| c2 = X1 )
| ~ spl0_5
| ~ spl0_75 ),
inference(superposition,[],[f113,f1812]) ).
fof(f1992,plain,
( ! [X0,X1] :
( f8(X1) = X0
| c2 = X1
| ~ big_f(X0,c2) )
| ~ spl0_5
| ~ spl0_75 ),
inference(duplicate_literal_removal,[],[f1991]) ).
fof(f2002,plain,
( ! [X2,X0,X1] :
( X0 = X2
| c2 = X1
| ~ big_f(X2,c2)
| c2 = X1
| ~ big_f(X0,c2) )
| ~ spl0_5
| ~ spl0_75 ),
inference(superposition,[],[f1992,f1992]) ).
fof(f2008,plain,
( ! [X2,X0,X1] :
( X0 = X2
| c2 = X1
| ~ big_f(X2,c2)
| ~ big_f(X0,c2) )
| ~ spl0_5
| ~ spl0_75 ),
inference(duplicate_literal_removal,[],[f2002]) ).
fof(f2013,definition,
( spl0_89
<=> ! [X1] :
( c1 = X1
| ~ big_f(X1,c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f2014,plain,
( ! [X1] :
( ~ big_f(X1,c2)
| c1 = X1 )
| ~ spl0_89 ),
inference(avatar_component_clause,[],[f2013]) ).
fof(f2017,definition,
( spl0_90
<=> ! [X2,X0] :
( X0 = X2
| ~ big_f(X0,c2)
| ~ big_f(X2,c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f2018,plain,
( ! [X2,X0] :
( ~ big_f(X2,c2)
| ~ big_f(X0,c2)
| X0 = X2 )
| ~ spl0_90 ),
inference(avatar_component_clause,[],[f2017]) ).
fof(f2020,plain,
( ! [X0] :
( c2 = X0
| c2 = f5(X0) )
| ~ spl0_7
| ~ spl0_41
| spl0_55 ),
inference(resolution,[],[f487,f1957]) ).
fof(f2032,plain,
( ! [X2,X0,X1] :
( X0 = X2
| c2 = X1
| ~ big_f(c2,X2)
| c2 = X1
| ~ big_f(c2,X0) )
| ~ spl0_8
| ~ spl0_41 ),
inference(superposition,[],[f488,f488]) ).
fof(f2045,plain,
( ! [X2,X0,X1] :
( X0 = X2
| c2 = X1
| ~ big_f(c2,X2)
| ~ big_f(c2,X0) )
| ~ spl0_8
| ~ spl0_41 ),
inference(duplicate_literal_removal,[],[f2032]) ).
fof(f2046,plain,
( ! [X0,X1] :
( c1 = X0
| big_f(c1,X0)
| c1 = X1
| c2 = f3(X0,X1) )
| ~ spl0_13
| ~ spl0_80 ),
inference(forward_demodulation,[],[f183,f1262]) ).
fof(f2047,plain,
( ! [X0,X1] :
( c2 = f3(X0,X1)
| c1 = X1
| c1 = X0 )
| ~ spl0_13
| ~ spl0_51
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f2046,f634]) ).
fof(f2049,plain,
( ! [X0,X1] :
( c2 != X1
| c4 = X0
| ~ big_f(c2,X0)
| c1 = X1
| c1 = X0 )
| ~ spl0_12
| ~ spl0_13
| ~ spl0_51
| ~ spl0_80 ),
inference(superposition,[],[f151,f2047]) ).
fof(f2051,plain,
( ! [X0,X1] :
( c4 = X0
| ~ big_f(c2,X0)
| c1 = X1
| c1 = X0 )
| ~ spl0_12
| ~ spl0_13
| ~ spl0_51
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f2049,f3]) ).
fof(f2052,plain,
( ! [X0,X1] :
( c1 = X0
| ~ big_f(c2,X0)
| c1 = X1
| c1 = X0 )
| ~ spl0_12
| ~ spl0_13
| ~ spl0_51
| ~ spl0_80 ),
inference(forward_demodulation,[],[f2051,f1262]) ).
fof(f2053,plain,
( ! [X0,X1] :
( c1 = X0
| ~ big_f(c2,X0)
| c1 = X1 )
| ~ spl0_12
| ~ spl0_13
| ~ spl0_51
| ~ spl0_80 ),
inference(duplicate_literal_removal,[],[f2052]) ).
fof(f2058,plain,
( ! [X0] : c2 != X0
| spl0_18
| ~ spl0_48 ),
inference(superposition,[],[f201,f597]) ).
fof(f2182,plain,
( spl0_55
| ~ spl0_26
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f410,f241,f236,f675]) ).
fof(f2184,plain,
( spl0_55
| ~ spl0_23
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f1479,f291,f221,f675]) ).
fof(f2192,definition,
( spl0_91
<=> ! [X0] :
( c2 = X0
| ~ big_f(c2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f2193,plain,
( ! [X0] :
( ~ big_f(c2,X0)
| c2 = X0 )
| ~ spl0_91 ),
inference(avatar_component_clause,[],[f2192]) ).
fof(f2203,plain,
( spl0_43
| ~ spl0_7
| spl0_18
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f1857,f439,f199,f123,f455]) ).
fof(f2204,plain,
( big_f(c2,c2)
| ~ spl0_7
| spl0_18
| ~ spl0_41
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f1984,f201]) ).
fof(f2206,definition,
( spl0_92
<=> big_f(c2,c2) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f2207,plain,
( ~ big_f(c2,c2)
| spl0_92 ),
inference(avatar_component_clause,[],[f2206]) ).
fof(f2208,plain,
( big_f(c2,c2)
| ~ spl0_92 ),
inference(avatar_component_clause,[],[f2206]) ).
fof(f2211,plain,
( spl0_92
| ~ spl0_7
| spl0_18
| ~ spl0_41
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f2204,f684,f439,f199,f123,f2206]) ).
fof(f2237,definition,
( spl0_93
<=> ! [X0] :
( ~ big_f(X0,c1)
| c2 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f2238,plain,
( ! [X0] :
( ~ big_f(X0,c1)
| c2 = X0 )
| ~ spl0_93 ),
inference(avatar_component_clause,[],[f2237]) ).
fof(f2252,plain,
( spl0_92
| ~ spl0_4
| spl0_18
| ~ spl0_75
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f1125,f1119,f1100,f199,f108,f2206]) ).
fof(f2263,definition,
( spl0_94
<=> ! [X0] :
( c2 = f3(c2,X0)
| f3(c2,X0) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f2264,plain,
( ! [X0] :
( f3(c2,X0) = X0
| c2 = f3(c2,X0) )
| ~ spl0_94 ),
inference(avatar_component_clause,[],[f2263]) ).
fof(f2266,plain,
( spl0_92
| ~ spl0_9
| ~ spl0_22
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f1239,f277,f217,f137,f2206]) ).
fof(f2267,plain,
( spl0_89
| ~ spl0_21
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1493,f217,f213,f2013]) ).
fof(f2269,plain,
( ! [X0] :
( big_f(c2,X0)
| c4 = X0
| c2 = X0 )
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f1741,f1679]) ).
fof(f2291,plain,
( big_f(c1,c2)
| c2 = f4(c2)
| ~ spl0_9
| ~ spl0_22 ),
inference(superposition,[],[f1238,f3]) ).
fof(f2292,plain,
( c2 = f4(c2)
| ~ spl0_9
| ~ spl0_22
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f2291,f282]) ).
fof(f2293,plain,
( spl0_31
| ~ spl0_9
| ~ spl0_22
| spl0_32 ),
inference(avatar_split_clause,[],[f2292,f281,f217,f137,f277]) ).
fof(f2294,plain,
( ! [X0] :
( ~ big_f(c2,X0)
| c2 = X0 )
| ~ spl0_47
| ~ spl0_92 ),
inference(resolution,[],[f2208,f504]) ).
fof(f2295,plain,
( spl0_91
| ~ spl0_47
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f2294,f2206,f503,f2192]) ).
fof(f2305,plain,
( ! [X0,X1] :
( f8(X1) = X0
| c1 = X1
| ~ big_f(X0,c1)
| c2 = f10(X1) )
| ~ spl0_5 ),
inference(superposition,[],[f113,f3]) ).
fof(f2316,plain,
( c2 = c1
| ~ spl0_89
| ~ spl0_92 ),
inference(resolution,[],[f2014,f2208]) ).
fof(f2326,plain,
( $false
| spl0_18
| ~ spl0_89
| ~ spl0_92 ),
inference(forward_subsumption_resolution,[],[f2316,f201]) ).
fof(f2327,plain,
( spl0_18
| ~ spl0_89
| ~ spl0_92 ),
inference(avatar_contradiction_clause,[],[f2326]) ).
fof(f2365,plain,
( big_f(c2,c2)
| ~ spl0_9
| ~ spl0_19
| ~ spl0_22 ),
inference(forward_demodulation,[],[f289,f219]) ).
fof(f2367,plain,
( ! [X0] :
( ~ big_f(c2,X0)
| c2 = X0 )
| spl0_55 ),
inference(superposition,[],[f676,f3]) ).
fof(f2368,plain,
( spl0_91
| spl0_55 ),
inference(avatar_split_clause,[],[f2367,f675,f2192]) ).
fof(f2369,plain,
( ! [X0] :
( c2 = X0
| big_f(c2,X0)
| c2 = X0 )
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| ~ spl0_84 ),
inference(forward_demodulation,[],[f2269,f219]) ).
fof(f2370,plain,
( ! [X0] :
( big_f(c2,X0)
| c2 = X0 )
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| ~ spl0_84 ),
inference(duplicate_literal_removal,[],[f2369]) ).
fof(f2373,plain,
( c2 = c1
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| spl0_55
| ~ spl0_84 ),
inference(resolution,[],[f2370,f676]) ).
fof(f2378,plain,
( $false
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| spl0_55
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f2373,f201]) ).
fof(f2379,plain,
( ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| spl0_55
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f2378]) ).
fof(f2381,plain,
( ! [X0] :
( c2 = X0
| big_f(c2,X0)
| ~ big_f(c1,X0)
| c2 = X0 )
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1741,f219]) ).
fof(f2382,plain,
( ! [X0] :
( big_f(c2,X0)
| c2 = X0
| ~ big_f(c1,X0) )
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22 ),
inference(duplicate_literal_removal,[],[f2381]) ).
fof(f2394,plain,
( c2 = c1
| ~ big_f(c1,c1)
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| spl0_55 ),
inference(resolution,[],[f2382,f676]) ).
fof(f2399,plain,
( c2 = c1
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| ~ spl0_34
| spl0_55 ),
inference(forward_subsumption_resolution,[],[f2394,f830]) ).
fof(f2405,plain,
( $false
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| ~ spl0_34
| spl0_55 ),
inference(forward_subsumption_resolution,[],[f2399,f201]) ).
fof(f2406,plain,
( ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| ~ spl0_34
| spl0_55 ),
inference(avatar_contradiction_clause,[],[f2405]) ).
fof(f2410,plain,
( ! [X0] :
( big_f(c2,X0)
| c2 = X0 )
| ~ spl0_55 ),
inference(superposition,[],[f677,f3]) ).
fof(f2418,plain,
( ! [X0] :
( c2 = f6(X0,c1)
| c1 = X0 )
| ~ spl0_86 ),
inference(equality_resolution,[],[f1873]) ).
fof(f2423,plain,
( ! [X0] : c2 = X0
| ~ spl0_55
| ~ spl0_91 ),
inference(forward_subsumption_resolution,[],[f2193,f2410]) ).
fof(f2424,plain,
( spl0_17
| ~ spl0_55
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f2423,f2192,f675,f196]) ).
fof(f2439,plain,
( ! [X0] :
( ~ big_f(X0,c2)
| c2 = X0 )
| ~ spl0_90
| ~ spl0_92 ),
inference(resolution,[],[f2018,f2208]) ).
fof(f2499,plain,
( ! [X0] :
( big_f(c2,c2)
| c2 = c1
| c1 = X0
| c1 = X0 )
| ~ spl0_6
| ~ spl0_52
| ~ spl0_86 ),
inference(superposition,[],[f1311,f2418]) ).
fof(f2503,plain,
( ! [X0,X1] :
( big_f(c2,c1)
| c1 = X1
| c1 = X0
| c2 = f6(X0,X1) )
| ~ spl0_6
| ~ spl0_52 ),
inference(superposition,[],[f1311,f3]) ).
fof(f2506,plain,
( ! [X0] :
( big_f(c2,c2)
| c2 = c1
| c1 = X0 )
| ~ spl0_6
| ~ spl0_52
| ~ spl0_86 ),
inference(duplicate_literal_removal,[],[f2499]) ).
fof(f2519,plain,
( ! [X2,X0,X1] :
( X0 = X2
| c1 = X1
| ~ big_f(X2,c1)
| c2 = f10(X1)
| c1 = X1
| ~ big_f(X0,c1)
| c2 = f10(X1) )
| ~ spl0_5 ),
inference(superposition,[],[f2305,f2305]) ).
fof(f2533,plain,
( ! [X2,X0,X1] :
( X0 = X2
| c1 = X1
| ~ big_f(X2,c1)
| c2 = f10(X1)
| ~ big_f(X0,c1) )
| ~ spl0_5 ),
inference(duplicate_literal_removal,[],[f2519]) ).
fof(f2539,definition,
( spl0_100
<=> ! [X1] :
( c1 = X1
| c2 = f10(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f2540,plain,
( ! [X1] :
( c2 = f10(X1)
| c1 = X1 )
| ~ spl0_100 ),
inference(avatar_component_clause,[],[f2539]) ).
fof(f2542,definition,
( spl0_101
<=> ! [X2,X0] :
( X0 = X2
| ~ big_f(X0,c1)
| ~ big_f(X2,c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f2543,plain,
( ! [X2,X0] :
( ~ big_f(X2,c1)
| ~ big_f(X0,c1)
| X0 = X2 )
| ~ spl0_101 ),
inference(avatar_component_clause,[],[f2542]) ).
fof(f2544,plain,
( spl0_100
| spl0_101
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f2533,f112,f2542,f2539]) ).
fof(f2547,plain,
( ! [X0] :
( ~ big_f(X0,c1)
| c2 = X0 )
| ~ spl0_55
| ~ spl0_101 ),
inference(resolution,[],[f2543,f677]) ).
fof(f2548,plain,
( ! [X0] :
( ~ big_f(X0,c1)
| c2 = X0
| c2 = c1 )
| ~ spl0_55
| ~ spl0_101 ),
inference(resolution,[],[f2543,f2410]) ).
fof(f2550,plain,
( ! [X0] :
( ~ big_f(X0,c1)
| c1 = X0 )
| ~ spl0_34
| ~ spl0_101 ),
inference(resolution,[],[f2543,f320]) ).
fof(f2561,plain,
( spl0_35
| ~ spl0_34
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f2550,f2542,f318,f346]) ).
fof(f2563,plain,
( ! [X0] :
( ~ big_f(X0,c1)
| c2 = X0 )
| spl0_18
| ~ spl0_55
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f2548,f201]) ).
fof(f2564,plain,
( spl0_93
| ~ spl0_55
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f2547,f2542,f675,f2237]) ).
fof(f2569,plain,
( spl0_93
| spl0_18
| ~ spl0_55
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f2563,f2542,f675,f199,f2237]) ).
fof(f2615,plain,
( big_f(c2,c1)
| ~ spl0_3
| spl0_18
| spl0_75
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f1194,f201]) ).
fof(f2619,plain,
( spl0_48
| spl0_56
| ~ spl0_12
| ~ spl0_13
| ~ spl0_51
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f2053,f1260,f633,f154,f150,f680,f596]) ).
fof(f2622,plain,
( spl0_75
| spl0_76
| ~ spl0_1
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f1910,f318,f97,f1104,f1100]) ).
fof(f2624,definition,
( spl0_103
<=> c1 = f10(c1) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f2625,plain,
( c1 != f10(c1)
| spl0_103 ),
inference(avatar_component_clause,[],[f2624]) ).
fof(f2626,plain,
( c1 = f10(c1)
| ~ spl0_103 ),
inference(avatar_component_clause,[],[f2624]) ).
fof(f2628,definition,
( spl0_104
<=> big_f(c2,f10(c1)) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f2629,plain,
( ~ big_f(c2,f10(c1))
| spl0_104 ),
inference(avatar_component_clause,[],[f2628]) ).
fof(f2640,plain,
( spl0_55
| ~ spl0_3
| spl0_18
| spl0_75
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f2615,f1104,f1100,f199,f104,f675]) ).
fof(f2653,definition,
( spl0_107
<=> ! [X0] :
( c1 != X0
| ~ big_f(c2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f2654,plain,
( ! [X0] :
( c1 != X0
| ~ big_f(c2,X0) )
| ~ spl0_107 ),
inference(avatar_component_clause,[],[f2653]) ).
fof(f2655,plain,
( ~ spl0_55
| spl0_27
| spl0_107
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_56
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f862,f704,f680,f199,f172,f165,f2653,f241,f675]) ).
fof(f2667,plain,
( big_f(c3,c1)
| c2 = f2(c3)
| ~ spl0_10 ),
inference(superposition,[],[f143,f3]) ).
fof(f2668,plain,
( spl0_25
| spl0_26
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f2667,f141,f236,f232]) ).
fof(f2694,plain,
( ! [X0] :
( big_f(c2,X0)
| c2 = X0 )
| ~ spl0_55 ),
inference(superposition,[],[f677,f3]) ).
fof(f2699,plain,
( ~ big_f(c2,c1)
| ~ spl0_107 ),
inference(equality_resolution,[],[f2654]) ).
fof(f2700,plain,
( $false
| ~ spl0_55
| ~ spl0_107 ),
inference(forward_subsumption_resolution,[],[f2699,f677]) ).
fof(f2701,plain,
( ~ spl0_55
| ~ spl0_107 ),
inference(avatar_contradiction_clause,[],[f2700]) ).
fof(f2708,plain,
( ! [X0] :
( f10(X0) = X0
| c2 = X0 )
| ~ spl0_103 ),
inference(superposition,[],[f2626,f3]) ).
fof(f2736,plain,
( big_f(c2,c4)
| ~ spl0_9
| ~ spl0_19 ),
inference(superposition,[],[f139,f206]) ).
fof(f2739,definition,
( spl0_108
<=> big_f(c2,c4) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f2740,plain,
( ~ big_f(c2,c4)
| spl0_108 ),
inference(avatar_component_clause,[],[f2739]) ).
fof(f2741,plain,
( big_f(c2,c4)
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f2739]) ).
fof(f2743,plain,
( spl0_108
| ~ spl0_9
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f2736,f204,f137,f2739]) ).
fof(f2744,plain,
( big_f(c2,c1)
| c2 = c4
| ~ spl0_108 ),
inference(superposition,[],[f2741,f3]) ).
fof(f2745,plain,
( ! [X0,X1] :
( big_f(X0,f1(X0,X1))
| c1 = X0
| f1(X0,X1) = X1 )
| ~ spl0_16
| ~ spl0_59 ),
inference(forward_demodulation,[],[f173,f706]) ).
fof(f2747,plain,
( c2 = f2(c1)
| ~ spl0_25
| ~ spl0_59 ),
inference(forward_demodulation,[],[f234,f706]) ).
fof(f2748,plain,
( spl0_82
| ~ spl0_25
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f2747,f704,f232,f1396]) ).
fof(f2762,plain,
( ~ big_f(c1,c2)
| ~ spl0_69
| spl0_73 ),
inference(forward_demodulation,[],[f1000,f932]) ).
fof(f2764,plain,
( c2 = c1
| ~ spl0_21
| ~ spl0_108 ),
inference(resolution,[],[f214,f2741]) ).
fof(f2775,plain,
( $false
| spl0_18
| ~ spl0_21
| ~ spl0_108 ),
inference(forward_subsumption_resolution,[],[f2764,f201]) ).
fof(f2776,plain,
( spl0_18
| ~ spl0_21
| ~ spl0_108 ),
inference(avatar_contradiction_clause,[],[f2775]) ).
fof(f2799,plain,
( c1 != c1
| c2 = c4
| spl0_80 ),
inference(superposition,[],[f1261,f3]) ).
fof(f2800,plain,
( c2 = c4
| spl0_80 ),
inference(trivial_inequality_removal,[],[f2799]) ).
fof(f2801,plain,
( spl0_22
| spl0_80 ),
inference(avatar_split_clause,[],[f2800,f1260,f217]) ).
fof(f2802,plain,
( big_f(c2,c1)
| ~ spl0_80
| ~ spl0_108 ),
inference(superposition,[],[f2741,f1262]) ).
fof(f2803,plain,
( c2 = f4(c1)
| ~ spl0_19
| ~ spl0_80 ),
inference(superposition,[],[f206,f1262]) ).
fof(f2809,plain,
( ! [X0,X1] :
( c2 = f1(X0,X1)
| c1 = X0
| c1 = X1
| big_f(X0,c1) )
| ~ spl0_16
| ~ spl0_59 ),
inference(superposition,[],[f2745,f3]) ).
fof(f2810,plain,
( ! [X0] :
( c2 = X0
| ~ big_f(X0,c1) )
| ~ spl0_24
| ~ spl0_33 ),
inference(forward_demodulation,[],[f227,f293]) ).
fof(f2811,plain,
( spl0_93
| ~ spl0_24
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f2810,f291,f226,f2237]) ).
fof(f2813,plain,
( c2 = c1
| c2 = c1
| ~ spl0_34
| ~ spl0_93 ),
inference(resolution,[],[f2238,f830]) ).
fof(f2818,plain,
( c2 = c3
| ~ spl0_26
| ~ spl0_93 ),
inference(resolution,[],[f2238,f238]) ).
fof(f2819,plain,
( ! [X0] :
( c2 = f3(c1,X0)
| c1 = c4
| f3(c1,X0) = X0 )
| ~ spl0_13
| ~ spl0_93 ),
inference(resolution,[],[f2238,f155]) ).
fof(f2820,plain,
( c2 = f4(c1)
| ~ spl0_23
| ~ spl0_93 ),
inference(resolution,[],[f2238,f223]) ).
fof(f2828,plain,
( c2 = c1
| ~ spl0_34
| ~ spl0_93 ),
inference(duplicate_literal_removal,[],[f2813]) ).
fof(f2830,plain,
( spl0_27
| ~ spl0_26
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f2818,f2237,f236,f241]) ).
fof(f2835,plain,
( $false
| spl0_18
| ~ spl0_34
| ~ spl0_93 ),
inference(forward_subsumption_resolution,[],[f2828,f201]) ).
fof(f2836,plain,
( spl0_18
| ~ spl0_34
| ~ spl0_93 ),
inference(avatar_contradiction_clause,[],[f2835]) ).
fof(f2839,plain,
( ! [X0,X1] :
( X0 != X0
| big_f(f9(X0,X1),X0)
| f9(X0,X1) = X1
| c2 = X0 )
| ~ spl0_3
| ~ spl0_103 ),
inference(superposition,[],[f105,f2708]) ).
fof(f2840,plain,
( ! [X0,X1] :
( X0 != X0
| c1 != X1
| ~ big_f(c1,X0)
| c2 = f9(X0,X1)
| c2 = X0 )
| ~ spl0_1
| ~ spl0_103 ),
inference(superposition,[],[f1811,f2708]) ).
fof(f2845,plain,
( ! [X0,X1] :
( c1 != X1
| ~ big_f(c1,X0)
| c2 = f9(X0,X1)
| c2 = X0 )
| ~ spl0_1
| ~ spl0_103 ),
inference(trivial_inequality_removal,[],[f2840]) ).
fof(f2846,plain,
( ! [X0,X1] :
( big_f(f9(X0,X1),X0)
| f9(X0,X1) = X1
| c2 = X0 )
| ~ spl0_3
| ~ spl0_103 ),
inference(trivial_inequality_removal,[],[f2839]) ).
fof(f2848,plain,
( ! [X0,X1] :
( c1 != X1
| c2 = f9(X0,X1)
| c2 = X0 )
| ~ spl0_1
| ~ spl0_84
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f2845,f1679]) ).
fof(f2850,plain,
( ! [X0] :
( c2 = f9(X0,c1)
| c2 = X0 )
| ~ spl0_1
| ~ spl0_84
| ~ spl0_103 ),
inference(equality_resolution,[],[f2848]) ).
fof(f2862,plain,
( ! [X0] :
( big_f(c2,X0)
| c2 = c1
| c2 = X0
| c2 = X0 )
| ~ spl0_1
| ~ spl0_3
| ~ spl0_84
| ~ spl0_103 ),
inference(superposition,[],[f2846,f2850]) ).
fof(f2866,plain,
( ! [X0] :
( big_f(c2,X0)
| c2 = c1
| c2 = X0 )
| ~ spl0_1
| ~ spl0_3
| ~ spl0_84
| ~ spl0_103 ),
inference(duplicate_literal_removal,[],[f2862]) ).
fof(f2913,plain,
( ! [X0,X1] :
( c1 != X1
| c1 = X0
| ~ big_f(X0,c1)
| c2 = f1(X0,X1) )
| ~ spl0_15
| ~ spl0_59 ),
inference(forward_demodulation,[],[f270,f706]) ).
fof(f2917,plain,
( ! [X0,X1] :
( c2 != X1
| c3 = X0
| ~ big_f(X0,c2)
| c1 = X0
| c1 = X1
| big_f(X0,c1) )
| ~ spl0_15
| ~ spl0_16
| ~ spl0_59 ),
inference(superposition,[],[f166,f2809]) ).
fof(f2919,plain,
( ! [X0,X1] :
( c3 = X0
| ~ big_f(X0,c2)
| c1 = X0
| c1 = X1
| big_f(X0,c1) )
| ~ spl0_15
| ~ spl0_16
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f2917,f3]) ).
fof(f2920,plain,
( ! [X0,X1] :
( c1 = X0
| ~ big_f(X0,c2)
| c1 = X0
| c1 = X1
| big_f(X0,c1) )
| ~ spl0_15
| ~ spl0_16
| ~ spl0_59 ),
inference(forward_demodulation,[],[f2919,f706]) ).
fof(f2921,plain,
( ! [X0,X1] :
( c1 = X0
| ~ big_f(X0,c2)
| c1 = X1
| big_f(X0,c1) )
| ~ spl0_15
| ~ spl0_16
| ~ spl0_59 ),
inference(duplicate_literal_removal,[],[f2920]) ).
fof(f2923,definition,
( spl0_109
<=> ! [X0] :
( c1 = X0
| big_f(X0,c1)
| ~ big_f(X0,c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f2924,plain,
( ! [X0] :
( big_f(X0,c1)
| c1 = X0
| ~ big_f(X0,c2) )
| ~ spl0_109 ),
inference(avatar_component_clause,[],[f2923]) ).
fof(f2941,plain,
( ! [X0] :
( c2 = f3(c2,X0)
| c2 = c4
| f3(c2,X0) = X0 )
| ~ spl0_13
| spl0_32 ),
inference(resolution,[],[f1908,f155]) ).
fof(f2950,definition,
( spl0_110
<=> c2 = f10(c2) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f2951,plain,
( c2 != f10(c2)
| spl0_110 ),
inference(avatar_component_clause,[],[f2950]) ).
fof(f2952,plain,
( c2 = f10(c2)
| ~ spl0_110 ),
inference(avatar_component_clause,[],[f2950]) ).
fof(f2954,definition,
( spl0_111
<=> c1 = f8(c2) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f2955,plain,
( c1 != f8(c2)
| spl0_111 ),
inference(avatar_component_clause,[],[f2954]) ).
fof(f2956,plain,
( c1 = f8(c2)
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f2954]) ).
fof(f2961,plain,
( ! [X0] :
( c2 = c1
| c2 = f3(c2,X0)
| f3(c2,X0) = X0 )
| ~ spl0_13
| spl0_32
| ~ spl0_80 ),
inference(forward_demodulation,[],[f2941,f1262]) ).
fof(f2962,plain,
( ! [X0] :
( c2 = f3(c2,X0)
| f3(c2,X0) = X0 )
| ~ spl0_13
| spl0_18
| spl0_32
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f2961,f201]) ).
fof(f2963,plain,
( spl0_94
| ~ spl0_13
| spl0_18
| spl0_32
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f2962,f1260,f281,f199,f154,f2263]) ).
fof(f2977,plain,
( c2 != c2
| c2 = c1
| ~ spl0_100
| spl0_110 ),
inference(superposition,[],[f2951,f2540]) ).
fof(f2979,plain,
( c2 = c1
| ~ spl0_100
| spl0_110 ),
inference(trivial_inequality_removal,[],[f2977]) ).
fof(f2981,plain,
( $false
| spl0_18
| ~ spl0_100
| spl0_110 ),
inference(forward_subsumption_resolution,[],[f2979,f201]) ).
fof(f2982,plain,
( spl0_18
| ~ spl0_100
| spl0_110 ),
inference(avatar_contradiction_clause,[],[f2981]) ).
fof(f2986,plain,
( ! [X0] :
( c2 != c2
| big_f(f9(c2,X0),c2)
| f9(c2,X0) = X0 )
| ~ spl0_3
| ~ spl0_110 ),
inference(superposition,[],[f105,f2952]) ).
fof(f2991,plain,
( ! [X0] :
( big_f(f9(c2,X0),c2)
| f9(c2,X0) = X0 )
| ~ spl0_3
| ~ spl0_110 ),
inference(trivial_inequality_removal,[],[f2986]) ).
fof(f2994,plain,
( ! [X0] :
( big_f(c1,c2)
| c1 = X0
| c2 = f9(c2,X0) )
| ~ spl0_3
| ~ spl0_110 ),
inference(superposition,[],[f2991,f3]) ).
fof(f2995,plain,
( ! [X0] :
( c2 = f9(c2,X0)
| c1 = X0 )
| ~ spl0_3
| spl0_32
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f2994,f282]) ).
fof(f3021,plain,
( ! [X0] :
( c2 != X0
| c2 != f10(c2)
| ~ big_f(c2,f10(c2))
| c1 = X0 )
| ~ spl0_1
| ~ spl0_3
| spl0_32
| ~ spl0_110 ),
inference(superposition,[],[f98,f2995]) ).
fof(f3022,plain,
( ! [X0] :
( c2 != f10(c2)
| ~ big_f(c2,f10(c2))
| c1 = X0 )
| ~ spl0_1
| ~ spl0_3
| spl0_32
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f3021,f3]) ).
fof(f3023,plain,
( ! [X0] :
( ~ big_f(c2,f10(c2))
| c1 = X0 )
| ~ spl0_1
| ~ spl0_3
| spl0_32
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f3022,f2952]) ).
fof(f3024,plain,
( ! [X0] :
( ~ big_f(c2,c2)
| c1 = X0 )
| ~ spl0_1
| ~ spl0_3
| spl0_32
| ~ spl0_110 ),
inference(forward_demodulation,[],[f3023,f2952]) ).
fof(f3040,plain,
( ! [X0] :
( c2 = f1(X0,c1)
| ~ big_f(X0,c1)
| c1 = X0 )
| ~ spl0_15
| ~ spl0_59 ),
inference(equality_resolution,[],[f2913]) ).
fof(f3043,plain,
( ! [X0] :
( big_f(X0,c2)
| c1 = X0
| c2 = c1
| ~ big_f(X0,c1)
| c1 = X0 )
| ~ spl0_15
| ~ spl0_16
| ~ spl0_59 ),
inference(superposition,[],[f2745,f3040]) ).
fof(f3045,plain,
( ! [X0] :
( big_f(X0,c2)
| c1 = X0
| c2 = c1
| ~ big_f(X0,c1) )
| ~ spl0_15
| ~ spl0_16
| ~ spl0_59 ),
inference(duplicate_literal_removal,[],[f3043]) ).
fof(f3046,plain,
( ! [X0] :
( big_f(X0,c2)
| c1 = X0
| ~ big_f(X0,c1) )
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f3045,f201]) ).
fof(f3048,plain,
( c2 = c1
| ~ big_f(c2,c1)
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_59
| spl0_92 ),
inference(resolution,[],[f3046,f2207]) ).
fof(f3052,plain,
( c2 = c1
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_55
| ~ spl0_59
| spl0_92 ),
inference(forward_subsumption_resolution,[],[f3048,f2694]) ).
fof(f3053,plain,
( $false
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_55
| ~ spl0_59
| spl0_92 ),
inference(forward_subsumption_resolution,[],[f3052,f201]) ).
fof(f3054,plain,
( ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_55
| ~ spl0_59
| spl0_92 ),
inference(avatar_contradiction_clause,[],[f3053]) ).
fof(f3090,definition,
( spl0_114
<=> ! [X0] : ~ big_f(X0,c2) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f3091,plain,
( ! [X0] : ~ big_f(X0,c2)
| ~ spl0_114 ),
inference(avatar_component_clause,[],[f3090]) ).
fof(f3096,plain,
( c2 = c1
| big_f(c2,c1)
| ~ spl0_80
| ~ spl0_108 ),
inference(forward_demodulation,[],[f2744,f1262]) ).
fof(f3097,plain,
( spl0_55
| ~ spl0_80
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f2802,f2739,f1260,f675]) ).
fof(f3111,plain,
( big_f(c2,c1)
| spl0_18
| ~ spl0_80
| ~ spl0_108 ),
inference(forward_subsumption_resolution,[],[f3096,f201]) ).
fof(f3114,plain,
( spl0_55
| spl0_18
| ~ spl0_80
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f3111,f2739,f1260,f199,f675]) ).
fof(f3120,plain,
( ~ big_f(c2,c1)
| ~ spl0_80
| spl0_108 ),
inference(forward_demodulation,[],[f2740,f1262]) ).
fof(f3126,plain,
( ~ spl0_55
| ~ spl0_80
| spl0_108 ),
inference(avatar_split_clause,[],[f3120,f2739,f1260,f675]) ).
fof(f3132,definition,
( spl0_115
<=> big_f(c2,f10(c2)) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f3133,plain,
( big_f(c2,f10(c2))
| ~ spl0_115 ),
inference(avatar_component_clause,[],[f3132]) ).
fof(f3158,plain,
( big_f(c1,f10(c2))
| c2 = f10(c2)
| ~ spl0_4
| ~ spl0_111 ),
inference(superposition,[],[f109,f2956]) ).
fof(f3279,definition,
( spl0_117
<=> ! [X0] :
( f7(X0) != X0
| c1 = X0
| ~ big_f(f7(X0),c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f3280,plain,
( ! [X0] :
( f7(X0) != X0
| c1 = X0
| ~ big_f(f7(X0),c2) )
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f3279]) ).
fof(f3282,definition,
( spl0_118
<=> ! [X1] : c2 != X1 ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f3283,plain,
( ! [X1] : c2 != X1
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f3282]) ).
fof(f3297,plain,
( $false
| ~ spl0_118 ),
inference(equality_resolution,[],[f3283]) ).
fof(f3298,plain,
~ spl0_118,
inference(avatar_contradiction_clause,[],[f3297]) ).
fof(f3327,plain,
( c2 = c1
| ~ big_f(c2,c2)
| spl0_55
| ~ spl0_109 ),
inference(resolution,[],[f676,f2924]) ).
fof(f3331,plain,
( ~ big_f(c2,c2)
| spl0_18
| spl0_55
| ~ spl0_109 ),
inference(forward_subsumption_resolution,[],[f3327,f201]) ).
fof(f3332,plain,
( $false
| spl0_18
| spl0_55
| ~ spl0_92
| ~ spl0_109 ),
inference(forward_subsumption_resolution,[],[f3331,f2208]) ).
fof(f3333,plain,
( spl0_18
| spl0_55
| ~ spl0_92
| ~ spl0_109 ),
inference(avatar_contradiction_clause,[],[f3332]) ).
fof(f3392,definition,
( spl0_119
<=> ! [X1] :
( c2 = X1
| ~ big_f(X1,c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f3393,plain,
( ! [X1] :
( ~ big_f(X1,c2)
| c2 = X1 )
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f3392]) ).
fof(f3413,plain,
( spl0_119
| ~ spl0_11
| ~ spl0_19
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1252,f217,f204,f146,f3392]) ).
fof(f3435,plain,
( ! [X2,X3] :
( big_f(f3(X2,X3),X2)
| c2 = X2
| f3(X2,X3) = X3 )
| ~ spl0_13
| ~ spl0_22 ),
inference(forward_demodulation,[],[f155,f219]) ).
fof(f3446,definition,
( spl0_122
<=> ! [X0] :
( c1 != X0
| c2 = f9(c2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f3447,plain,
( ! [X0] :
( c1 != X0
| c2 = f9(c2,X0) )
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f3446]) ).
fof(f3455,plain,
( spl0_119
| ~ spl0_90
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f2439,f2206,f2017,f3392]) ).
fof(f3475,plain,
( big_f(c1,f10(c2))
| c2 = f10(c2)
| ~ spl0_4
| ~ spl0_111 ),
inference(superposition,[],[f109,f2956]) ).
fof(f3483,plain,
( ! [X0] :
( big_f(c2,X0)
| c2 = X0 )
| ~ spl0_55 ),
inference(superposition,[],[f677,f3]) ).
fof(f3499,plain,
( ! [X0] :
( c2 != c2
| c1 != X0
| ~ big_f(c1,c2)
| c2 = f9(c2,X0) )
| ~ spl0_1
| ~ spl0_110 ),
inference(superposition,[],[f1811,f2952]) ).
fof(f3500,plain,
( ! [X0] :
( c1 != X0
| ~ big_f(c1,c2)
| c2 = f9(c2,X0) )
| ~ spl0_1
| ~ spl0_110 ),
inference(trivial_inequality_removal,[],[f3499]) ).
fof(f3502,plain,
( ! [X0] :
( c1 != X0
| c2 = f9(c2,X0) )
| ~ spl0_1
| ~ spl0_32
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f3500,f283]) ).
fof(f3503,plain,
( spl0_122
| ~ spl0_1
| ~ spl0_32
| ~ spl0_110 ),
inference(avatar_split_clause,[],[f3502,f2950,f281,f97,f3446]) ).
fof(f3505,plain,
( c2 = f9(c2,c1)
| ~ spl0_122 ),
inference(equality_resolution,[],[f3447]) ).
fof(f3527,plain,
( c2 = c1
| ~ spl0_32
| ~ spl0_119 ),
inference(resolution,[],[f3393,f283]) ).
fof(f3533,plain,
( $false
| spl0_18
| ~ spl0_32
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f3527,f201]) ).
fof(f3534,plain,
( spl0_18
| ~ spl0_32
| ~ spl0_119 ),
inference(avatar_contradiction_clause,[],[f3533]) ).
fof(f3542,plain,
( spl0_92
| ~ spl0_10
| ~ spl0_25
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f406,f241,f232,f141,f2206]) ).
fof(f3550,plain,
( spl0_103
| ~ spl0_4
| ~ spl0_56
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f1127,f1119,f680,f108,f2624]) ).
fof(f3570,plain,
( ! [X0] :
( big_f(c2,X0)
| c2 = X0 )
| ~ spl0_1
| ~ spl0_3
| spl0_18
| ~ spl0_84
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f2866,f201]) ).
fof(f3636,plain,
( big_f(c2,c2)
| c2 = c1
| ~ spl0_3
| ~ spl0_110
| ~ spl0_122 ),
inference(superposition,[],[f2991,f3505]) ).
fof(f3650,plain,
( ! [X0] :
( big_f(c2,c2)
| c2 = c1
| c1 = X0 )
| ~ spl0_6
| ~ spl0_52
| ~ spl0_86 ),
inference(duplicate_literal_removal,[],[f2499]) ).
fof(f3659,plain,
( ! [X0] :
( c2 = c1
| c1 = X0 )
| ~ spl0_6
| ~ spl0_52
| ~ spl0_56
| ~ spl0_86 ),
inference(forward_subsumption_resolution,[],[f2506,f681]) ).
fof(f3665,plain,
( ! [X0] : c1 = X0
| ~ spl0_6
| spl0_18
| ~ spl0_52
| ~ spl0_56
| ~ spl0_86 ),
inference(forward_subsumption_resolution,[],[f3659,f201]) ).
fof(f3670,plain,
( spl0_48
| ~ spl0_6
| spl0_18
| ~ spl0_52
| ~ spl0_56
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f3665,f1872,f680,f637,f199,f116,f596]) ).
fof(f3699,plain,
( big_f(c2,c2)
| ~ spl0_3
| spl0_18
| ~ spl0_110
| ~ spl0_122 ),
inference(forward_subsumption_resolution,[],[f3636,f201]) ).
fof(f3700,plain,
( ! [X0] :
( big_f(c2,c2)
| c1 = X0 )
| ~ spl0_6
| spl0_18
| ~ spl0_52
| ~ spl0_86 ),
inference(forward_subsumption_resolution,[],[f2506,f201]) ).
fof(f3702,plain,
( ! [X0] :
( big_f(c2,c2)
| c1 = X0 )
| ~ spl0_6
| spl0_18
| ~ spl0_52
| ~ spl0_86 ),
inference(forward_subsumption_resolution,[],[f3650,f201]) ).
fof(f3704,plain,
( spl0_92
| ~ spl0_3
| spl0_18
| ~ spl0_110
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f3699,f3446,f2950,f199,f104,f2206]) ).
fof(f3707,plain,
( spl0_48
| spl0_92
| ~ spl0_6
| spl0_18
| ~ spl0_52
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f3702,f1872,f637,f199,f116,f2206,f596]) ).
fof(f3730,plain,
( spl0_48
| ~ spl0_92
| ~ spl0_1
| ~ spl0_3
| spl0_32
| ~ spl0_110 ),
inference(avatar_split_clause,[],[f3024,f2950,f281,f104,f97,f2206,f596]) ).
fof(f3748,plain,
( ~ spl0_32
| ~ spl0_69
| spl0_73 ),
inference(avatar_split_clause,[],[f2762,f999,f930,f281]) ).
fof(f3789,plain,
( ! [X0] :
( c1 = X0
| ~ big_f(X0,c4)
| c2 = f4(c4) )
| ~ spl0_11 ),
inference(superposition,[],[f147,f3]) ).
fof(f3791,plain,
( spl0_19
| spl0_21
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f3789,f146,f213,f204]) ).
fof(f3799,plain,
( ! [X0] :
( X0 != X0
| c2 = c4
| ~ big_f(X0,c2)
| c2 = f3(c2,X0) )
| ~ spl0_12
| ~ spl0_94 ),
inference(superposition,[],[f151,f2264]) ).
fof(f3801,plain,
( ! [X0] :
( c2 = c4
| ~ big_f(X0,c2)
| c2 = f3(c2,X0) )
| ~ spl0_12
| ~ spl0_94 ),
inference(trivial_inequality_removal,[],[f3799]) ).
fof(f3803,definition,
( spl0_126
<=> ! [X0] :
( ~ big_f(X0,c2)
| c2 = f3(c2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f3804,plain,
( ! [X0] :
( c2 = f3(c2,X0)
| ~ big_f(X0,c2) )
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f3803]) ).
fof(f3862,plain,
( ! [X0] :
( c2 != X0
| c1 = X0
| ~ big_f(c2,c2)
| c1 = X0 )
| ~ spl0_52
| ~ spl0_117 ),
inference(superposition,[],[f3280,f638]) ).
fof(f3863,plain,
( ! [X0] :
( c2 != X0
| c1 = X0
| ~ big_f(c2,c2) )
| ~ spl0_52
| ~ spl0_117 ),
inference(duplicate_literal_removal,[],[f3862]) ).
fof(f3864,plain,
( ! [X0] :
( c1 = X0
| ~ big_f(c2,c2) )
| ~ spl0_52
| ~ spl0_117 ),
inference(forward_subsumption_resolution,[],[f3863,f3]) ).
fof(f3866,plain,
( ~ spl0_92
| spl0_48
| ~ spl0_52
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f3864,f3279,f637,f596,f2206]) ).
fof(f3932,plain,
( ! [X0] :
( ~ big_f(X0,c2)
| c2 = X0 )
| spl0_32 ),
inference(superposition,[],[f282,f3]) ).
fof(f3943,plain,
( ! [X0] :
( c2 = X0
| c2 = c1
| ~ big_f(X0,c1) )
| ~ spl0_15
| ~ spl0_16
| ~ spl0_27
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f569,f3393]) ).
fof(f3945,plain,
( ! [X0] :
( c2 = X0
| ~ big_f(X0,c1) )
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_27
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f3943,f201]) ).
fof(f3947,plain,
( spl0_93
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_27
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f3945,f3392,f241,f199,f172,f165,f2237]) ).
fof(f3965,plain,
( ! [X0] :
( ~ big_f(c1,X0)
| c2 = X0
| ~ big_f(c1,c1) )
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_27
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f645,f201]) ).
fof(f3968,plain,
( spl0_119
| spl0_32 ),
inference(avatar_split_clause,[],[f3932,f281,f3392]) ).
fof(f3973,definition,
( spl0_127
<=> big_f(c1,f10(c2)) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f3975,plain,
( big_f(c1,f10(c2))
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f3973]) ).
fof(f3986,definition,
( spl0_129
<=> ! [X0] :
( c1 = X0
| c2 = f9(c1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f3987,plain,
( ! [X0] :
( c2 = f9(c1,X0)
| c1 = X0 )
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f3986]) ).
fof(f3988,plain,
( spl0_129
| spl0_34
| ~ spl0_3
| spl0_75 ),
inference(avatar_split_clause,[],[f1196,f1100,f104,f318,f3986]) ).
fof(f4001,plain,
( ~ spl0_34
| spl0_62
| ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_27
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f3965,f640,f241,f199,f172,f165,f773,f318]) ).
fof(f4010,plain,
( spl0_33
| ~ spl0_19
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f2803,f1260,f204,f291]) ).
fof(f4011,plain,
( spl0_33
| ~ spl0_23
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f2820,f2237,f221,f291]) ).
fof(f4012,plain,
( ! [X0] :
( c2 = X0
| ~ big_f(X0,c1) )
| ~ spl0_11
| ~ spl0_26
| ~ spl0_27
| ~ spl0_80 ),
inference(forward_demodulation,[],[f1422,f243]) ).
fof(f4015,definition,
( spl0_132
<=> ! [X0] :
( c2 = f3(c1,X0)
| f3(c1,X0) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f4016,plain,
( ! [X0] :
( f3(c1,X0) = X0
| c2 = f3(c1,X0) )
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f4015]) ).
fof(f4017,plain,
( spl0_80
| spl0_132
| ~ spl0_13
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f2819,f2237,f154,f4015,f1260]) ).
fof(f4021,plain,
( spl0_93
| ~ spl0_11
| ~ spl0_26
| ~ spl0_27
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f4012,f1260,f241,f236,f146,f2237]) ).
fof(f4042,plain,
( big_f(c1,c1)
| c2 = f10(c2)
| ~ spl0_127 ),
inference(superposition,[],[f3975,f3]) ).
fof(f4043,plain,
( spl0_110
| spl0_34
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f4042,f3973,f318,f2950]) ).
fof(f4060,plain,
( big_f(c2,c1)
| c2 = f10(c2)
| ~ spl0_115 ),
inference(superposition,[],[f3133,f3]) ).
fof(f4076,definition,
( spl0_133
<=> c2 = f8(c2) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f4078,plain,
( c2 = f8(c2)
| ~ spl0_133 ),
inference(avatar_component_clause,[],[f4076]) ).
fof(f4103,plain,
( c2 = f10(c1)
| ~ spl0_55
| spl0_104 ),
inference(resolution,[],[f2629,f3483]) ).
fof(f4111,plain,
( spl0_75
| ~ spl0_55
| spl0_104 ),
inference(avatar_split_clause,[],[f4103,f2628,f675,f1100]) ).
fof(f4141,plain,
( c2 = c1
| ~ big_f(c1,c2)
| spl0_34
| ~ spl0_49 ),
inference(resolution,[],[f319,f600]) ).
fof(f4183,plain,
( ! [X0] :
( big_f(f7(X0),c2)
| f7(X0) = X0
| c1 = X0
| c2 = f7(X0) )
| ~ spl0_7
| ~ spl0_50 ),
inference(superposition,[],[f124,f631]) ).
fof(f4184,plain,
( ! [X0] :
( f7(X0) = X0
| c1 = X0
| c2 = f7(X0) )
| ~ spl0_7
| ~ spl0_50
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f4183,f3393]) ).
fof(f4185,plain,
( ! [X0] :
( c1 = X0
| c1 = X0
| c2 = c1
| c2 = f7(X0) )
| ~ spl0_7
| ~ spl0_50
| ~ spl0_119 ),
inference(superposition,[],[f4184,f3]) ).
fof(f4189,plain,
( ! [X0] :
( c2 != X0
| c1 = X0
| c2 = f7(X0) )
| ~ spl0_7
| ~ spl0_50
| ~ spl0_119 ),
inference(equality_factoring,[],[f4184]) ).
fof(f4194,plain,
( ! [X0] :
( c1 = X0
| c2 = c1
| c2 = f7(X0) )
| ~ spl0_7
| ~ spl0_50
| ~ spl0_119 ),
inference(duplicate_literal_removal,[],[f4185]) ).
fof(f4195,plain,
( ! [X0] :
( c1 = X0
| c2 = f7(X0) )
| ~ spl0_7
| ~ spl0_50
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f4189,f3]) ).
fof(f4196,plain,
( ! [X0] :
( c1 = X0
| c2 = f7(X0) )
| ~ spl0_7
| spl0_18
| ~ spl0_50
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f4194,f201]) ).
fof(f4197,plain,
( spl0_52
| ~ spl0_7
| ~ spl0_50
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f4195,f3392,f630,f123,f637]) ).
fof(f4198,plain,
( spl0_52
| ~ spl0_7
| spl0_18
| ~ spl0_50
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f4196,f3392,f630,f199,f123,f637]) ).
fof(f4209,plain,
( ! [X2,X3] :
( f3(X2,X3) != X3
| c1 = X2
| ~ big_f(f3(X2,X3),X2) )
| ~ spl0_12
| ~ spl0_80 ),
inference(forward_demodulation,[],[f151,f1262]) ).
fof(f4210,plain,
( ! [X0] :
( c1 = X0
| big_f(c2,X0)
| ~ big_f(c1,X0)
| c1 = X0 )
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_80 ),
inference(forward_demodulation,[],[f1797,f1262]) ).
fof(f4211,plain,
( ! [X0] :
( big_f(c2,X0)
| c1 = X0
| ~ big_f(c1,X0) )
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_80 ),
inference(duplicate_literal_removal,[],[f4210]) ).
fof(f4212,plain,
( ! [X0] :
( c2 = c1
| ~ big_f(X0,c2)
| c2 = f3(c2,X0) )
| ~ spl0_12
| ~ spl0_80
| ~ spl0_94 ),
inference(forward_demodulation,[],[f3801,f1262]) ).
fof(f4220,plain,
( ! [X0] :
( ~ big_f(X0,c2)
| c2 = f3(c2,X0) )
| ~ spl0_12
| spl0_18
| ~ spl0_80
| ~ spl0_94 ),
inference(forward_subsumption_resolution,[],[f4212,f201]) ).
fof(f4222,plain,
( spl0_126
| ~ spl0_12
| spl0_18
| ~ spl0_80
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f4220,f2263,f1260,f199,f150,f3803]) ).
fof(f4228,plain,
( big_f(c2,f10(c2))
| c2 = f10(c2)
| ~ spl0_4
| ~ spl0_133 ),
inference(superposition,[],[f109,f4078]) ).
fof(f4258,plain,
( ! [X0] :
( c2 != X0
| c2 = c1
| ~ big_f(c2,c2)
| ~ big_f(X0,c2) )
| ~ spl0_12
| ~ spl0_80
| ~ spl0_126 ),
inference(superposition,[],[f4209,f3804]) ).
fof(f4265,plain,
( ! [X0] :
( c2 = c1
| ~ big_f(c2,c2)
| ~ big_f(X0,c2) )
| ~ spl0_12
| ~ spl0_80
| ~ spl0_119
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f4258,f3393]) ).
fof(f4313,plain,
( c2 = c1
| ~ big_f(c1,c2)
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_80
| spl0_92 ),
inference(resolution,[],[f4211,f2207]) ).
fof(f4334,plain,
( c1 != c1
| c2 = f10(c1)
| spl0_103 ),
inference(superposition,[],[f2625,f3]) ).
fof(f4335,plain,
( c2 = f10(c1)
| spl0_103 ),
inference(trivial_inequality_removal,[],[f4334]) ).
fof(f4336,plain,
( $false
| spl0_75
| spl0_103 ),
inference(forward_subsumption_resolution,[],[f4335,f1101]) ).
fof(f4337,plain,
( spl0_75
| spl0_103 ),
inference(avatar_contradiction_clause,[],[f4336]) ).
fof(f4345,plain,
( ! [X0] :
( big_f(X0,c2)
| c2 = c1
| c2 = X0
| ~ big_f(X0,c1) )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_69 ),
inference(duplicate_literal_removal,[],[f1382]) ).
fof(f4358,plain,
( spl0_118
| spl0_18
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f2058,f596,f199,f3282]) ).
fof(f4370,plain,
( ! [X0] :
( c2 = c1
| c1 = X0 )
| ~ spl0_6
| ~ spl0_52
| ~ spl0_86
| ~ spl0_89 ),
inference(forward_subsumption_resolution,[],[f2506,f2014]) ).
fof(f4378,plain,
( ! [X0] :
( c2 = f6(c1,X0)
| c1 = X0 )
| ~ spl0_6
| spl0_34
| ~ spl0_69 ),
inference(forward_subsumption_resolution,[],[f1031,f319]) ).
fof(f4385,plain,
( ! [X0] : c1 = X0
| ~ spl0_6
| spl0_18
| ~ spl0_52
| ~ spl0_86
| ~ spl0_89 ),
inference(forward_subsumption_resolution,[],[f4370,f201]) ).
fof(f4390,plain,
( spl0_48
| ~ spl0_6
| spl0_18
| ~ spl0_52
| ~ spl0_86
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f4385,f2013,f1872,f637,f199,f116,f596]) ).
fof(f4391,plain,
( $false
| ~ spl0_92
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f2208,f3091]) ).
fof(f4392,plain,
( ~ spl0_92
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f4391]) ).
fof(f4393,plain,
( ! [X0] : c1 = X0
| ~ spl0_6
| spl0_18
| ~ spl0_52
| ~ spl0_86
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f3700,f3091]) ).
fof(f4400,plain,
( spl0_48
| ~ spl0_6
| spl0_18
| ~ spl0_52
| ~ spl0_86
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f4393,f3090,f1872,f637,f199,f116,f596]) ).
fof(f4409,plain,
( ! [X0] :
( ~ big_f(c2,c2)
| ~ big_f(X0,c2) )
| ~ spl0_12
| spl0_18
| ~ spl0_80
| ~ spl0_119
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f4265,f201]) ).
fof(f4413,plain,
( ! [X0] :
( big_f(c2,c2)
| c1 = X0 )
| ~ spl0_6
| spl0_18
| ~ spl0_52
| ~ spl0_86 ),
inference(forward_subsumption_resolution,[],[f3650,f201]) ).
fof(f4414,plain,
( spl0_114
| ~ spl0_92
| ~ spl0_12
| spl0_18
| ~ spl0_80
| ~ spl0_119
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f4409,f3803,f3392,f1260,f199,f150,f2206,f3090]) ).
fof(f4418,plain,
( spl0_48
| spl0_92
| ~ spl0_6
| spl0_18
| ~ spl0_52
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f4413,f1872,f637,f199,f116,f2206,f596]) ).
fof(f4426,plain,
( spl0_92
| ~ spl0_9
| ~ spl0_19
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f2365,f217,f204,f137,f2206]) ).
fof(f4438,plain,
( big_f(c1,c4)
| c2 = f4(c4)
| ~ spl0_9 ),
inference(superposition,[],[f139,f3]) ).
fof(f4439,plain,
( big_f(f4(c1),c1)
| c2 = c4
| ~ spl0_9 ),
inference(superposition,[],[f139,f3]) ).
fof(f4441,plain,
( spl0_19
| spl0_20
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f4438,f137,f208,f204]) ).
fof(f4457,plain,
( ! [X0] :
( X0 != X0
| c2 = c4
| ~ big_f(X0,c2)
| c2 = f3(c2,X0) )
| ~ spl0_12
| ~ spl0_94 ),
inference(superposition,[],[f151,f2264]) ).
fof(f4459,plain,
( ! [X0] :
( c2 = c4
| ~ big_f(X0,c2)
| c2 = f3(c2,X0) )
| ~ spl0_12
| ~ spl0_94 ),
inference(trivial_inequality_removal,[],[f4457]) ).
fof(f4460,plain,
( spl0_126
| spl0_22
| ~ spl0_12
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f4459,f2263,f150,f217,f3803]) ).
fof(f4491,plain,
( ! [X0,X1] :
( c2 != X0
| c1 != X1
| ~ big_f(c2,c1)
| c2 = f6(X0,X1)
| c1 = X0 )
| ~ spl0_2
| ~ spl0_52 ),
inference(superposition,[],[f1277,f638]) ).
fof(f4492,plain,
( ! [X0,X1] :
( c1 != X1
| ~ big_f(c2,c1)
| c2 = f6(X0,X1)
| c1 = X0 )
| ~ spl0_2
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f4491,f3]) ).
fof(f4496,plain,
( ! [X0] :
( X0 != X0
| c1 = c4
| ~ big_f(X0,c1)
| c2 = f3(c1,X0) )
| ~ spl0_12
| ~ spl0_132 ),
inference(superposition,[],[f151,f4016]) ).
fof(f4498,plain,
( ! [X0] :
( c1 = c4
| ~ big_f(X0,c1)
| c2 = f3(c1,X0) )
| ~ spl0_12
| ~ spl0_132 ),
inference(trivial_inequality_removal,[],[f4496]) ).
fof(f4499,plain,
( ! [X0] :
( c2 = c1
| ~ big_f(X0,c1)
| c2 = f3(c1,X0) )
| ~ spl0_12
| ~ spl0_22
| ~ spl0_132 ),
inference(forward_demodulation,[],[f4498,f219]) ).
fof(f4501,plain,
( ! [X0] :
( c2 = f3(c1,X0)
| ~ big_f(X0,c1) )
| ~ spl0_12
| spl0_18
| ~ spl0_22
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f4499,f201]) ).
fof(f4505,plain,
( ! [X0] :
( c2 != X0
| c1 = c4
| ~ big_f(c2,c1)
| ~ big_f(X0,c1) )
| ~ spl0_12
| spl0_18
| ~ spl0_22
| ~ spl0_132 ),
inference(superposition,[],[f151,f4501]) ).
fof(f4506,plain,
( ! [X0] :
( c1 = c4
| ~ big_f(c2,c1)
| ~ big_f(X0,c1) )
| ~ spl0_12
| spl0_18
| ~ spl0_22
| ~ spl0_101
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f4505,f2543]) ).
fof(f4507,plain,
( ! [X0] :
( c1 = c4
| ~ big_f(X0,c1) )
| ~ spl0_12
| spl0_18
| ~ spl0_22
| ~ spl0_55
| ~ spl0_101
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f4506,f677]) ).
fof(f4508,plain,
( ! [X0] :
( c2 = c1
| ~ big_f(X0,c1) )
| ~ spl0_12
| spl0_18
| ~ spl0_22
| ~ spl0_55
| ~ spl0_101
| ~ spl0_132 ),
inference(forward_demodulation,[],[f4507,f219]) ).
fof(f4509,plain,
( ! [X0] : ~ big_f(X0,c1)
| ~ spl0_12
| spl0_18
| ~ spl0_22
| ~ spl0_55
| ~ spl0_101
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f4508,f201]) ).
fof(f4510,plain,
( spl0_39
| ~ spl0_12
| spl0_18
| ~ spl0_22
| ~ spl0_55
| ~ spl0_101
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f4509,f4015,f2542,f675,f217,f199,f150,f383]) ).
fof(f4530,plain,
( $false
| ~ spl0_39
| ~ spl0_55 ),
inference(resolution,[],[f384,f677]) ).
fof(f4536,plain,
( ~ spl0_39
| ~ spl0_55 ),
inference(avatar_contradiction_clause,[],[f4530]) ).
fof(f4540,plain,
( ! [X0] :
( c2 != X0
| c1 = c4
| ~ big_f(X0,c1) )
| ~ spl0_12
| spl0_18
| ~ spl0_22
| ~ spl0_55
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f4505,f677]) ).
fof(f4541,plain,
( ! [X0] :
( c1 = c4
| ~ big_f(X0,c1) )
| ~ spl0_12
| spl0_18
| ~ spl0_22
| ~ spl0_55
| ~ spl0_93
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f4540,f2238]) ).
fof(f4542,plain,
( ! [X0] :
( c2 = c1
| ~ big_f(X0,c1) )
| ~ spl0_12
| spl0_18
| ~ spl0_22
| ~ spl0_55
| ~ spl0_93
| ~ spl0_132 ),
inference(forward_demodulation,[],[f4541,f219]) ).
fof(f4543,plain,
( ! [X0] : ~ big_f(X0,c1)
| ~ spl0_12
| spl0_18
| ~ spl0_22
| ~ spl0_55
| ~ spl0_93
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f4542,f201]) ).
fof(f4544,plain,
( spl0_39
| ~ spl0_12
| spl0_18
| ~ spl0_22
| ~ spl0_55
| ~ spl0_93
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f4543,f4015,f2237,f675,f217,f199,f150,f383]) ).
fof(f4558,plain,
( ! [X0] :
( f2(c1) = X0
| ~ big_f(c1,X0)
| c2 = c3 )
| ~ spl0_14 ),
inference(superposition,[],[f159,f3]) ).
fof(f4563,plain,
( spl0_27
| spl0_30
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f4558,f158,f267,f241]) ).
fof(f4567,plain,
( big_f(c1,f2(c1))
| ~ spl0_10
| ~ spl0_59 ),
inference(superposition,[],[f143,f706]) ).
fof(f4568,plain,
( big_f(c1,c2)
| ~ spl0_10
| ~ spl0_59
| ~ spl0_82 ),
inference(forward_demodulation,[],[f4567,f1398]) ).
fof(f4570,plain,
( $false
| ~ spl0_10
| spl0_32
| ~ spl0_59
| ~ spl0_82 ),
inference(forward_subsumption_resolution,[],[f4568,f282]) ).
fof(f4571,plain,
( ~ spl0_10
| spl0_32
| ~ spl0_59
| ~ spl0_82 ),
inference(avatar_contradiction_clause,[],[f4570]) ).
fof(f4577,plain,
( ! [X2,X3] :
( f3(X2,X3) != X3
| c2 = X2
| ~ big_f(f3(X2,X3),X2) )
| ~ spl0_12
| ~ spl0_22 ),
inference(forward_demodulation,[],[f151,f219]) ).
fof(f4579,plain,
( ! [X0] :
( c2 = c1
| c2 = X0
| ~ big_f(X0,c1) )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_69
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f4345,f3393]) ).
fof(f4582,plain,
( ! [X0] :
( c2 = X0
| ~ big_f(X0,c1) )
| ~ spl0_2
| ~ spl0_6
| spl0_18
| ~ spl0_69
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f4579,f201]) ).
fof(f4584,plain,
( spl0_93
| ~ spl0_2
| ~ spl0_6
| spl0_18
| ~ spl0_69
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f4582,f3392,f930,f199,f116,f100,f2237]) ).
fof(f4604,plain,
( spl0_57
| ~ spl0_7
| ~ spl0_41
| spl0_55 ),
inference(avatar_split_clause,[],[f2020,f675,f439,f123,f684]) ).
fof(f4617,plain,
( spl0_75
| spl0_103 ),
inference(avatar_split_clause,[],[f4335,f2624,f1100]) ).
fof(f4620,plain,
( ~ spl0_55
| spl0_86
| ~ spl0_2
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f4492,f637,f100,f1872,f675]) ).
fof(f4621,plain,
( spl0_110
| spl0_55
| ~ spl0_115 ),
inference(avatar_split_clause,[],[f4060,f3132,f675,f2950]) ).
fof(f4624,definition,
( spl0_137
<=> ! [X0,X1] :
( c1 = X1
| c1 = X0
| c2 = f6(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f4625,plain,
( ! [X0,X1] :
( c2 = f6(X0,X1)
| c1 = X0
| c1 = X1 )
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f4624]) ).
fof(f4626,plain,
( spl0_137
| spl0_55
| ~ spl0_6
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f2503,f637,f116,f675,f4624]) ).
fof(f4669,plain,
( ! [X0,X1] :
( c2 != X1
| f7(X0) != X0
| ~ big_f(f7(X0),c2)
| c1 = X0
| c1 = X1 )
| ~ spl0_2
| ~ spl0_137 ),
inference(superposition,[],[f101,f4625]) ).
fof(f4670,plain,
( ! [X0,X1] :
( f7(X0) != X0
| ~ big_f(f7(X0),c2)
| c1 = X0
| c1 = X1 )
| ~ spl0_2
| ~ spl0_137 ),
inference(forward_subsumption_resolution,[],[f4669,f3]) ).
fof(f4757,plain,
( ! [X0] :
( c2 != X0
| c1 != f10(c1)
| ~ big_f(c2,f10(c1))
| c1 = X0 )
| ~ spl0_1
| ~ spl0_129 ),
inference(superposition,[],[f98,f3987]) ).
fof(f4862,plain,
( ! [X0] :
( c2 = X0
| c2 = X0
| ~ big_f(c1,X0) )
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| ~ spl0_91 ),
inference(resolution,[],[f2193,f2382]) ).
fof(f4868,plain,
( ! [X0] :
( c2 = X0
| ~ big_f(c1,X0) )
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| ~ spl0_91 ),
inference(duplicate_literal_removal,[],[f4862]) ).
fof(f4869,plain,
( spl0_62
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f4868,f2192,f217,f199,f154,f150,f773]) ).
fof(f4870,plain,
( c2 = c1
| ~ big_f(c1,c2)
| ~ spl0_49
| ~ spl0_62 ),
inference(duplicate_literal_removal,[],[f780]) ).
fof(f4893,plain,
( ! [X0,X1] :
( big_f(c1,X0)
| c2 = X0
| c1 = X1
| c2 = f3(X0,X1) )
| ~ spl0_13
| ~ spl0_22 ),
inference(superposition,[],[f3435,f3]) ).
fof(f4895,plain,
( ! [X0,X1] :
( c2 = f3(X0,X1)
| c1 = X1
| c2 = X0 )
| ~ spl0_13
| ~ spl0_22
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f4893,f774]) ).
fof(f4904,plain,
( ! [X0,X1] :
( c2 != X1
| c2 = X0
| ~ big_f(c2,X0)
| c1 = X1
| c2 = X0 )
| ~ spl0_12
| ~ spl0_13
| ~ spl0_22
| ~ spl0_62 ),
inference(superposition,[],[f4577,f4895]) ).
fof(f4905,plain,
( ! [X0,X1] :
( c2 != X1
| c2 = X0
| ~ big_f(c2,X0)
| c1 = X1 )
| ~ spl0_12
| ~ spl0_13
| ~ spl0_22
| ~ spl0_62 ),
inference(duplicate_literal_removal,[],[f4904]) ).
fof(f4915,plain,
( c1 != c1
| c2 = f8(c2)
| spl0_111 ),
inference(superposition,[],[f2955,f3]) ).
fof(f4916,plain,
( c2 = f8(c2)
| spl0_111 ),
inference(trivial_inequality_removal,[],[f4915]) ).
fof(f4917,plain,
( spl0_133
| spl0_111 ),
inference(avatar_split_clause,[],[f4916,f2954,f4076]) ).
fof(f4953,plain,
( c2 = f10(c2)
| ~ spl0_4
| ~ spl0_62
| ~ spl0_111 ),
inference(forward_subsumption_resolution,[],[f3158,f774]) ).
fof(f4956,plain,
( ~ big_f(c1,c2)
| spl0_18
| spl0_34
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f4141,f201]) ).
fof(f4958,plain,
( ~ big_f(c1,c2)
| spl0_18
| ~ spl0_49
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f4870,f201]) ).
fof(f4969,plain,
( ! [X0] :
( c1 != f10(c1)
| ~ big_f(c2,f10(c1))
| c1 = X0 )
| ~ spl0_1
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f4757,f3]) ).
fof(f4985,plain,
( spl0_110
| ~ spl0_4
| ~ spl0_62
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f4953,f2954,f773,f108,f2950]) ).
fof(f4986,plain,
( ~ spl0_32
| spl0_18
| spl0_34
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f4956,f599,f318,f199,f281]) ).
fof(f4987,plain,
( ~ spl0_32
| spl0_18
| ~ spl0_49
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f4958,f773,f599,f199,f281]) ).
fof(f4988,plain,
( spl0_48
| ~ spl0_104
| ~ spl0_103
| ~ spl0_1
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f4969,f3986,f97,f2624,f2628,f596]) ).
fof(f5110,plain,
( ! [X0] :
( c2 != X0
| c1 != f7(c1)
| ~ big_f(f7(c1),c2)
| c1 = X0 )
| ~ spl0_2
| ~ spl0_6
| spl0_34
| ~ spl0_69 ),
inference(superposition,[],[f101,f4378]) ).
fof(f5115,plain,
( spl0_48
| spl0_109
| ~ spl0_15
| ~ spl0_16
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f2921,f704,f172,f165,f2923,f596]) ).
fof(f5118,plain,
( ! [X0] :
( c2 != X0
| ~ big_f(f7(c1),c2)
| c1 = X0 )
| ~ spl0_2
| ~ spl0_6
| spl0_34
| ~ spl0_69 ),
inference(forward_subsumption_resolution,[],[f5110,f932]) ).
fof(f5120,plain,
( ! [X0] :
( c2 != X0
| c1 = X0 )
| ~ spl0_2
| ~ spl0_6
| spl0_34
| ~ spl0_69
| ~ spl0_73 ),
inference(forward_subsumption_resolution,[],[f5118,f1001]) ).
fof(f5121,plain,
( ! [X0] : c1 = X0
| ~ spl0_2
| ~ spl0_6
| spl0_34
| ~ spl0_69
| ~ spl0_73 ),
inference(forward_subsumption_resolution,[],[f5120,f3]) ).
fof(f5122,plain,
( spl0_48
| ~ spl0_2
| ~ spl0_6
| spl0_34
| ~ spl0_69
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f5121,f999,f930,f318,f116,f100,f596]) ).
fof(f5143,plain,
( spl0_110
| spl0_127
| ~ spl0_4
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f3475,f2954,f108,f3973,f2950]) ).
fof(f5181,plain,
( spl0_17
| spl0_90
| ~ spl0_5
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f2008,f1100,f112,f2017,f196]) ).
fof(f5186,plain,
( spl0_34
| ~ spl0_20
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f1313,f1260,f208,f318]) ).
fof(f5193,plain,
( ~ big_f(c1,c2)
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_80
| spl0_92 ),
inference(forward_subsumption_resolution,[],[f4313,f201]) ).
fof(f5214,plain,
( ! [X0] : c2 = X0
| ~ spl0_1
| ~ spl0_3
| spl0_18
| ~ spl0_84
| ~ spl0_91
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f3570,f2193]) ).
fof(f5227,plain,
( spl0_48
| spl0_117
| ~ spl0_2
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f4670,f4624,f100,f3279,f596]) ).
fof(f5275,plain,
( $false
| ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_32
| ~ spl0_80
| spl0_92 ),
inference(forward_subsumption_resolution,[],[f5193,f283]) ).
fof(f5276,plain,
( ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_32
| ~ spl0_80
| spl0_92 ),
inference(avatar_contradiction_clause,[],[f5275]) ).
fof(f5304,plain,
( spl0_17
| ~ spl0_1
| ~ spl0_3
| spl0_18
| ~ spl0_84
| ~ spl0_91
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f5214,f2624,f2192,f1678,f199,f104,f97,f196]) ).
fof(f5346,plain,
( spl0_17
| spl0_47
| ~ spl0_8
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f2045,f439,f130,f503,f196]) ).
fof(f5354,plain,
( ! [X0,X1] :
( c2 = X0
| ~ big_f(c2,X0)
| c1 = X1 )
| ~ spl0_12
| ~ spl0_13
| ~ spl0_22
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f4905,f3]) ).
fof(f5355,plain,
( ~ spl0_34
| spl0_26
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f1508,f704,f236,f318]) ).
fof(f5379,plain,
( spl0_110
| spl0_115
| ~ spl0_4
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f4228,f4076,f108,f3132,f2950]) ).
fof(f5381,plain,
( spl0_22
| spl0_23
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f4439,f137,f221,f217]) ).
fof(f5382,plain,
( spl0_48
| spl0_91
| ~ spl0_12
| ~ spl0_13
| ~ spl0_22
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f5354,f773,f217,f154,f150,f2192,f596]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f102]) ).
cnf(s2,plain,
( spl0_2
| spl0_3 ),
inference(sat_conversion,[],[f106]) ).
cnf(s3,plain,
( spl0_2
| spl0_4 ),
inference(sat_conversion,[],[f110]) ).
cnf(s4,plain,
( spl0_2
| spl0_5 ),
inference(sat_conversion,[],[f114]) ).
cnf(s5,plain,
( spl0_1
| spl0_6 ),
inference(sat_conversion,[],[f118]) ).
cnf(s6,plain,
( spl0_3
| spl0_6 ),
inference(sat_conversion,[],[f119]) ).
cnf(s7,plain,
( spl0_4
| spl0_6 ),
inference(sat_conversion,[],[f120]) ).
cnf(s8,plain,
( spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f121]) ).
cnf(s9,plain,
( spl0_1
| spl0_7 ),
inference(sat_conversion,[],[f125]) ).
cnf(s10,plain,
( spl0_3
| spl0_7 ),
inference(sat_conversion,[],[f126]) ).
cnf(s11,plain,
( spl0_4
| spl0_7 ),
inference(sat_conversion,[],[f127]) ).
cnf(s13,plain,
( spl0_1
| spl0_8 ),
inference(sat_conversion,[],[f132]) ).
cnf(s14,plain,
( spl0_3
| spl0_8 ),
inference(sat_conversion,[],[f133]) ).
cnf(s16,plain,
( spl0_5
| spl0_8 ),
inference(sat_conversion,[],[f135]) ).
cnf(s17,plain,
( spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f144]) ).
cnf(s19,plain,
( spl0_10
| spl0_12 ),
inference(sat_conversion,[],[f152]) ).
cnf(s20,plain,
( spl0_10
| spl0_13 ),
inference(sat_conversion,[],[f156]) ).
cnf(s21,plain,
( spl0_9
| spl0_14 ),
inference(sat_conversion,[],[f160]) ).
cnf(s22,plain,
( spl0_11
| spl0_14 ),
inference(sat_conversion,[],[f161]) ).
cnf(s23,plain,
( spl0_12
| spl0_14 ),
inference(sat_conversion,[],[f162]) ).
cnf(s24,plain,
( spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f163]) ).
cnf(s25,plain,
( spl0_9
| spl0_15 ),
inference(sat_conversion,[],[f167]) ).
cnf(s26,plain,
( spl0_11
| spl0_15 ),
inference(sat_conversion,[],[f168]) ).
cnf(s27,plain,
( spl0_12
| spl0_15 ),
inference(sat_conversion,[],[f169]) ).
cnf(s28,plain,
( spl0_13
| spl0_15 ),
inference(sat_conversion,[],[f170]) ).
cnf(s29,plain,
( spl0_9
| spl0_16 ),
inference(sat_conversion,[],[f174]) ).
cnf(s30,plain,
( spl0_11
| spl0_16 ),
inference(sat_conversion,[],[f175]) ).
cnf(s31,plain,
( spl0_12
| spl0_16 ),
inference(sat_conversion,[],[f176]) ).
cnf(s32,plain,
( spl0_13
| spl0_16 ),
inference(sat_conversion,[],[f177]) ).
cnf(s54,plain,
~ spl0_18,
inference(sat_conversion,[],[f338]) ).
cnf(s67,plain,
( spl0_18
| ~ spl0_26
| ~ spl0_27
| ~ spl0_35 ),
inference(sat_conversion,[],[f414]) ).
cnf(s76,plain,
( ~ spl0_14
| ~ spl0_27
| spl0_47 ),
inference(sat_conversion,[],[f508]) ).
cnf(s81,plain,
( ~ spl0_15
| ~ spl0_16
| ~ spl0_27
| spl0_48
| spl0_49 ),
inference(sat_conversion,[],[f601]) ).
cnf(s82,plain,
( ~ spl0_8
| spl0_50
| spl0_51 ),
inference(sat_conversion,[],[f635]) ).
cnf(s83,plain,
( ~ spl0_8
| spl0_52
| spl0_53 ),
inference(sat_conversion,[],[f642]) ).
cnf(s84,plain,
( ~ spl0_34
| spl0_51
| ~ spl0_53 ),
inference(sat_conversion,[],[f654]) ).
cnf(s85,plain,
( spl0_18
| ~ spl0_32
| ~ spl0_49
| spl0_51
| ~ spl0_53 ),
inference(sat_conversion,[],[f655]) ).
cnf(s86,plain,
( spl0_18
| ~ spl0_34
| spl0_51
| ~ spl0_53 ),
inference(sat_conversion,[],[f657]) ).
cnf(s94,plain,
( ~ spl0_47
| ~ spl0_55
| spl0_56 ),
inference(sat_conversion,[],[f692]) ).
cnf(s102,plain,
( ~ spl0_8
| ~ spl0_50
| spl0_52
| spl0_62 ),
inference(sat_conversion,[],[f776]) ).
cnf(s104,plain,
( spl0_18
| ~ spl0_34
| ~ spl0_62 ),
inference(sat_conversion,[],[f788]) ).
cnf(s106,plain,
( ~ spl0_26
| spl0_34
| ~ spl0_59 ),
inference(sat_conversion,[],[f796]) ).
cnf(s115,plain,
( ~ spl0_7
| spl0_34
| spl0_50 ),
inference(sat_conversion,[],[f823]) ).
cnf(s118,plain,
( spl0_18
| ~ spl0_26
| spl0_34
| ~ spl0_59 ),
inference(sat_conversion,[],[f826]) ).
cnf(s123,plain,
( ~ spl0_7
| ~ spl0_15
| ~ spl0_16
| spl0_17
| spl0_18
| ~ spl0_41
| ~ spl0_47
| ~ spl0_55
| ~ spl0_56
| ~ spl0_59 ),
inference(sat_conversion,[],[f877]) ).
cnf(s135,plain,
( ~ spl0_43
| spl0_55
| ~ spl0_56 ),
inference(sat_conversion,[],[f921]) ).
cnf(s138,plain,
( spl0_18
| ~ spl0_43
| spl0_55
| ~ spl0_56 ),
inference(sat_conversion,[],[f928]) ).
cnf(s148,plain,
( spl0_41
| spl0_69 ),
inference(sat_conversion,[],[f1011]) ).
cnf(s171,plain,
( ~ spl0_14
| spl0_53
| ~ spl0_59 ),
inference(sat_conversion,[],[f1218]) ).
cnf(s181,plain,
( ~ spl0_2
| ~ spl0_34
| spl0_41
| spl0_42 ),
inference(sat_conversion,[],[f1232]) ).
cnf(s188,plain,
( ~ spl0_6
| spl0_18
| spl0_32
| ~ spl0_42
| ~ spl0_69 ),
inference(sat_conversion,[],[f1233]) ).
cnf(s207,plain,
( ~ spl0_11
| spl0_24
| ~ spl0_80 ),
inference(sat_conversion,[],[f1292]) ).
cnf(s211,plain,
( ~ spl0_30
| spl0_53 ),
inference(sat_conversion,[],[f1400]) ).
cnf(s226,plain,
( ~ spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f1618]) ).
cnf(s239,plain,
( ~ spl0_26
| spl0_27
| spl0_84 ),
inference(sat_conversion,[],[f1680]) ).
cnf(s244,plain,
( spl0_27
| spl0_59 ),
inference(sat_conversion,[],[f1696]) ).
cnf(s264,plain,
( ~ spl0_11
| ~ spl0_34
| spl0_35
| ~ spl0_80 ),
inference(sat_conversion,[],[f1754]) ).
cnf(s273,plain,
( spl0_41
| spl0_69 ),
inference(sat_conversion,[],[f1807]) ).
cnf(s276,plain,
( spl0_18
| ~ spl0_32
| ~ spl0_51 ),
inference(sat_conversion,[],[f1847]) ).
cnf(s279,plain,
( ~ spl0_4
| spl0_18
| spl0_32
| ~ spl0_75
| spl0_77 ),
inference(sat_conversion,[],[f1852]) ).
cnf(s283,plain,
( spl0_26
| ~ spl0_27
| ~ spl0_55 ),
inference(sat_conversion,[],[f1867]) ).
cnf(s311,plain,
( ~ spl0_26
| ~ spl0_27
| spl0_55 ),
inference(sat_conversion,[],[f2182]) ).
cnf(s313,plain,
( ~ spl0_23
| ~ spl0_33
| spl0_55 ),
inference(sat_conversion,[],[f2184]) ).
cnf(s330,plain,
( ~ spl0_7
| spl0_18
| ~ spl0_41
| spl0_43 ),
inference(sat_conversion,[],[f2203]) ).
cnf(s334,plain,
( ~ spl0_7
| spl0_18
| ~ spl0_41
| ~ spl0_57
| spl0_92 ),
inference(sat_conversion,[],[f2211]) ).
cnf(s343,plain,
( ~ spl0_4
| spl0_18
| ~ spl0_75
| ~ spl0_77
| spl0_92 ),
inference(sat_conversion,[],[f2252]) ).
cnf(s348,plain,
( ~ spl0_9
| ~ spl0_22
| ~ spl0_31
| spl0_92 ),
inference(sat_conversion,[],[f2266]) ).
cnf(s350,plain,
( ~ spl0_21
| ~ spl0_22
| spl0_89 ),
inference(sat_conversion,[],[f2267]) ).
cnf(s364,plain,
( ~ spl0_9
| ~ spl0_22
| spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f2293]) ).
cnf(s365,plain,
( ~ spl0_47
| spl0_91
| ~ spl0_92 ),
inference(sat_conversion,[],[f2295]) ).
cnf(s367,plain,
( spl0_18
| ~ spl0_89
| ~ spl0_92 ),
inference(sat_conversion,[],[f2327]) ).
cnf(s373,plain,
( spl0_55
| spl0_91 ),
inference(sat_conversion,[],[f2368]) ).
cnf(s374,plain,
( ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| spl0_55
| ~ spl0_84 ),
inference(sat_conversion,[],[f2379]) ).
cnf(s377,plain,
( ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| ~ spl0_34
| spl0_55 ),
inference(sat_conversion,[],[f2406]) ).
cnf(s381,plain,
( spl0_17
| ~ spl0_55
| ~ spl0_91 ),
inference(sat_conversion,[],[f2424]) ).
cnf(s388,plain,
( ~ spl0_5
| spl0_100
| spl0_101 ),
inference(sat_conversion,[],[f2544]) ).
cnf(s390,plain,
( ~ spl0_34
| spl0_35
| ~ spl0_101 ),
inference(sat_conversion,[],[f2561]) ).
cnf(s391,plain,
( ~ spl0_55
| spl0_93
| ~ spl0_101 ),
inference(sat_conversion,[],[f2564]) ).
cnf(s393,plain,
( spl0_18
| ~ spl0_55
| spl0_93
| ~ spl0_101 ),
inference(sat_conversion,[],[f2569]) ).
cnf(s427,plain,
( ~ spl0_12
| ~ spl0_13
| spl0_48
| ~ spl0_51
| spl0_56
| ~ spl0_80 ),
inference(sat_conversion,[],[f2619]) ).
cnf(s433,plain,
( ~ spl0_1
| ~ spl0_34
| spl0_75
| spl0_76 ),
inference(sat_conversion,[],[f2622]) ).
cnf(s440,plain,
( ~ spl0_3
| spl0_18
| spl0_55
| spl0_75
| ~ spl0_76 ),
inference(sat_conversion,[],[f2640]) ).
cnf(s446,plain,
( ~ spl0_15
| ~ spl0_16
| spl0_18
| spl0_27
| ~ spl0_55
| ~ spl0_56
| ~ spl0_59
| spl0_107 ),
inference(sat_conversion,[],[f2655]) ).
cnf(s457,plain,
( ~ spl0_10
| spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f2668]) ).
cnf(s463,plain,
( ~ spl0_55
| ~ spl0_107 ),
inference(sat_conversion,[],[f2701]) ).
cnf(s466,plain,
( ~ spl0_9
| ~ spl0_19
| spl0_108 ),
inference(sat_conversion,[],[f2743]) ).
cnf(s467,plain,
( ~ spl0_25
| ~ spl0_59
| spl0_82 ),
inference(sat_conversion,[],[f2748]) ).
cnf(s469,plain,
( spl0_18
| ~ spl0_21
| ~ spl0_108 ),
inference(sat_conversion,[],[f2776]) ).
cnf(s474,plain,
( spl0_22
| spl0_80 ),
inference(sat_conversion,[],[f2801]) ).
cnf(s475,plain,
( ~ spl0_24
| ~ spl0_33
| spl0_93 ),
inference(sat_conversion,[],[f2811]) ).
cnf(s476,plain,
( ~ spl0_26
| spl0_27
| ~ spl0_93 ),
inference(sat_conversion,[],[f2830]) ).
cnf(s479,plain,
( spl0_18
| ~ spl0_34
| ~ spl0_93 ),
inference(sat_conversion,[],[f2836]) ).
cnf(s483,plain,
( ~ spl0_13
| spl0_18
| spl0_32
| ~ spl0_80
| spl0_94 ),
inference(sat_conversion,[],[f2963]) ).
cnf(s485,plain,
( spl0_18
| ~ spl0_100
| spl0_110 ),
inference(sat_conversion,[],[f2982]) ).
cnf(s488,plain,
( ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_55
| ~ spl0_59
| spl0_92 ),
inference(sat_conversion,[],[f3054]) ).
cnf(s519,plain,
( spl0_55
| ~ spl0_80
| ~ spl0_108 ),
inference(sat_conversion,[],[f3097]) ).
cnf(s534,plain,
( spl0_18
| spl0_55
| ~ spl0_80
| ~ spl0_108 ),
inference(sat_conversion,[],[f3114]) ).
cnf(s542,plain,
( ~ spl0_55
| ~ spl0_80
| spl0_108 ),
inference(sat_conversion,[],[f3126]) ).
cnf(s604,plain,
~ spl0_118,
inference(sat_conversion,[],[f3298]) ).
cnf(s609,plain,
( spl0_18
| spl0_55
| ~ spl0_92
| ~ spl0_109 ),
inference(sat_conversion,[],[f3333]) ).
cnf(s631,plain,
( ~ spl0_11
| ~ spl0_19
| ~ spl0_22
| spl0_119 ),
inference(sat_conversion,[],[f3413]) ).
cnf(s644,plain,
( ~ spl0_90
| ~ spl0_92
| spl0_119 ),
inference(sat_conversion,[],[f3455]) ).
cnf(s672,plain,
( ~ spl0_1
| ~ spl0_32
| ~ spl0_110
| spl0_122 ),
inference(sat_conversion,[],[f3503]) ).
cnf(s674,plain,
( spl0_18
| ~ spl0_32
| ~ spl0_119 ),
inference(sat_conversion,[],[f3534]) ).
cnf(s675,plain,
( ~ spl0_10
| ~ spl0_25
| ~ spl0_27
| spl0_92 ),
inference(sat_conversion,[],[f3542]) ).
cnf(s684,plain,
( ~ spl0_4
| ~ spl0_56
| ~ spl0_77
| spl0_103 ),
inference(sat_conversion,[],[f3550]) ).
cnf(s724,plain,
( ~ spl0_6
| spl0_18
| spl0_48
| ~ spl0_52
| ~ spl0_56
| ~ spl0_86 ),
inference(sat_conversion,[],[f3670]) ).
cnf(s736,plain,
( ~ spl0_3
| spl0_18
| spl0_92
| ~ spl0_110
| ~ spl0_122 ),
inference(sat_conversion,[],[f3704]) ).
cnf(s739,plain,
( ~ spl0_6
| spl0_18
| spl0_48
| ~ spl0_52
| ~ spl0_86
| spl0_92 ),
inference(sat_conversion,[],[f3707]) ).
cnf(s751,plain,
( ~ spl0_1
| ~ spl0_3
| spl0_32
| spl0_48
| ~ spl0_92
| ~ spl0_110 ),
inference(sat_conversion,[],[f3730]) ).
cnf(s772,plain,
( ~ spl0_32
| ~ spl0_69
| spl0_73 ),
inference(sat_conversion,[],[f3748]) ).
cnf(s813,plain,
( ~ spl0_11
| spl0_19
| spl0_21 ),
inference(sat_conversion,[],[f3791]) ).
cnf(s823,plain,
( spl0_48
| ~ spl0_52
| ~ spl0_92
| ~ spl0_117 ),
inference(sat_conversion,[],[f3866]) ).
cnf(s831,plain,
( ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_27
| spl0_93
| ~ spl0_119 ),
inference(sat_conversion,[],[f3947]) ).
cnf(s846,plain,
( spl0_32
| spl0_119 ),
inference(sat_conversion,[],[f3968]) ).
cnf(s853,plain,
( ~ spl0_3
| spl0_34
| spl0_75
| spl0_129 ),
inference(sat_conversion,[],[f3988]) ).
cnf(s867,plain,
( ~ spl0_15
| ~ spl0_16
| spl0_18
| ~ spl0_27
| ~ spl0_34
| ~ spl0_53
| spl0_62 ),
inference(sat_conversion,[],[f4001]) ).
cnf(s870,plain,
( ~ spl0_19
| spl0_33
| ~ spl0_80 ),
inference(sat_conversion,[],[f4010]) ).
cnf(s872,plain,
( ~ spl0_23
| spl0_33
| ~ spl0_93 ),
inference(sat_conversion,[],[f4011]) ).
cnf(s878,plain,
( ~ spl0_13
| spl0_80
| ~ spl0_93
| spl0_132 ),
inference(sat_conversion,[],[f4017]) ).
cnf(s883,plain,
( ~ spl0_11
| ~ spl0_26
| ~ spl0_27
| ~ spl0_80
| spl0_93 ),
inference(sat_conversion,[],[f4021]) ).
cnf(s887,plain,
( spl0_34
| spl0_110
| ~ spl0_127 ),
inference(sat_conversion,[],[f4043]) ).
cnf(s897,plain,
( ~ spl0_55
| spl0_75
| spl0_104 ),
inference(sat_conversion,[],[f4111]) ).
cnf(s900,plain,
( ~ spl0_7
| ~ spl0_50
| spl0_52
| ~ spl0_119 ),
inference(sat_conversion,[],[f4197]) ).
cnf(s901,plain,
( ~ spl0_7
| spl0_18
| ~ spl0_50
| spl0_52
| ~ spl0_119 ),
inference(sat_conversion,[],[f4198]) ).
cnf(s903,plain,
( ~ spl0_12
| spl0_18
| ~ spl0_80
| ~ spl0_94
| spl0_126 ),
inference(sat_conversion,[],[f4222]) ).
cnf(s908,plain,
( spl0_75
| spl0_103 ),
inference(sat_conversion,[],[f4337]) ).
cnf(s911,plain,
( spl0_18
| ~ spl0_48
| spl0_118 ),
inference(sat_conversion,[],[f4358]) ).
cnf(s920,plain,
( ~ spl0_6
| spl0_18
| spl0_48
| ~ spl0_52
| ~ spl0_86
| ~ spl0_89 ),
inference(sat_conversion,[],[f4390]) ).
cnf(s924,plain,
( ~ spl0_92
| ~ spl0_114 ),
inference(sat_conversion,[],[f4392]) ).
cnf(s925,plain,
( ~ spl0_6
| spl0_18
| spl0_48
| ~ spl0_52
| ~ spl0_86
| ~ spl0_114 ),
inference(sat_conversion,[],[f4400]) ).
cnf(s936,plain,
( ~ spl0_12
| spl0_18
| ~ spl0_80
| ~ spl0_92
| spl0_114
| ~ spl0_119
| ~ spl0_126 ),
inference(sat_conversion,[],[f4414]) ).
cnf(s940,plain,
( ~ spl0_6
| spl0_18
| spl0_48
| ~ spl0_52
| ~ spl0_86
| spl0_92 ),
inference(sat_conversion,[],[f4418]) ).
cnf(s950,plain,
( ~ spl0_9
| ~ spl0_19
| ~ spl0_22
| spl0_92 ),
inference(sat_conversion,[],[f4426]) ).
cnf(s963,plain,
( ~ spl0_9
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f4441]) ).
cnf(s968,plain,
( ~ spl0_12
| spl0_22
| ~ spl0_94
| spl0_126 ),
inference(sat_conversion,[],[f4460]) ).
cnf(s969,plain,
( ~ spl0_12
| spl0_18
| ~ spl0_22
| spl0_39
| ~ spl0_55
| ~ spl0_101
| ~ spl0_132 ),
inference(sat_conversion,[],[f4510]) ).
cnf(s975,plain,
( ~ spl0_39
| ~ spl0_55 ),
inference(sat_conversion,[],[f4536]) ).
cnf(s978,plain,
( ~ spl0_12
| spl0_18
| ~ spl0_22
| spl0_39
| ~ spl0_55
| ~ spl0_93
| ~ spl0_132 ),
inference(sat_conversion,[],[f4544]) ).
cnf(s995,plain,
( ~ spl0_14
| spl0_27
| spl0_30 ),
inference(sat_conversion,[],[f4563]) ).
cnf(s996,plain,
( ~ spl0_10
| spl0_32
| ~ spl0_59
| ~ spl0_82 ),
inference(sat_conversion,[],[f4571]) ).
cnf(s997,plain,
( ~ spl0_2
| ~ spl0_6
| spl0_18
| ~ spl0_69
| spl0_93
| ~ spl0_119 ),
inference(sat_conversion,[],[f4584]) ).
cnf(s1009,plain,
( ~ spl0_7
| ~ spl0_41
| spl0_55
| spl0_57 ),
inference(sat_conversion,[],[f4604]) ).
cnf(s1051,plain,
( spl0_75
| spl0_103 ),
inference(sat_conversion,[],[f4617]) ).
cnf(s1054,plain,
( ~ spl0_2
| ~ spl0_52
| ~ spl0_55
| spl0_86 ),
inference(sat_conversion,[],[f4620]) ).
cnf(s1055,plain,
( spl0_55
| spl0_110
| ~ spl0_115 ),
inference(sat_conversion,[],[f4621]) ).
cnf(s1057,plain,
( ~ spl0_6
| ~ spl0_52
| spl0_55
| spl0_137 ),
inference(sat_conversion,[],[f4626]) ).
cnf(s1109,plain,
( ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_22
| spl0_62
| ~ spl0_91 ),
inference(sat_conversion,[],[f4869]) ).
cnf(s1116,plain,
( spl0_111
| spl0_133 ),
inference(sat_conversion,[],[f4917]) ).
cnf(s1156,plain,
( ~ spl0_4
| ~ spl0_62
| spl0_110
| ~ spl0_111 ),
inference(sat_conversion,[],[f4985]) ).
cnf(s1158,plain,
( spl0_18
| ~ spl0_32
| spl0_34
| ~ spl0_49 ),
inference(sat_conversion,[],[f4986]) ).
cnf(s1160,plain,
( spl0_18
| ~ spl0_32
| ~ spl0_49
| ~ spl0_62 ),
inference(sat_conversion,[],[f4987]) ).
cnf(s1166,plain,
( ~ spl0_1
| spl0_48
| ~ spl0_103
| ~ spl0_104
| ~ spl0_129 ),
inference(sat_conversion,[],[f4988]) ).
cnf(s1194,plain,
( ~ spl0_15
| ~ spl0_16
| spl0_48
| ~ spl0_59
| spl0_109 ),
inference(sat_conversion,[],[f5115]) ).
cnf(s1206,plain,
( ~ spl0_2
| ~ spl0_6
| spl0_34
| spl0_48
| ~ spl0_69
| ~ spl0_73 ),
inference(sat_conversion,[],[f5122]) ).
cnf(s1208,plain,
( ~ spl0_4
| spl0_110
| ~ spl0_111
| spl0_127 ),
inference(sat_conversion,[],[f5143]) ).
cnf(s1285,plain,
( ~ spl0_5
| spl0_17
| ~ spl0_75
| spl0_90 ),
inference(sat_conversion,[],[f5181]) ).
cnf(s1286,plain,
( ~ spl0_20
| spl0_34
| ~ spl0_80 ),
inference(sat_conversion,[],[f5186]) ).
cnf(s1299,plain,
( ~ spl0_2
| spl0_48
| spl0_117
| ~ spl0_137 ),
inference(sat_conversion,[],[f5227]) ).
cnf(s1351,plain,
( ~ spl0_12
| ~ spl0_13
| spl0_18
| ~ spl0_32
| ~ spl0_80
| spl0_92 ),
inference(sat_conversion,[],[f5276]) ).
cnf(s1363,plain,
( ~ spl0_1
| ~ spl0_3
| spl0_17
| spl0_18
| ~ spl0_84
| ~ spl0_91
| ~ spl0_103 ),
inference(sat_conversion,[],[f5304]) ).
cnf(s1385,plain,
( ~ spl0_8
| spl0_17
| ~ spl0_41
| spl0_47 ),
inference(sat_conversion,[],[f5346]) ).
cnf(s1416,plain,
( spl0_26
| ~ spl0_34
| ~ spl0_59 ),
inference(sat_conversion,[],[f5355]) ).
cnf(s1461,plain,
( ~ spl0_4
| spl0_110
| spl0_115
| ~ spl0_133 ),
inference(sat_conversion,[],[f5379]) ).
cnf(s1463,plain,
( ~ spl0_9
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f5381]) ).
cnf(s1473,plain,
( ~ spl0_12
| ~ spl0_13
| ~ spl0_22
| spl0_48
| ~ spl0_62
| spl0_91 ),
inference(sat_conversion,[],[f5382]) ).
cnf(s1486,plain,
~ spl0_48,
inference(rat,[],[s911,s604,s54]) ).
cnf(s1487,plain,
~ spl0_17,
inference(rat,[],[s226,s54]) ).
cnf(s1488,plain,
( ~ spl0_26
| spl0_34
| spl0_9
| spl0_1 ),
inference(rat,[],[s1054,s739,s900,s365,s846,s381,s1158,s311,s81,s76,s244,s118,s5,s1,s29,s25,s21,s115,s9,s1486,s54,s1487]) ).
cnf(s1489,plain,
( ~ spl0_27
| spl0_34
| spl0_9
| spl0_1 ),
inference(rat,[],[s1299,s823,s1057,s900,s846,s1158,s675,s283,s81,s5,s1,s29,s25,s115,s9,s457,s1488,s17,s1486,s54]) ).
cnf(s1490,plain,
( ~ spl0_69
| ~ spl0_32
| spl0_34
| spl0_1 ),
inference(rat,[],[s1206,s772,s5,s1,s1486]) ).
cnf(s1491,plain,
( spl0_55
| ~ spl0_41
| ~ spl0_109
| ~ spl0_7 ),
inference(rat,[],[s334,s1009,s609,s54]) ).
cnf(s1492,plain,
( spl0_34
| spl0_9
| spl0_1 ),
inference(rat,[],[s123,s94,s1491,s1385,s273,s1490,s996,s1194,s467,s244,s1489,s457,s1488,s13,s9,s29,s25,s17,s1487,s54,s1486]) ).
cnf(s1493,plain,
( spl0_55
| ~ spl0_27
| ~ spl0_52
| ~ spl0_10
| spl0_1 ),
inference(rat,[],[s823,s675,s1299,s457,s1057,s311,s5,s1,s1486]) ).
cnf(s1494,plain,
( spl0_53
| spl0_9
| spl0_1 ),
inference(rat,[],[s724,s1054,s94,s1493,s76,s995,s83,s211,s13,s5,s1,s21,s17,s1486,s54]) ).
cnf(s1495,plain,
( spl0_9
| spl0_1 ),
inference(rat,[],[s123,s94,s1491,s1385,s273,s997,s1194,s846,s244,s276,s867,s84,s1494,s104,s479,s1492,s25,s29,s13,s9,s5,s1,s1487,s54,s1486]) ).
cnf(s1496,plain,
( ~ spl0_52
| ~ spl0_92
| spl0_55
| spl0_1 ),
inference(rat,[],[s1299,s823,s1057,s5,s1,s1486]) ).
cnf(s1497,plain,
( spl0_19
| ~ spl0_11
| spl0_89
| spl0_34
| ~ spl0_9 ),
inference(rat,[],[s474,s1286,s350,s963,s813]) ).
cnf(s1498,plain,
( ~ spl0_11
| spl0_89
| spl0_34
| spl0_119
| spl0_55
| ~ spl0_9 ),
inference(rat,[],[s474,s519,s631,s466,s1497]) ).
cnf(s1499,plain,
( spl0_34
| ~ spl0_32
| spl0_55
| ~ spl0_59
| spl0_1 ),
inference(rat,[],[s1194,s26,s30,s1498,s367,s334,s1009,s1491,s273,s1490,s9,s1495,s674,s1486,s54]) ).
cnf(s1500,plain,
( ~ spl0_32
| spl0_55
| ~ spl0_59
| spl0_1 ),
inference(rat,[],[s474,s377,s1351,s23,s24,s1496,s171,s102,s86,s104,s1499,s82,s276,s13,s54]) ).
cnf(s1501,plain,
( ~ spl0_80
| spl0_34
| spl0_55
| ~ spl0_9 ),
inference(rat,[],[s466,s963,s534,s1286,s54]) ).
cnf(s1502,plain,
( spl0_34
| spl0_32
| spl0_55
| spl0_1 ),
inference(rat,[],[s348,s364,s474,s1501,s1496,s900,s115,s9,s1495,s846]) ).
cnf(s1503,plain,
( spl0_16
| ~ spl0_80
| ~ spl0_51
| spl0_56 ),
inference(rat,[],[s427,s31,s32,s1486]) ).
cnf(s1504,plain,
( ~ spl0_80
| ~ spl0_51
| spl0_56
| spl0_109
| ~ spl0_59 ),
inference(rat,[],[s427,s27,s28,s1194,s1503,s1486]) ).
cnf(s1505,plain,
( spl0_16
| ~ spl0_22
| ~ spl0_84
| spl0_55 ),
inference(rat,[],[s374,s31,s32,s54]) ).
cnf(s1506,plain,
( spl0_55
| spl0_27
| spl0_1 ),
inference(rat,[],[s374,s27,s28,s1194,s1505,s474,s1504,s84,s83,s1496,s334,s138,s1009,s1491,s330,s273,s239,s997,s1416,s479,s1502,s846,s1500,s13,s9,s5,s1,s244,s54,s1486]) ).
cnf(s1507,plain,
( spl0_16
| spl0_92
| ~ spl0_32
| ~ spl0_80 ),
inference(rat,[],[s1351,s31,s32,s54]) ).
cnf(s1508,plain,
( ~ spl0_32
| ~ spl0_80
| spl0_34
| spl0_27
| spl0_1 ),
inference(rat,[],[s1351,s27,s28,s446,s1507,s365,s94,s1385,s273,s1490,s13,s244,s463,s381,s1506,s54,s1487]) ).
cnf(s1509,plain,
( ~ spl0_10
| spl0_32
| spl0_26
| ~ spl0_59 ),
inference(rat,[],[s467,s996,s457]) ).
cnf(s1510,plain,
( ~ spl0_80
| spl0_34
| spl0_27
| spl0_1 ),
inference(rat,[],[s903,s936,s483,s19,s20,s1509,s925,s940,s1054,s900,s846,s1508,s5,s1,s1506,s115,s9,s106,s244,s54,s1486]) ).
cnf(s1511,plain,
( spl0_16
| spl0_19
| ~ spl0_22
| spl0_34
| ~ spl0_55
| spl0_1 ),
inference(rat,[],[s1054,s920,s102,s1497,s1473,s30,s31,s32,s13,s5,s1,s1495,s381,s115,s9,s54,s1486,s1487]) ).
cnf(s1512,plain,
( ~ spl0_47
| spl0_34
| spl0_27
| spl0_1 ),
inference(rat,[],[s1054,s920,s102,s1497,s1473,s26,s27,s28,s446,s1511,s950,s365,s94,s13,s5,s1,s1495,s244,s463,s381,s1506,s115,s9,s474,s1510,s54,s1486,s1487]) ).
cnf(s1513,plain,
( spl0_34
| spl0_27
| spl0_1 ),
inference(rat,[],[s878,s978,s19,s20,s997,s1509,s846,s1490,s273,s1385,s1512,s474,s1510,s106,s13,s5,s1,s244,s975,s1506,s54,s1487]) ).
cnf(s1514,plain,
( ~ spl0_11
| spl0_21
| ~ spl0_80
| spl0_93 ),
inference(rat,[],[s870,s475,s813,s207]) ).
cnf(s1515,plain,
( spl0_11
| spl0_27
| spl0_1 ),
inference(rat,[],[s188,s181,s273,s276,s1385,s84,s365,s171,s488,s22,s26,s30,s13,s5,s1,s244,s381,s1506,s1513,s54,s1487]) ).
cnf(s1516,plain,
( ~ spl0_80
| ~ spl0_11
| spl0_93
| ~ spl0_55 ),
inference(rat,[],[s469,s1514,s542,s54]) ).
cnf(s1517,plain,
( ~ spl0_32
| spl0_27
| spl0_1 ),
inference(rat,[],[s920,s1054,s350,s102,s813,s82,s631,s276,s674,s13,s5,s1,s104,s474,s1516,s1515,s479,s1513,s1506,s54,s1486]) ).
cnf(s1518,plain,
( spl0_27
| spl0_1 ),
inference(rat,[],[s1385,s365,s273,s348,s997,s364,s846,s1517,s474,s1516,s1515,s479,s1513,s381,s1506,s13,s5,s1,s1495,s1487,s54]) ).
cnf(s1519,plain,
( spl0_34
| spl0_55
| spl0_1 ),
inference(rat,[],[s81,s26,s30,s1498,s367,s334,s1009,s273,s1490,s1158,s674,s1502,s9,s1495,s1518,s1486,s54]) ).
cnf(s1520,plain,
( ~ spl0_32
| ~ spl0_80
| spl0_55
| spl0_1 ),
inference(rat,[],[s1351,s19,s20,s1493,s1496,s102,s82,s276,s13,s1518,s104,s1519,s54]) ).
cnf(s1521,plain,
( ~ spl0_80
| spl0_55
| spl0_1 ),
inference(rat,[],[s427,s27,s28,s831,s1503,s84,s83,s1496,s334,s138,s1009,s330,s273,s997,s846,s1520,s13,s9,s5,s1,s1518,s479,s1519,s1486,s54]) ).
cnf(s1522,plain,
( spl0_10
| ~ spl0_22
| ~ spl0_34
| spl0_55 ),
inference(rat,[],[s377,s19,s20,s54]) ).
cnf(s1523,plain,
( spl0_12
| ~ spl0_119
| spl0_93
| ~ spl0_27 ),
inference(rat,[],[s831,s27,s31,s54]) ).
cnf(s1524,plain,
( spl0_55
| spl0_1 ),
inference(rat,[],[s831,s28,s32,s377,s1523,s846,s276,s84,s83,s1493,s1522,s474,s1521,s479,s1519,s13,s1518,s54]) ).
cnf(s1525,plain,
( ~ spl0_32
| ~ spl0_80
| spl0_34
| spl0_1 ),
inference(rat,[],[s1351,s27,s28,s81,s1507,s365,s1385,s273,s1490,s1158,s13,s1518,s381,s1524,s54,s1486,s1487]) ).
cnf(s1526,plain,
( ~ spl0_80
| spl0_34
| spl0_1 ),
inference(rat,[],[s903,s936,s483,s23,s24,s76,s365,s925,s940,s1054,s901,s846,s1525,s5,s1,s1518,s381,s1524,s115,s9,s54,s1486,s1487]) ).
cnf(s1527,plain,
( ~ spl0_32
| spl0_34
| spl0_1 ),
inference(rat,[],[s1054,s920,s102,s1497,s1473,s26,s27,s28,s81,s1511,s950,s365,s1385,s273,s1490,s1158,s13,s5,s1,s1495,s1518,s381,s1524,s115,s9,s474,s1526,s54,s1486,s1487]) ).
cnf(s1528,plain,
( spl0_34
| spl0_1 ),
inference(rat,[],[s978,s878,s997,s23,s24,s273,s76,s1385,s365,s348,s364,s846,s1527,s474,s1526,s13,s5,s1,s1495,s1518,s975,s381,s1524,s54,s1487]) ).
cnf(s1529,plain,
( ~ spl0_32
| spl0_1 ),
inference(rat,[],[s813,s631,s350,s474,s883,s22,s76,s365,s920,s940,s1054,s102,s82,s276,s674,s13,s5,s1,s381,s283,s1524,s1518,s479,s104,s1528,s54,s1486,s1487]) ).
cnf(s1530,plain,
( spl0_11
| spl0_1 ),
inference(rat,[],[s831,s26,s30,s1518,s479,s1528,s846,s1529,s54]) ).
cnf(s1531,plain,
spl0_1,
inference(rat,[],[s348,s364,s474,s883,s1530,s365,s1385,s273,s997,s846,s1529,s479,s1528,s283,s381,s1524,s1518,s1495,s1,s5,s13,s1487,s54]) ).
cnf(s1533,plain,
( ~ spl0_110
| ~ spl0_3
| spl0_92
| ~ spl0_32 ),
inference(rat,[],[s736,s672,s54,s1531]) ).
cnf(s1534,plain,
( spl0_6
| spl0_92
| ~ spl0_32
| spl0_34
| spl0_55 ),
inference(rat,[],[s1116,s1208,s1461,s887,s1055,s1533,s6,s7]) ).
cnf(s1535,plain,
( spl0_2
| spl0_92
| ~ spl0_32
| spl0_34
| spl0_55 ),
inference(rat,[],[s1116,s1208,s1461,s887,s1055,s1533,s2,s3]) ).
cnf(s1536,plain,
( ~ spl0_69
| ~ spl0_2
| ~ spl0_6
| ~ spl0_32
| spl0_34 ),
inference(rat,[],[s1206,s772,s1486]) ).
cnf(s1537,plain,
( spl0_9
| spl0_34
| spl0_55
| ~ spl0_59 ),
inference(rat,[],[s1116,s1208,s1461,s887,s1055,s1533,s10,s11,s1491,s273,s1536,s1535,s1534,s609,s1509,s1194,s17,s25,s29,s106,s54,s1486]) ).
cnf(s1538,plain,
( spl0_7
| spl0_92
| ~ spl0_32
| spl0_34
| spl0_55 ),
inference(rat,[],[s1116,s1208,s1461,s887,s1055,s1533,s10,s11]) ).
cnf(s1539,plain,
( spl0_92
| ~ spl0_32
| spl0_55
| spl0_34 ),
inference(rat,[],[s334,s1009,s1538,s273,s1536,s1535,s1534,s54]) ).
cnf(s1540,plain,
( ~ spl0_32
| spl0_34
| spl0_55
| ~ spl0_59 ),
inference(rat,[],[s1194,s26,s30,s1498,s609,s367,s1539,s674,s1537,s1486,s54]) ).
cnf(s1541,plain,
( spl0_6
| ~ spl0_62
| ~ spl0_92
| spl0_32
| spl0_55 ),
inference(rat,[],[s1116,s1461,s1156,s1055,s751,s6,s7,s1531,s1486]) ).
cnf(s1542,plain,
( ~ spl0_52
| ~ spl0_2
| ~ spl0_6
| ~ spl0_92
| spl0_55 ),
inference(rat,[],[s1299,s823,s1057,s1486]) ).
cnf(s1543,plain,
( ~ spl0_7
| spl0_52
| ~ spl0_119
| spl0_34 ),
inference(rat,[],[s900,s115]) ).
cnf(s1544,plain,
( spl0_7
| ~ spl0_62
| ~ spl0_92
| spl0_32
| spl0_55 ),
inference(rat,[],[s1116,s1461,s1156,s1055,s751,s10,s11,s1531,s1486]) ).
cnf(s1545,plain,
( spl0_34
| spl0_55
| ~ spl0_59 ),
inference(rat,[],[s1116,s1461,s1156,s1055,s751,s2,s3,s1542,s1543,s1544,s1541,s1109,s348,s19,s20,s364,s1509,s846,s1540,s474,s1501,s1537,s106,s373,s1531,s1486,s54]) ).
cnf(s1546,plain,
( spl0_6
| spl0_90
| ~ spl0_84
| ~ spl0_91 ),
inference(rat,[],[s908,s1363,s1285,s6,s8,s1487,s54,s1531]) ).
cnf(s1547,plain,
( spl0_8
| spl0_90
| ~ spl0_84
| ~ spl0_91 ),
inference(rat,[],[s908,s1363,s1285,s14,s16,s1487,s54,s1531]) ).
cnf(s1548,plain,
( ~ spl0_32
| ~ spl0_84
| spl0_55
| ~ spl0_59 ),
inference(rat,[],[s908,s1363,s1285,s2,s4,s1542,s83,s1547,s1546,s644,s1351,s474,s377,s23,s24,s171,s86,s276,s674,s373,s1545,s1487,s54,s1531]) ).
cnf(s1549,plain,
( spl0_6
| spl0_92
| spl0_32
| ~ spl0_84
| ~ spl0_91 ),
inference(rat,[],[s279,s343,s1051,s1363,s6,s7,s54,s1487,s1531]) ).
cnf(s1550,plain,
( spl0_7
| spl0_92
| spl0_32
| ~ spl0_84
| ~ spl0_91 ),
inference(rat,[],[s279,s343,s1051,s1363,s10,s11,s54,s1487,s1531]) ).
cnf(s1551,plain,
( ~ spl0_41
| ~ spl0_7
| spl0_92
| spl0_55 ),
inference(rat,[],[s334,s1009,s54]) ).
cnf(s1552,plain,
( spl0_92
| spl0_32
| ~ spl0_84
| spl0_93
| spl0_55 ),
inference(rat,[],[s279,s343,s1051,s1363,s2,s3,s997,s273,s1551,s1550,s1549,s373,s846,s54,s1487,s1531]) ).
cnf(s1553,plain,
( ~ spl0_80
| spl0_56
| spl0_109
| ~ spl0_92
| spl0_32
| ~ spl0_34
| ~ spl0_59 ),
inference(rat,[],[s903,s936,s483,s23,s24,s171,s86,s1504,s846,s924,s54]) ).
cnf(s1554,plain,
( ~ spl0_22
| ~ spl0_84
| spl0_55
| ~ spl0_59 ),
inference(rat,[],[s1109,s27,s28,s1194,s1505,s373,s104,s609,s1552,s1548,s479,s1545,s54,s1486]) ).
cnf(s1555,plain,
( spl0_6
| ~ spl0_56
| spl0_32
| ~ spl0_84
| ~ spl0_91 ),
inference(rat,[],[s279,s684,s1051,s1363,s6,s7,s54,s1487,s1531]) ).
cnf(s1556,plain,
( spl0_7
| ~ spl0_56
| spl0_32
| ~ spl0_84
| ~ spl0_91 ),
inference(rat,[],[s279,s684,s1051,s1363,s10,s11,s54,s1487,s1531]) ).
cnf(s1557,plain,
( spl0_55
| spl0_27 ),
inference(rat,[],[s279,s684,s1051,s1363,s2,s3,s997,s273,s330,s1556,s1555,s135,s1553,s474,s1554,s609,s1552,s846,s1548,s239,s1416,s479,s1545,s373,s244,s54,s1487,s1531]) ).
cnf(s1558,plain,
( ~ spl0_80
| spl0_92
| ~ spl0_32
| spl0_27 ),
inference(rat,[],[s1351,s27,s28,s488,s1507,s244,s1557,s54]) ).
cnf(s1559,plain,
( spl0_12
| spl0_92
| spl0_27 ),
inference(rat,[],[s488,s27,s31,s244,s1557,s54]) ).
cnf(s1560,plain,
( spl0_13
| spl0_92
| spl0_27 ),
inference(rat,[],[s488,s28,s32,s244,s1557,s54]) ).
cnf(s1561,plain,
( ~ spl0_101
| ~ spl0_13
| ~ spl0_12
| spl0_80
| ~ spl0_55 ),
inference(rat,[],[s878,s969,s393,s975,s474,s54]) ).
cnf(s1562,plain,
( spl0_6
| spl0_101
| spl0_92
| ~ spl0_32 ),
inference(rat,[],[s485,s1533,s388,s6,s8,s54]) ).
cnf(s1563,plain,
( spl0_5
| ~ spl0_6
| spl0_62
| spl0_92
| spl0_51
| ~ spl0_55 ),
inference(rat,[],[s739,s1054,s102,s82,s4,s16,s1486,s54]) ).
cnf(s1564,plain,
( spl0_92
| ~ spl0_32
| spl0_27 ),
inference(rat,[],[s739,s1054,s102,s82,s2,s14,s1533,s485,s388,s1563,s1562,s1561,s1473,s1560,s1559,s474,s1558,s381,s1557,s276,s1486,s54,s1487]) ).
cnf(s1565,plain,
( spl0_6
| spl0_34
| spl0_90
| ~ spl0_55 ),
inference(rat,[],[s1166,s853,s897,s1051,s1285,s6,s8,s1486,s1531,s1487]) ).
cnf(s1566,plain,
( spl0_75
| ~ spl0_3
| spl0_34
| ~ spl0_55 ),
inference(rat,[],[s1166,s853,s897,s1051,s1486,s1531]) ).
cnf(s1567,plain,
( spl0_5
| ~ spl0_6
| spl0_34
| spl0_47
| ~ spl0_32 ),
inference(rat,[],[s148,s1536,s1385,s4,s16,s1487]) ).
cnf(s1568,plain,
( spl0_34
| spl0_90
| spl0_47
| ~ spl0_32
| ~ spl0_55 ),
inference(rat,[],[s148,s1536,s1385,s2,s14,s1566,s1285,s1567,s1565,s1487]) ).
cnf(s1569,plain,
( ~ spl0_32
| spl0_27 ),
inference(rat,[],[s813,s631,s350,s474,s1516,s22,s171,s86,s479,s1568,s644,s365,s367,s1564,s276,s674,s244,s381,s1557,s54,s1487]) ).
cnf(s1570,plain,
( spl0_6
| spl0_34
| spl0_92
| spl0_27 ),
inference(rat,[],[s279,s343,s1566,s6,s7,s1557,s1569,s54]) ).
cnf(s1571,plain,
( ~ spl0_4
| ~ spl0_75
| spl0_92
| spl0_32 ),
inference(rat,[],[s279,s343,s54]) ).
cnf(s1572,plain,
( spl0_4
| spl0_34
| spl0_92
| spl0_27 ),
inference(rat,[],[s739,s1054,s1543,s3,s11,s1557,s846,s1569,s1570,s1486,s54]) ).
cnf(s1573,plain,
( spl0_34
| spl0_92
| spl0_27 ),
inference(rat,[],[s739,s1054,s1543,s2,s10,s1566,s1571,s1572,s1570,s1557,s846,s1569,s1486,s54]) ).
cnf(s1574,plain,
( spl0_11
| spl0_92
| spl0_27 ),
inference(rat,[],[s488,s26,s30,s244,s1557,s54]) ).
cnf(s1575,plain,
( ~ spl0_9
| ~ spl0_22
| spl0_92
| spl0_32 ),
inference(rat,[],[s348,s364]) ).
cnf(s1576,plain,
( spl0_92
| spl0_27 ),
inference(rat,[],[s488,s25,s29,s1575,s474,s1516,s1574,s479,s1573,s244,s1557,s1569,s54]) ).
cnf(s1577,plain,
( ~ spl0_80
| spl0_10
| spl0_27 ),
inference(rat,[],[s903,s936,s483,s846,s1569,s924,s1576,s20,s19,s54]) ).
cnf(s1578,plain,
( spl0_6
| spl0_101
| spl0_27 ),
inference(rat,[],[s485,s751,s388,s6,s8,s1569,s1576,s54,s1531,s1486]) ).
cnf(s1579,plain,
( ~ spl0_93
| spl0_80
| ~ spl0_12
| ~ spl0_13
| ~ spl0_55 ),
inference(rat,[],[s978,s878,s975,s474,s54]) ).
cnf(s1580,plain,
( spl0_5
| spl0_10
| spl0_27 ),
inference(rat,[],[s148,s997,s1385,s4,s16,s846,s1569,s365,s1576,s381,s1578,s1561,s1579,s1577,s19,s20,s1557,s54,s1487]) ).
cnf(s1581,plain,
( spl0_10
| spl0_27 ),
inference(rat,[],[s148,s997,s1385,s2,s14,s751,s485,s388,s1580,s1579,s1578,s1561,s1577,s19,s20,s846,s1569,s365,s1576,s381,s1557,s54,s1487,s1531,s1486]) ).
cnf(s1582,plain,
( spl0_5
| spl0_27 ),
inference(rat,[],[s148,s997,s1385,s4,s16,s846,s365,s1576,s381,s1578,s391,s476,s1509,s1581,s1569,s244,s1557,s54,s1487]) ).
cnf(s1583,plain,
spl0_27,
inference(rat,[],[s148,s997,s1385,s2,s14,s751,s485,s388,s1582,s1578,s391,s476,s1509,s1581,s365,s1576,s846,s1569,s381,s1557,s244,s54,s1487,s1531,s1486]) ).
cnf(s1584,plain,
( ~ spl0_10
| spl0_92
| spl0_26 ),
inference(rat,[],[s675,s457,s1583]) ).
cnf(s1585,plain,
( spl0_92
| ~ spl0_32
| spl0_55 ),
inference(rat,[],[s474,s1351,s1522,s19,s20,s1584,s1539,s311,s54,s1583]) ).
cnf(s1586,plain,
( spl0_9
| spl0_49 ),
inference(rat,[],[s81,s25,s29,s1486,s1583]) ).
cnf(s1587,plain,
( spl0_34
| ~ spl0_32
| spl0_55 ),
inference(rat,[],[s81,s26,s30,s1498,s1586,s1158,s674,s367,s1585,s1486,s1583,s54]) ).
cnf(s1588,plain,
( spl0_6
| ~ spl0_32
| spl0_55 ),
inference(rat,[],[s440,s433,s1285,s6,s8,s644,s1585,s674,s1587,s54,s1531,s1487]) ).
cnf(s1589,plain,
( spl0_75
| ~ spl0_3
| ~ spl0_34
| spl0_55 ),
inference(rat,[],[s440,s433,s54,s1531]) ).
cnf(s1590,plain,
( spl0_5
| ~ spl0_32
| spl0_55 ),
inference(rat,[],[s1542,s83,s4,s16,s1585,s86,s1587,s276,s1588,s54]) ).
cnf(s1591,plain,
( ~ spl0_32
| spl0_55 ),
inference(rat,[],[s1542,s83,s2,s14,s1589,s1285,s1590,s1588,s86,s1587,s644,s1585,s276,s674,s1487,s54]) ).
cnf(s1592,plain,
( spl0_6
| spl0_92
| spl0_55 ),
inference(rat,[],[s1589,s1571,s6,s7,s1501,s474,s1575,s1591,s17,s1584,s311,s1583]) ).
cnf(s1593,plain,
( spl0_4
| spl0_92
| spl0_55 ),
inference(rat,[],[s148,s997,s1551,s3,s11,s846,s872,s313,s1463,s1575,s17,s1584,s311,s1591,s1592,s54,s1583]) ).
cnf(s1594,plain,
( spl0_92
| spl0_55 ),
inference(rat,[],[s148,s997,s1551,s2,s10,s1589,s1571,s1593,s1592,s872,s1501,s313,s474,s1463,s1575,s17,s1584,s311,s846,s1591,s54,s1583]) ).
cnf(s1595,plain,
( spl0_6
| spl0_34
| spl0_55 ),
inference(rat,[],[s1116,s1208,s1461,s887,s1055,s751,s6,s7,s1591,s1594,s1531,s1486]) ).
cnf(s1596,plain,
( ~ spl0_4
| spl0_127
| spl0_115
| spl0_110 ),
inference(rat,[],[s1116,s1208,s1461]) ).
cnf(s1597,plain,
( spl0_4
| spl0_34
| spl0_55 ),
inference(rat,[],[s1542,s1543,s3,s11,s846,s1591,s1594,s1595]) ).
cnf(s1598,plain,
( spl0_110
| spl0_34
| spl0_55 ),
inference(rat,[],[s1596,s887,s1055,s1597]) ).
cnf(s1599,plain,
( spl0_34
| spl0_55 ),
inference(rat,[],[s1542,s1543,s2,s10,s751,s1598,s1595,s846,s1591,s1594,s1531,s1486]) ).
cnf(s1600,plain,
( spl0_13
| spl0_55 ),
inference(rat,[],[s831,s28,s32,s846,s1591,s479,s1599,s54,s1583]) ).
cnf(s1601,plain,
spl0_55,
inference(rat,[],[s968,s483,s936,s474,s1109,s1600,s1523,s104,s479,s1599,s924,s1594,s846,s1591,s373,s54,s1583]) ).
cnf(s1604,plain,
~ spl0_91,
inference(rat,[],[s381,s1487,s1601]) ).
cnf(s1606,plain,
spl0_26,
inference(rat,[],[s283,s1583,s1601]) ).
cnf(s1607,plain,
~ spl0_35,
inference(rat,[],[s67,s1583,s54,s1606]) ).
cnf(s1609,plain,
( spl0_12
| spl0_49 ),
inference(rat,[],[s81,s27,s31,s1486,s1583]) ).
cnf(s1610,plain,
( spl0_13
| spl0_49 ),
inference(rat,[],[s81,s28,s32,s1486,s1583]) ).
cnf(s1611,plain,
( spl0_49
| spl0_92
| ~ spl0_32 ),
inference(rat,[],[s739,s1054,s102,s82,s2,s14,s1533,s485,s388,s1563,s1562,s1473,s1561,s474,s1351,s1610,s1609,s276,s1486,s54,s1601,s1604]) ).
cnf(s1612,plain,
( spl0_92
| ~ spl0_32 ),
inference(rat,[],[s739,s1054,s83,s2,s14,s1533,s485,s388,s1563,s1562,s390,s85,s1160,s1158,s1611,s276,s1486,s54,s1601,s1607]) ).
cnf(s1613,plain,
~ spl0_32,
inference(rat,[],[s813,s631,s350,s474,s883,s479,s22,s1568,s76,s644,s365,s367,s1612,s674,s1583,s1606,s54,s1601,s1604]) ).
cnf(s1614,plain,
spl0_119,
inference(rat,[],[s846,s1613]) ).
cnf(s1615,plain,
( spl0_4
| spl0_92
| spl0_34 ),
inference(rat,[],[s739,s1054,s1543,s3,s7,s11,s1486,s54,s1601,s1614]) ).
cnf(s1616,plain,
( spl0_92
| spl0_34 ),
inference(rat,[],[s739,s1054,s1543,s2,s6,s10,s1566,s1571,s1615,s1613,s1614,s1601,s54,s1486]) ).
cnf(s1617,plain,
( ~ spl0_80
| ~ spl0_92 ),
inference(rat,[],[s903,s483,s936,s924,s24,s23,s76,s365,s54,s1613,s1614,s1583,s1604]) ).
cnf(s1618,plain,
( spl0_5
| ~ spl0_92 ),
inference(rat,[],[s148,s997,s1385,s4,s8,s16,s1579,s1617,s24,s23,s76,s365,s54,s1614,s1487,s1601,s1583,s1604]) ).
cnf(s1619,plain,
~ spl0_92,
inference(rat,[],[s148,s997,s1385,s2,s6,s14,s751,s485,s388,s1618,s1561,s1579,s1617,s23,s24,s76,s365,s54,s1614,s1487,s1531,s1486,s1613,s1601,s1583,s1604]) ).
cnf(s1620,plain,
spl0_34,
inference(rat,[],[s1616,s1619]) ).
cnf(s1621,plain,
~ spl0_93,
inference(rat,[],[s479,s54,s1620]) ).
cnf(s1627,plain,
spl0_11,
inference(rat,[],[s831,s26,s30,s54,s1614,s1621,s1583]) ).
cnf(s1628,plain,
~ spl0_80,
inference(rat,[],[s264,s1607,s1620,s1627]) ).
cnf(s1629,plain,
spl0_22,
inference(rat,[],[s474,s1628]) ).
cnf(s1632,plain,
~ spl0_9,
inference(rat,[],[s1575,s1613,s1619,s1629]) ).
cnf(s1634,plain,
spl0_16,
inference(rat,[],[s29,s1632]) ).
cnf(s1635,plain,
spl0_15,
inference(rat,[],[s25,s1632]) ).
cnf(s1639,plain,
$false,
inference(rat,[],[s831,s1583,s1621,s1614,s54,s1634,s1635]) ).
fof(f5383,plain,
$false,
inference(avatar_sat_refutation,[],[s1639]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN076-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.19 % Computer : n008.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Mon Sep 28 15:31:39 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 Running first-order theorem proving
% 0.10/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.74/2.35 % (2344035)Input is clausal, will run a generic CNF schedule.
% 11.74/2.35 % (2344042)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1363917459:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.74/2.35 % (2344043)lrs+10_1_sil=8000:sp=occurrence:random_seed=830341750:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.74/2.35 % (2344044)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3681959541:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.74/2.35 % (2344041)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3726281503:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.74/2.35 % (2344046)dis-21_1_sil=8000:lcm=predicate:random_seed=3644143033: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)
% 11.74/2.35 % (2344040)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=3994025076:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.74/2.35 % (2344045)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3286305337:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.74/2.35 % (2344043)Refutation not found, incomplete strategy
% 11.74/2.35 % (2344043)------------------------------
% 11.74/2.35 % (2344043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.74/2.35 % (2344043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.74/2.35 % (2344043)CaDiCaL version: 2.1.3
% 11.74/2.35 % (2344043)Termination reason: Refutation not found, incomplete strategy
% 11.74/2.35 % (2344043)Time elapsed: 0.002 s
% 11.74/2.35 % (2344043)Peak memory usage: 88 MB
% 11.74/2.35 % (2344043)Instructions burned: 2 (million)
% 11.74/2.35 % (2344044)Refutation not found, incomplete strategy
% 11.74/2.35 % (2344044)------------------------------
% 11.74/2.35 % (2344044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.74/2.35 % (2344044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.74/2.35 % (2344044)CaDiCaL version: 2.1.3
% 11.74/2.35 % (2344044)Termination reason: Refutation not found, incomplete strategy
% 11.74/2.35 % (2344044)Time elapsed: 0.003 s
% 11.74/2.35 % (2344044)Peak memory usage: 88 MB
% 11.74/2.35 % (2344044)Instructions burned: 3 (million)
% 11.74/2.35 % (2344046)Instruction limit reached!
% 11.74/2.35 % (2344046)------------------------------
% 11.74/2.35 % (2344046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.74/2.35 % (2344046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.74/2.35 % (2344046)CaDiCaL version: 2.1.3
% 11.74/2.35 % (2344046)Termination reason: Instruction limit
% 11.74/2.35 % (2344046)Termination phase: Saturation
% 11.74/2.35 % (2344046)Time elapsed: 0.067 s
% 11.74/2.35 % (2344046)Peak memory usage: 89 MB
% 11.74/2.35 % (2344046)Instructions burned: 119 (million)
% 11.74/2.35 % (2344045)Instruction limit reached!
% 11.74/2.35 % (2344045)------------------------------
% 11.74/2.35 % (2344045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.74/2.35 % (2344045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.74/2.35 % (2344045)CaDiCaL version: 2.1.3
% 11.74/2.35 % (2344045)Termination reason: Instruction limit
% 11.74/2.35 % (2344045)Termination phase: Saturation
% 11.74/2.35 % (2344045)Time elapsed: 0.114 s
% 11.74/2.35 % (2344045)Peak memory usage: 89 MB
% 11.74/2.35 % (2344045)Instructions burned: 181 (million)
% 11.74/2.35 % (2344054)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=3955932112:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.74/2.35 % (2344054)Refutation not found, incomplete strategy
% 11.74/2.35 % (2344054)------------------------------
% 11.74/2.35 % (2344054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.74/2.35 % (2344054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.74/2.35 % (2344054)CaDiCaL version: 2.1.3
% 11.74/2.35 % (2344054)Termination reason: Refutation not found, incomplete strategy
% 11.74/2.35 % (2344054)Time elapsed: 0.003 s
% 11.74/2.35 % (2344054)Peak memory usage: 88 MB
% 11.74/2.35 % (2344054)Instructions burned: 3 (million)
% 11.74/2.35 % (2344043)------------------------------
% 21.36/3.70 % (2344043)------------------------------
% 21.36/3.70 % (2344044)------------------------------
% 21.36/3.70 % (2344044)------------------------------
% 21.36/3.70 % (2344055)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3816360134: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)
% 21.36/3.70 % (2344055)Refutation not found, incomplete strategy
% 21.36/3.70 % (2344055)------------------------------
% 21.36/3.70 % (2344055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.36/3.70 % (2344055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.36/3.70 % (2344055)CaDiCaL version: 2.1.3
% 21.36/3.70 % (2344055)Termination reason: Refutation not found, incomplete strategy
% 21.36/3.70 % (2344055)Time elapsed: 0.003 s
% 21.36/3.70 % (2344055)Peak memory usage: 88 MB
% 21.36/3.70 % (2344055)Instructions burned: 4 (million)
% 21.36/3.70 % (2344057)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1683500853:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 21.36/3.70 % (2344058)lrs+10_64_to=lpo:sil=8000:random_seed=2893143432:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 21.36/3.70 % (2344057)Refutation not found, incomplete strategy
% 21.36/3.70 % (2344057)------------------------------
% 21.36/3.70 % (2344057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.36/3.70 % (2344057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.36/3.70 % (2344057)CaDiCaL version: 2.1.3
% 21.36/3.70 % (2344057)Termination reason: Refutation not found, incomplete strategy
% 21.36/3.70 % (2344057)Time elapsed: 0.002 s
% 21.36/3.70 % (2344057)Peak memory usage: 88 MB
% 21.36/3.70 % (2344057)Instructions burned: 2 (million)
% 21.36/3.70 % (2344054)------------------------------
% 21.36/3.70 % (2344054)------------------------------
% 21.36/3.70 % (2344058)Instruction limit reached!
% 21.36/3.70 % (2344058)------------------------------
% 21.36/3.70 % (2344058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.36/3.70 % (2344058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.36/3.70 % (2344058)CaDiCaL version: 2.1.3
% 21.36/3.70 % (2344058)Termination reason: Instruction limit
% 21.36/3.70 % (2344058)Termination phase: Saturation
% 21.36/3.70 % (2344058)Time elapsed: 0.070 s
% 21.36/3.70 % (2344058)Peak memory usage: 88 MB
% 21.36/3.70 % (2344058)Instructions burned: 126 (million)
% 21.36/3.70 % (2344055)------------------------------
% 21.36/3.70 % (2344055)------------------------------
% 21.36/3.70 % (2344063)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3161603834:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 21.36/3.70 % (2344062)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1128139283:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 21.36/3.70 % (2344057)------------------------------
% 21.36/3.70 % (2344057)------------------------------
% 21.36/3.70 % (2344064)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3507317162:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 21.36/3.70 % (2344063)Instruction limit reached!
% 21.36/3.70 % (2344063)------------------------------
% 21.36/3.70 % (2344063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.36/3.70 % (2344063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.36/3.70 % (2344063)CaDiCaL version: 2.1.3
% 21.36/3.70 % (2344063)Termination reason: Instruction limit
% 21.36/3.70 % (2344063)Termination phase: Saturation
% 21.36/3.70 % (2344063)Time elapsed: 0.081 s
% 21.36/3.70 % (2344063)Peak memory usage: 89 MB
% 21.36/3.70 % (2344063)Instructions burned: 159 (million)
% 21.36/3.70 % (2344062)Instruction limit reached!
% 21.36/3.70 % (2344062)------------------------------
% 21.36/3.70 % (2344062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.36/3.70 % (2344062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.36/3.70 % (2344062)CaDiCaL version: 2.1.3
% 21.36/3.70 % (2344062)Termination reason: Instruction limit
% 21.36/3.70 % (2344062)Termination phase: Saturation
% 21.36/3.70 % (2344062)Time elapsed: 0.084 s
% 21.36/3.70 % (2344062)Peak memory usage: 88 MB
% 21.36/3.70 % (2344062)Instructions burned: 196 (million)
% 21.36/3.70 % (2344067)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=461840702:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 31.91/5.19 % (2344067)Refutation not found, incomplete strategy
% 31.91/5.19 % (2344067)------------------------------
% 31.91/5.19 % (2344067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.91/5.19 % (2344067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.91/5.19 % (2344067)CaDiCaL version: 2.1.3
% 31.91/5.19 % (2344067)Termination reason: Refutation not found, incomplete strategy
% 31.91/5.19 % (2344067)Time elapsed: 0.005 s
% 31.91/5.19 % (2344067)Peak memory usage: 89 MB
% 31.91/5.19 % (2344067)Instructions burned: 6 (million)
% 31.91/5.19 % (2344069)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1164872027:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 31.91/5.19 % (2344070)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2252867734:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 31.91/5.19 % (2344069)Instruction limit reached!
% 31.91/5.19 % (2344069)------------------------------
% 31.91/5.19 % (2344069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.91/5.19 % (2344069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.91/5.19 % (2344069)CaDiCaL version: 2.1.3
% 31.91/5.19 % (2344069)Termination reason: Instruction limit
% 31.91/5.19 % (2344069)Termination phase: Saturation
% 31.91/5.19 % (2344069)Time elapsed: 0.057 s
% 31.91/5.19 % (2344069)Peak memory usage: 88 MB
% 31.91/5.19 % (2344069)Instructions burned: 108 (million)
% 31.91/5.19 % (2344070)Instruction limit reached!
% 31.91/5.19 % (2344070)------------------------------
% 31.91/5.19 % (2344070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.91/5.19 % (2344070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.91/5.19 % (2344070)CaDiCaL version: 2.1.3
% 31.91/5.19 % (2344070)Termination reason: Instruction limit
% 31.91/5.19 % (2344070)Termination phase: Saturation
% 31.91/5.19 % (2344070)Time elapsed: 0.109 s
% 31.91/5.19 % (2344070)Peak memory usage: 87 MB
% 31.91/5.19 % (2344070)Instructions burned: 242 (million)
% 31.91/5.19 % (2344067)------------------------------
% 31.91/5.19 % (2344067)------------------------------
% 31.91/5.19 % (2344074)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1597338394:cond=fast:i=5208:av=off_2988 on theBenchmark for (2988ds/5208Mi)
% 31.91/5.19 % (2344075)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=466222476:i=134:sd=2:doe=on:ss=axioms:sgt=14_2988 on theBenchmark for (2988ds/134Mi)
% 31.91/5.19 % (2344076)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2114353660:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 31.91/5.19 % (2344075)Instruction limit reached!
% 31.91/5.19 % (2344075)------------------------------
% 31.91/5.19 % (2344075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.91/5.19 % (2344075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.91/5.19 % (2344075)CaDiCaL version: 2.1.3
% 31.91/5.19 % (2344075)Termination reason: Instruction limit
% 31.91/5.19 % (2344075)Termination phase: Saturation
% 31.91/5.19 % (2344075)Time elapsed: 0.089 s
% 31.91/5.19 % (2344075)Peak memory usage: 89 MB
% 31.91/5.19 % (2344075)Instructions burned: 135 (million)
% 31.91/5.19 % (2344080)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3266048807:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 31.91/5.19 % (2344076)Instruction limit reached!
% 31.91/5.19 % (2344076)------------------------------
% 31.91/5.19 % (2344076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.91/5.19 % (2344076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.91/5.19 % (2344076)CaDiCaL version: 2.1.3
% 31.91/5.19 % (2344076)Termination reason: Instruction limit
% 31.91/5.19 % (2344076)Termination phase: Saturation
% 31.91/5.19 % (2344076)Time elapsed: 0.261 s
% 31.91/5.19 % (2344076)Peak memory usage: 89 MB
% 31.91/5.19 % (2344076)Instructions burned: 499 (million)
% 31.91/5.19 % (2344080)Instruction limit reached!
% 31.91/5.19 % (2344080)------------------------------
% 31.91/5.19 % (2344080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.91/5.19 % (2344080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.72/6.54 % (2344080)CaDiCaL version: 2.1.3
% 41.72/6.54 % (2344080)Termination reason: Instruction limit
% 41.72/6.54 % (2344080)Termination phase: Saturation
% 41.72/6.54 % (2344080)Time elapsed: 0.108 s
% 41.72/6.54 % (2344080)Peak memory usage: 89 MB
% 41.72/6.54 % (2344080)Instructions burned: 192 (million)
% 41.72/6.54 % (2344082)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4226972915:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 41.72/6.54 % (2344083)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2439987919:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 41.72/6.54 % (2344083)Instruction limit reached!
% 41.72/6.54 % (2344083)------------------------------
% 41.72/6.54 % (2344083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.72/6.54 % (2344083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.72/6.54 % (2344083)CaDiCaL version: 2.1.3
% 41.72/6.54 % (2344083)Termination reason: Instruction limit
% 41.72/6.54 % (2344083)Termination phase: Saturation
% 41.72/6.54 % (2344083)Time elapsed: 0.090 s
% 41.72/6.54 % (2344083)Peak memory usage: 89 MB
% 41.72/6.54 % (2344083)Instructions burned: 158 (million)
% 41.72/6.54 % (2344082)Instruction limit reached!
% 41.72/6.54 % (2344082)------------------------------
% 41.72/6.54 % (2344082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.72/6.54 % (2344082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.72/6.54 % (2344082)CaDiCaL version: 2.1.3
% 41.72/6.54 % (2344082)Termination reason: Instruction limit
% 41.72/6.54 % (2344082)Termination phase: Saturation
% 41.72/6.54 % (2344082)Time elapsed: 0.165 s
% 41.72/6.54 % (2344082)Peak memory usage: 90 MB
% 41.72/6.54 % (2344082)Instructions burned: 264 (million)
% 41.72/6.54 % (2344086)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=2519811973:i=3256:kws=precedence:bd=preordered:av=off_2980 on theBenchmark for (2980ds/3256Mi)
% 41.72/6.54 % (2344087)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=508177547:i=537:av=off:ss=included_2980 on theBenchmark for (2980ds/537Mi)
% 41.72/6.54 % (2344087)Instruction limit reached!
% 41.72/6.54 % (2344087)------------------------------
% 41.72/6.54 % (2344087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.72/6.54 % (2344087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.72/6.54 % (2344087)CaDiCaL version: 2.1.3
% 41.72/6.54 % (2344087)Termination reason: Instruction limit
% 41.72/6.54 % (2344087)Termination phase: Saturation
% 41.72/6.54 % (2344087)Time elapsed: 0.245 s
% 41.72/6.54 % (2344087)Peak memory usage: 88 MB
% 41.72/6.54 % (2344087)Instructions burned: 538 (million)
% 41.72/6.54 % (2344090)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3763241542:i=180:bd=preordered:av=off_2976 on theBenchmark for (2976ds/180Mi)
% 41.72/6.54 % (2344090)Instruction limit reached!
% 41.72/6.54 % (2344090)------------------------------
% 41.72/6.54 % (2344090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.72/6.54 % (2344090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.72/6.54 % (2344090)CaDiCaL version: 2.1.3
% 41.72/6.54 % (2344090)Termination reason: Instruction limit
% 41.72/6.54 % (2344090)Termination phase: Saturation
% 41.72/6.54 % (2344090)Time elapsed: 0.101 s
% 41.72/6.54 % (2344090)Peak memory usage: 88 MB
% 41.72/6.54 % (2344090)Instructions burned: 181 (million)
% 41.72/6.54 % (2344092)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=3369609260:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2973 on theBenchmark for (2973ds/10307Mi)
% 41.72/6.54 % (2344064)Instruction limit reached!
% 41.72/6.54 % (2344064)------------------------------
% 41.72/6.54 % (2344064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.72/6.54 % (2344064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.72/6.54 % (2344064)CaDiCaL version: 2.1.3
% 41.72/6.54 % (2344064)Termination reason: Instruction limit
% 41.72/6.54 % (2344064)Termination phase: Saturation
% 41.72/6.54 % (2344064)Time elapsed: 2.030 s
% 41.72/6.54 % (2344064)Peak memory usage: 140 MB
% 41.72/6.54 % (2344064)Instructions burned: 3394 (million)
% 41.72/6.54 % (2344094)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=3451306983:i=412:gtgl=4:gtg=exists_all_2971 on theBenchmark for (2971ds/412Mi)
% 41.72/6.54 % (2344094)Instruction limit reached!
% 41.72/6.54 % (2344094)------------------------------
% 41.72/6.54 % (2344094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.72/6.54 % (2344094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.72/6.54 % (2344094)CaDiCaL version: 2.1.3
% 41.72/6.54 % (2344094)Termination reason: Instruction limit
% 41.72/6.54 % (2344094)Termination phase: Saturation
% 41.72/6.54 % (2344094)Time elapsed: 0.176 s
% 41.72/6.54 % (2344094)Peak memory usage: 89 MB
% 41.72/6.54 % (2344094)Instructions burned: 414 (million)
% 41.72/6.54 % (2344096)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=147281842:s2pl=no:i=8478:s2at=4:nm=6_2967 on theBenchmark for (2967ds/8478Mi)
% 41.72/6.54 % (2344086)Instruction limit reached!
% 41.72/6.54 % (2344086)------------------------------
% 41.72/6.54 % (2344086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.72/6.54 % (2344086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.72/6.54 % (2344086)CaDiCaL version: 2.1.3
% 41.72/6.54 % (2344086)Termination reason: Instruction limit
% 41.72/6.54 % (2344086)Termination phase: Saturation
% 41.72/6.54 % (2344086)Time elapsed: 1.864 s
% 41.72/6.54 % (2344086)Peak memory usage: 139 MB
% 41.72/6.54 % (2344086)Instructions burned: 3258 (million)
% 41.72/6.54 % (2344074)Instruction limit reached!
% 41.72/6.54 % (2344074)------------------------------
% 41.72/6.54 % (2344074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.72/6.54 % (2344074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.72/6.54 % (2344074)CaDiCaL version: 2.1.3
% 41.72/6.54 % (2344074)Termination reason: Instruction limit
% 41.72/6.54 % (2344074)Termination phase: Saturation
% 41.72/6.54 % (2344074)Time elapsed: 2.750 s
% 41.72/6.54 % (2344074)Peak memory usage: 138 MB
% 41.72/6.54 % (2344074)Instructions burned: 5209 (million)
% 41.72/6.54 % (2344099)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=2247698880:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2960 on theBenchmark for (2960ds/303Mi)
% 41.72/6.54 % (2344099)Refutation not found, incomplete strategy
% 41.72/6.54 % (2344099)------------------------------
% 41.72/6.54 % (2344099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.72/6.54 % (2344099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.72/6.54 % (2344099)CaDiCaL version: 2.1.3
% 41.72/6.54 % (2344099)Termination reason: Refutation not found, incomplete strategy
% 41.72/6.54 % (2344099)Time elapsed: 0.003 s
% 41.72/6.54 % (2344099)Peak memory usage: 88 MB
% 41.72/6.54 % (2344099)Instructions burned: 3 (million)
% 41.72/6.54 % (2344100)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=763980483:st=4:i=720:sd=3:fsr=off:ss=axioms_2959 on theBenchmark for (2959ds/720Mi)
% 41.72/6.54 % (2344100)Refutation not found, incomplete strategy
% 41.72/6.54 % (2344100)------------------------------
% 41.72/6.54 % (2344100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.72/6.54 % (2344100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.72/6.54 % (2344100)CaDiCaL version: 2.1.3
% 41.72/6.54 % (2344100)Termination reason: Refutation not found, incomplete strategy
% 41.72/6.54 % (2344100)Time elapsed: 0.002 s
% 41.72/6.54 % (2344100)Peak memory usage: 88 MB
% 41.72/6.54 % (2344100)Instructions burned: 2 (million)
% 41.72/6.54 % (2344099)------------------------------
% 41.72/6.54 % (2344099)------------------------------
% 41.72/6.54 % (2344100)------------------------------
% 41.72/6.54 % (2344100)------------------------------
% 41.72/6.54 % (2344103)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1275742305:i=598:bs=on:bd=preordered:av=off:ss=axioms_2956 on theBenchmark for (2956ds/598Mi)
% 41.72/6.54 % (2344103)Refutation not found, incomplete strategy
% 41.72/6.54 % (2344103)------------------------------
% 41.72/6.54 % (2344103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.72/6.54 % (2344103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.72/6.54 % (2344103)CaDiCaL version: 2.1.3
% 41.72/6.54 % (2344103)Termination reason: Refutation not found, incomplete strategy
% 41.72/6.54 % (2344103)Time elapsed: 0.029 s
% 41.72/6.54 % (2344103)Peak memory usage: 88 MB
% 41.72/6.54 % (2344103)Instructions burned: 53 (million)
% 41.72/6.54 % (2344104)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=233908879:i=2989:sd=3:ss=axioms:sgt=60_2955 on theBenchmark for (2955ds/2989Mi)
% 41.72/6.54 % (2344103)------------------------------
% 41.72/6.54 % (2344103)------------------------------
% 41.72/6.54 % (2344107)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=461027016:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2952 on theBenchmark for (2952ds/1997Mi)
% 41.72/6.54 % (2344104)First to succeed.
% 41.72/6.54 % (2344104)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2344035"
% 41.72/6.54 % (2344104)Refutation found. Thanks to Tanya!
% 41.72/6.54 % SZS status Unsatisfiable for theBenchmark
% 41.72/6.54 % SZS output start Proof for theBenchmark
% See solution above
% 42.21/6.74 % (2344104)------------------------------
% 42.21/6.74 % (2344104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.21/6.74 % (2344104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.21/6.74 % (2344104)CaDiCaL version: 2.1.3
% 42.21/6.74 % (2344104)Termination reason: Refutation
% 42.21/6.74 % (2344104)Time elapsed: 1.026 s
% 42.21/6.74 % (2344104)Peak memory usage: 132 MB
% 42.21/6.74 % (2344104)Instructions burned: 1457 (million)
% 42.21/6.74 % (2344104)------------------------------
% 42.21/6.74 % (2344104)------------------------------
% 42.21/6.74 % (2344035)Success in time 5.87 s
% 42.21/6.74 % Vampire exiting
%------------------------------------------------------------------------------