%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : SET837-2 : TPTP v3.4.2. Released v3.2.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art09.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1003MB
% OS : Linux 2.6.11-1.1369_FC4
% CPULimit : 600s
% Result : Unsatisfiable 30.0s
% Output : Assurance 30.0s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----NO SOLUTION OUTPUT BY SYSTEM
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
%
% Gandalf c-2.6 r1 starting to prove: /tmp/SystemOnTPTP7098/SET/SET837-2+eq_r.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: neq
% detected subclass: medium
%
% strategies selected:
% (hyper 25 #f 2 7)
% (binary-unit 9 #f 2 7)
% (binary-double 9 #f 2 7)
% (binary-double 15 #f)
% (binary-double 15 #t)
% (binary 50 #t 2 7)
% (binary-order 25 #f 2 7)
% (binary-posweight-order 101 #f)
% (binary-posweight-lex-big-order 25 #f)
% (binary-posweight-lex-small-order 9 #f)
% (binary-order-sos 50 #t)
% (binary-unit-uniteq 25 #f)
% (binary-weightorder 50 #f)
% (binary-order 50 #f)
% (hyper-order 30 #f)
% (binary 112 #t)
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(14,40,0,28,0,0,41950,5,2506,41950,1,2506,41950,50,2507,41950,40,2507,41964,0,2507,41978,50,2507,41992,0,2507,42006,50,2507,42020,0,2509,42034,50,2509,42048,0,2509,42062,50,2509,42076,0,2509,42090,50,2509,42104,0,2511,42118,50,2511,42132,0,2511,42146,50,2511,42160,0,2512,42174,50,2512,42188,0,2512,42202,50,2512,42216,0,2512,42230,50,2512,42244,0,2514,42258,50,2514,42272,0,2514,42286,50,2514,42300,0,2515,42314,50,2515,42328,0,2515,42342,50,2515,42356,0,2515,42370,50,2515,42384,0,2517,42398,50,2517,42412,0,2517,42426,50,2517,42440,0,2518,42454,50,2518,42468,0,2518,42482,50,2518,42496,0,2519,42510,50,2519,42510,40,2519,42524,0,2520,60047,3,2971)
%
%
% START OF PROOF
% 42511 [] equal(X,X).
% 42512 [] c_in(X,c_union(Y,Z,U),U) | -c_in(X,Z,U).
% 42513 [] c_in(X,c_union(Y,Z,U),U) | -c_in(X,Y,U).
% 42514 [] -c_in(X,c_union(Y,Z,U),U) | c_in(X,Z,U) | c_in(X,Y,U).
% 42515 [] -c_lessequals(X,Y,tc_set(Z)) | -c_in(U,X,Z) | c_in(U,Y,Z).
% 42516 [] c_in(c_^main_^osubset^i__1(X,Y,Z),X,Z) | c_lessequals(X,Y,tc_set(Z)).
% 42517 [] -c_in(c_^main_^osubset^i__1(X,Y,Z),Y,Z) | c_lessequals(X,Y,tc_set(Z)).
% 42518 [] -c_lessequals(Y,X,tc_set(Z)) | -c_lessequals(X,Y,tc_set(Z)) | equal(Y,X).
% 42519 [] equal(v_^x,c_union(v_^y,v_^z,t_a)) | c_lessequals(v_^y,v_^x,tc_set(t_a)).
% 42520 [] equal(v_^x,c_union(v_^y,v_^z,t_a)) | c_lessequals(v_^z,v_^x,tc_set(t_a)).
% 42521 [] -equal(v_^x,c_union(v_^y,v_^z,t_a)) | -c_lessequals(v_^y,v_^x,tc_set(t_a)) | -c_lessequals(v_^z,v_^x,tc_set(t_a)) | c_lessequals(v_^y,v_x,tc_set(t_a)).
% 42522 [] -equal(v_^x,c_union(v_^y,v_^z,t_a)) | -c_lessequals(v_^y,v_^x,tc_set(t_a)) | -c_lessequals(v_^z,v_^x,tc_set(t_a)) | c_lessequals(v_^z,v_x,tc_set(t_a)).
% 42523 [?] ?
% 42524 [] equal(v_^x,c_union(v_^y,v_^z,t_a)) | -c_lessequals(v_^z,X,tc_set(t_a)) | -c_lessequals(v_^y,X,tc_set(t_a)) | c_lessequals(v_^x,X,tc_set(t_a)).
% 42530 [para:42519.1.2,42513.1.2] c_lessequals(v_^y,v_^x,tc_set(t_a)) | -c_in(X,v_^y,t_a) | c_in(X,v_^x,t_a).
% 42532 [para:42520.1.2,42512.1.2] c_lessequals(v_^z,v_^x,tc_set(t_a)) | -c_in(X,v_^z,t_a) | c_in(X,v_^x,t_a).
% 42536 [binary:42512.2,42516] c_in(c_^main_^osubset^i__1(X,Y,Z),c_union(U,X,Z),Z) | c_lessequals(X,Y,tc_set(Z)).
% 42537 [binary:42513.2,42516] c_in(c_^main_^osubset^i__1(X,Y,Z),c_union(X,U,Z),Z) | c_lessequals(X,Y,tc_set(Z)).
% 42543 [binary:42516,42517] c_lessequals(X,X,tc_set(Y)).
% 42546 [binary:42512.2,42515.3] c_in(X,c_union(Y,Z,U),U) | -c_lessequals(V,Z,tc_set(U)) | -c_in(X,V,U).
% 42587 [binary:42516,42530.2,factor:binarycut:42517] c_lessequals(v_^y,v_^x,tc_set(t_a)).
% 42589 [binary:42515,42587] -c_in(X,v_^y,t_a) | c_in(X,v_^x,t_a).
% 42600 [input:42523,cut:42587] -equal(v_^x,c_union(v_^y,v_^z,t_a)) | -c_lessequals(v_^x,v_x,tc_set(t_a)) | -c_lessequals(v_^z,v_^x,tc_set(t_a)).
% 42624 [binary:42516,42532.2,factor:binarycut:42517] c_lessequals(v_^z,v_^x,tc_set(t_a)).
% 42625 [binary:42515,42624] -c_in(X,v_^z,t_a) | c_in(X,v_^x,t_a).
% 42628 [binary:42600.3,42624] -equal(v_^x,c_union(v_^y,v_^z,t_a)) | -c_lessequals(v_^x,v_x,tc_set(t_a)).
% 42666 [binary:42513.2,42514.2] -c_in(X,c_union(Y,Z,U),U) | c_in(X,c_union(Z,V,U),U) | c_in(X,Y,U).
% 42668 [binary:42517,42514.2] -c_in(c_^main_^osubset^i__1(X,Y,Z),c_union(U,Y,Z),Z) | c_in(c_^main_^osubset^i__1(X,Y,Z),U,Z) | c_lessequals(X,Y,tc_set(Z)).
% 42672 [binary:42589,42514.3] -c_in(X,c_union(v_^y,Y,t_a),t_a) | c_in(X,v_^x,t_a) | c_in(X,Y,t_a).
% 42690 [binary:42516.2,42628.2] c_in(c_^main_^osubset^i__1(v_^x,v_x,t_a),v_^x,t_a) | -equal(v_^x,c_union(v_^y,v_^z,t_a)).
% 42691 [binary:42517.2,42628.2] -c_in(c_^main_^osubset^i__1(v_^x,v_x,t_a),v_x,t_a) | -equal(v_^x,c_union(v_^y,v_^z,t_a)).
% 42692 [binary:42518.3,42628] -c_lessequals(v_^x,v_x,tc_set(t_a)) | -c_lessequals(c_union(v_^y,v_^z,t_a),v_^x,tc_set(X)) | -c_lessequals(v_^x,c_union(v_^y,v_^z,t_a),tc_set(X)).
% 42726 [binary:42517,42536] c_lessequals(X,c_union(Y,X,Z),tc_set(Z)).
% 42736 [binary:42524.2,42726] equal(v_^x,c_union(v_^y,v_^z,t_a)) | -c_lessequals(v_^y,c_union(X,v_^z,t_a),tc_set(t_a)) | c_lessequals(v_^x,c_union(X,v_^z,t_a),tc_set(t_a)).
% 42739 [binary:42517,42537] c_lessequals(X,c_union(X,Y,Z),tc_set(Z)).
% 42753 [binary:42518.3,42690.2] c_in(c_^main_^osubset^i__1(v_^x,v_x,t_a),v_^x,t_a) | -c_lessequals(c_union(v_^y,v_^z,t_a),v_^x,tc_set(X)) | -c_lessequals(v_^x,c_union(v_^y,v_^z,t_a),tc_set(X)).
% 44982 [binary:42625,42672.3] -c_in(X,c_union(v_^y,v_^z,t_a),t_a) | c_in(X,v_^x,t_a).
% 44986 [binary:42517,44982.2] -c_in(c_^main_^osubset^i__1(X,v_^x,t_a),c_union(v_^y,v_^z,t_a),t_a) | c_lessequals(X,v_^x,tc_set(t_a)).
% 45022 [binary:42521.2,42587,cut:42624] -equal(v_^x,c_union(v_^y,v_^z,t_a)) | c_lessequals(v_^y,v_x,tc_set(t_a)).
% 45139 [binary:42522.2,42587,cut:42624] -equal(v_^x,c_union(v_^y,v_^z,t_a)) | c_lessequals(v_^z,v_x,tc_set(t_a)).
% 45140 [binary:42515,45139.2] -equal(v_^x,c_union(v_^y,v_^z,t_a)) | -c_in(X,v_^z,t_a) | c_in(X,v_x,t_a).
% 45502 [binary:42691,45140.3] -c_in(c_^main_^osubset^i__1(v_^x,v_x,t_a),v_^z,t_a) | -equal(v_^x,c_union(v_^y,v_^z,t_a)).
% 55889 [binary:42739,42736.2] c_lessequals(v_^x,c_union(v_^y,v_^z,t_a),tc_set(t_a)) | equal(v_^x,c_union(v_^y,v_^z,t_a)).
% 55918 [binary:42518,55889] -c_lessequals(c_union(v_^y,v_^z,t_a),v_^x,tc_set(t_a)) | equal(v_^x,c_union(v_^y,v_^z,t_a)).
% 56342 [para:55918.2.2,45022.1.2,cut:42511] -c_lessequals(c_union(v_^y,v_^z,t_a),v_^x,tc_set(t_a)) | c_lessequals(v_^y,v_x,tc_set(t_a)).
% 61605 [binary:42516,44986] c_lessequals(c_union(v_^y,v_^z,t_a),v_^x,tc_set(t_a)).
% 61626 [binary:42518.2,61605,binarycut:55889] equal(v_^x,c_union(v_^y,v_^z,t_a)).
% 61627 [binary:42692.2,61605,demod:61626,cut:42543] -c_lessequals(v_^x,v_x,tc_set(t_a)).
% 61628 [binary:56342,61605] c_lessequals(v_^y,v_x,tc_set(t_a)).
% 61630 [binary:42753.2,61605,demod:61626,cut:42543] c_in(c_^main_^osubset^i__1(v_^x,v_x,t_a),v_^x,t_a).
% 61645 [binary:42546.2,61628] c_in(X,c_union(Y,v_x,t_a),t_a) | -c_in(X,v_^y,t_a).
% 61673 [binary:45502.2,61626] -c_in(c_^main_^osubset^i__1(v_^x,v_x,t_a),v_^z,t_a).
% 61716 [binary:42668.2,61673,cut:61627] -c_in(c_^main_^osubset^i__1(v_^x,v_x,t_a),c_union(v_^z,v_x,t_a),t_a).
% 62004 [binary:42666.3,61645.2,factor] -c_in(X,c_union(v_^y,Y,t_a),t_a) | c_in(X,c_union(Y,v_x,t_a),t_a).
% 63800 [binary:61716,62004.2,demod:61626,cut:61630] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% not using sos strategy
% using unit paramodulation strategy
% using unit strategy
% using double strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% clause length limited to 7
% clause depth limited to 2
% seconds given: 9
%
%
% old unit clauses discarded
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 1305
% derived clauses: 311675
% kept clauses: 37631
% kept size sum: 0
% kept mid-nuclei: 22075
% kept new demods: 6
% forw unit-subs: 30187
% forw double-subs: 41496
% forw overdouble-subs: 123433
% backward subs: 607
% fast unit cutoff: 4108
% full unit cutoff: 22
% dbl unit cutoff: 252
% real runtime : 32.14
% process. runtime: 32.10
% specific non-discr-tree subsumption statistics:
% tried: 12627239
% length fails: 2279218
% strength fails: 2871939
% predlist fails: 1951445
% aux str. fails: 24770
% by-lit fails: 780748
% full subs tried: 4381136
% full subs fail: 4268515
%
% ; program args: ("/home/graph/tptp/Systems/Gandalf---c-2.6/gandalf" "-time" "600" "/tmp/SystemOnTPTP7098/SET/SET837-2+eq_r.in")
% WARNING: TreeLimitedRun lost 29.97s, total lost is 29.97s
%
%------------------------------------------------------------------------------