%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LAT274-2 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:29:34 EDT 2024
% Result : Unsatisfiable 16.45s 16.66s
% Output : Refutation 16.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 15
% Syntax : Number of clauses : 52 ( 13 unt; 29 nHn; 39 RR)
% Number of literals : 136 ( 17 equ; 39 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-4 aty)
% Number of variables : 68 ( 10 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_conjecture_6,negated_conjecture,
~ c_in(v_L,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_6) ).
cnf(cls_conjecture_1,negated_conjecture,
c_in(v_b,v_A,t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
cnf(cls_conjecture_4,negated_conjecture,
c_Tarski_OisLub(v_S,v_cl,v_L,t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
cnf(cls_Tarski_O_91_124_AisLub_AS1_Acl_AL1_59_Az1_A_58_AA_59_AALL_Ay_58S1_O_A_Iy_M_Az1_J_A_58_Ar_A_124_93_A_61_61_62_A_IL1_M_Az1_J_A_58_Ar_A_61_61_ATrue_1,axiom,
( ~ c_Tarski_OisLub(X163,v_cl,X164,t_a)
| ~ c_in(X162,v_A,t_a)
| ~ c_in(c_Pair(v_sko__4mi(X163,v_r,X162),X162,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(c_Pair(X164,X162,t_a,t_a),v_r,tc_prod(t_a,t_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_O_91_124_AisLub_AS1_Acl_AL1_59_Az1_A_58_AA_59_AALL_Ay_58S1_O_A_Iy_M_Az1_J_A_58_Ar_A_124_93_A_61_61_62_A_IL1_M_Az1_J_A_58_Ar_A_61_61_ATrue_1) ).
cnf(cls_conjecture_2,negated_conjecture,
c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
cnf(cls_Tarski_O_91_124_AS1_A_60_61_Ainterval_Ar_Aa1_Ab1_59_Ax1_A_58_AS1_A_124_93_A_61_61_62_A_Ix1_M_Ab1_J_A_58_Ar_A_61_61_ATrue_0,axiom,
( ~ c_in(X85,X88,X90)
| ~ c_lessequals(X88,c_Tarski_Ointerval(X89,X87,X86,X90),tc_set(X90))
| c_in(c_Pair(X85,X86,X90,X90),X89,tc_prod(X90,X90)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_O_91_124_AS1_A_60_61_Ainterval_Ar_Aa1_Ab1_59_Ax1_A_58_AS1_A_124_93_A_61_61_62_A_Ix1_M_Ab1_J_A_58_Ar_A_61_61_ATrue_0) ).
cnf(c32,plain,
( ~ c_in(X255,v_S,t_a)
| c_in(c_Pair(X255,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a)) ),
inference(resolution,[status(thm)],[cls_Tarski_O_91_124_AS1_A_60_61_Ainterval_Ar_Aa1_Ab1_59_Ax1_A_58_AS1_A_124_93_A_61_61_62_A_Ix1_M_Ab1_J_A_58_Ar_A_61_61_ATrue_0,cls_conjecture_2]) ).
cnf(cls_Tarski_O_91_124_AisLub_AS1_Acl_AL1_59_Az1_A_58_AA_59_AALL_Ay_58S1_O_A_Iy_M_Az1_J_A_58_Ar_A_124_93_A_61_61_62_A_IL1_M_Az1_J_A_58_Ar_A_61_61_ATrue_0,axiom,
( ~ c_Tarski_OisLub(X147,v_cl,X148,t_a)
| ~ c_in(X146,v_A,t_a)
| c_in(c_Pair(X148,X146,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_sko__4mi(X147,v_r,X146),X147,t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_O_91_124_AisLub_AS1_Acl_AL1_59_Az1_A_58_AA_59_AALL_Ay_58S1_O_A_Iy_M_Az1_J_A_58_Ar_A_124_93_A_61_61_62_A_IL1_M_Az1_J_A_58_Ar_A_61_61_ATrue_0) ).
cnf(c49,plain,
( ~ c_in(X282,v_A,t_a)
| c_in(c_Pair(v_L,X282,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_sko__4mi(v_S,v_r,X282),v_S,t_a) ),
inference(resolution,[status(thm)],[cls_Tarski_O_91_124_AisLub_AS1_Acl_AL1_59_Az1_A_58_AA_59_AALL_Ay_58S1_O_A_Iy_M_Az1_J_A_58_Ar_A_124_93_A_61_61_62_A_IL1_M_Az1_J_A_58_Ar_A_61_61_ATrue_0,cls_conjecture_4]) ).
cnf(c143,plain,
( c_in(c_Pair(v_L,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_sko__4mi(v_S,v_r,v_b),v_S,t_a) ),
inference(resolution,[status(thm)],[c49,cls_conjecture_1]) ).
cnf(c493,plain,
( c_in(c_Pair(v_L,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(c_Pair(v_sko__4mi(v_S,v_r,v_b),v_b,t_a,t_a),v_r,tc_prod(t_a,t_a)) ),
inference(resolution,[status(thm)],[c143,c32]) ).
cnf(c542,plain,
( c_in(c_Pair(v_L,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a))
| ~ c_Tarski_OisLub(v_S,v_cl,X923,t_a)
| ~ c_in(v_b,v_A,t_a)
| c_in(c_Pair(X923,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a)) ),
inference(resolution,[status(thm)],[c493,cls_Tarski_O_91_124_AisLub_AS1_Acl_AL1_59_Az1_A_58_AA_59_AALL_Ay_58S1_O_A_Iy_M_Az1_J_A_58_Ar_A_124_93_A_61_61_62_A_IL1_M_Az1_J_A_58_Ar_A_61_61_ATrue_1]) ).
cnf(c758,plain,
( c_in(c_Pair(v_L,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a))
| ~ c_in(v_b,v_A,t_a) ),
inference(resolution,[status(thm)],[c542,cls_conjecture_4]) ).
cnf(c759,plain,
c_in(c_Pair(v_L,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a)),
inference(resolution,[status(thm)],[c758,cls_conjecture_1]) ).
cnf(cls_Tarski_O_91_124_A_Ia1_M_Ax1_J_A_58_Ar_59_A_Ix1_M_Ab1_J_A_58_Ar_A_124_93_A_61_61_62_Ax1_A_58_Ainterval_Ar_Aa1_Ab1_A_61_61_ATrue_0,axiom,
( ~ c_in(c_Pair(X107,X108,X111,X111),X110,tc_prod(X111,X111))
| ~ c_in(c_Pair(X109,X107,X111,X111),X110,tc_prod(X111,X111))
| c_in(X107,c_Tarski_Ointerval(X110,X109,X108,X111),X111) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_O_91_124_A_Ia1_M_Ax1_J_A_58_Ar_59_A_Ix1_M_Ab1_J_A_58_Ar_A_124_93_A_61_61_62_Ax1_A_58_Ainterval_Ar_Aa1_Ab1_A_61_61_ATrue_0) ).
cnf(cls_conjecture_3,negated_conjecture,
v_S != c_emptyset,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
cnf(cls_Tarski_O_91_124_AS1_A_60_61_Ainterval_Ar_Aa1_Ab1_59_Ax1_A_58_AS1_A_124_93_A_61_61_62_A_Ia1_M_Ax1_J_A_58_Ar_A_61_61_ATrue_0,axiom,
( ~ c_in(X67,X70,X72)
| ~ c_lessequals(X70,c_Tarski_Ointerval(X71,X69,X68,X72),tc_set(X72))
| c_in(c_Pair(X69,X67,X72,X72),X71,tc_prod(X72,X72)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_O_91_124_AS1_A_60_61_Ainterval_Ar_Aa1_Ab1_59_Ax1_A_58_AS1_A_124_93_A_61_61_62_A_Ia1_M_Ax1_J_A_58_Ar_A_61_61_ATrue_0) ).
cnf(c27,plain,
( ~ c_in(X254,v_S,t_a)
| c_in(c_Pair(v_a,X254,t_a,t_a),v_r,tc_prod(t_a,t_a)) ),
inference(resolution,[status(thm)],[cls_Tarski_O_91_124_AS1_A_60_61_Ainterval_Ar_Aa1_Ab1_59_Ax1_A_58_AS1_A_124_93_A_61_61_62_A_Ia1_M_Ax1_J_A_58_Ar_A_61_61_ATrue_0,cls_conjecture_2]) ).
cnf(cls_Tarski_O_91_124_AS1_A_60_61_AA_59_AS1_A_126_61_A_123_125_59_AALL_Ax_58S1_O_A_Ia1_M_Ax_J_A_58_Ar_59_AALL_Ay_58S1_O_A_Iy_M_AL1_J_A_58_Ar_A_124_93_A_61_61_62_A_Ia1_M_AL1_J_A_58_Ar_A_61_61_ATrue_1,axiom,
( ~ c_in(c_Pair(v_sko__4mk(X21,X20,v_r),X21,t_a,t_a),v_r,tc_prod(t_a,t_a))
| ~ c_lessequals(X20,X18,tc_set(t_a))
| c_in(c_Pair(X19,X21,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_sko__4mj(X20,X19,v_r),X20,t_a)
| X20 = c_emptyset ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_O_91_124_AS1_A_60_61_AA_59_AS1_A_126_61_A_123_125_59_AALL_Ax_58S1_O_A_Ia1_M_Ax_J_A_58_Ar_59_AALL_Ay_58S1_O_A_Iy_M_AL1_J_A_58_Ar_A_124_93_A_61_61_62_A_Ia1_M_AL1_J_A_58_Ar_A_61_61_ATrue_1) ).
cnf(cls_Tarski_O_91_124_AisLub_AS1_Acl_AL1_59_Ay1_A_58_AS1_A_124_93_A_61_61_62_A_Iy1_M_AL1_J_A_58_Ar_A_61_61_ATrue_0,axiom,
( ~ c_Tarski_OisLub(X127,v_cl,X128,t_a)
| ~ c_in(X129,X127,t_a)
| c_in(c_Pair(X129,X128,t_a,t_a),v_r,tc_prod(t_a,t_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_O_91_124_AisLub_AS1_Acl_AL1_59_Ay1_A_58_AS1_A_124_93_A_61_61_62_A_Iy1_M_AL1_J_A_58_Ar_A_61_61_ATrue_0) ).
cnf(c41,plain,
( ~ c_in(X256,v_S,t_a)
| c_in(c_Pair(X256,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a)) ),
inference(resolution,[status(thm)],[cls_Tarski_O_91_124_AisLub_AS1_Acl_AL1_59_Ay1_A_58_AS1_A_124_93_A_61_61_62_A_Iy1_M_AL1_J_A_58_Ar_A_61_61_ATrue_0,cls_conjecture_4]) ).
cnf(cls_Tarski_O_91_124_AS1_A_60_61_AA_59_AS1_A_126_61_A_123_125_59_AALL_Ax_58S1_O_A_Ia1_M_Ax_J_A_58_Ar_59_AALL_Ay_58S1_O_A_Iy_M_AL1_J_A_58_Ar_A_124_93_A_61_61_62_A_Ia1_M_AL1_J_A_58_Ar_A_61_61_ATrue_2,axiom,
( ~ c_in(c_Pair(X30,v_sko__4mj(X31,X30,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))
| ~ c_lessequals(X31,X29,tc_set(t_a))
| c_in(c_Pair(X30,X32,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_sko__4mk(X32,X31,v_r),X31,t_a)
| X31 = c_emptyset ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_O_91_124_AS1_A_60_61_AA_59_AS1_A_126_61_A_123_125_59_AALL_Ax_58S1_O_A_Ia1_M_Ax_J_A_58_Ar_59_AALL_Ay_58S1_O_A_Iy_M_AL1_J_A_58_Ar_A_124_93_A_61_61_62_A_Ia1_M_AL1_J_A_58_Ar_A_61_61_ATrue_2) ).
cnf(cls_Tarski_O_91_124_AS1_A_60_61_AA_59_AS1_A_126_61_A_123_125_59_AALL_Ax_58S1_O_A_Ia1_M_Ax_J_A_58_Ar_59_AALL_Ay_58S1_O_A_Iy_M_AL1_J_A_58_Ar_A_124_93_A_61_61_62_A_Ia1_M_AL1_J_A_58_Ar_A_61_61_ATrue_0,axiom,
( ~ c_lessequals(X8,X6,tc_set(t_a))
| c_in(c_Pair(X7,X9,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_sko__4mj(X8,X7,v_r),X8,t_a)
| c_in(v_sko__4mk(X9,X8,v_r),X8,t_a)
| X8 = c_emptyset ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_O_91_124_AS1_A_60_61_AA_59_AS1_A_126_61_A_123_125_59_AALL_Ax_58S1_O_A_Ia1_M_Ax_J_A_58_Ar_59_AALL_Ay_58S1_O_A_Iy_M_AL1_J_A_58_Ar_A_124_93_A_61_61_62_A_Ia1_M_AL1_J_A_58_Ar_A_61_61_ATrue_0) ).
cnf(c14,plain,
( c_in(c_Pair(X252,X253,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_sko__4mj(v_S,X252,v_r),v_S,t_a)
| c_in(v_sko__4mk(X253,v_S,v_r),v_S,t_a)
| v_S = c_emptyset ),
inference(resolution,[status(thm)],[cls_conjecture_2,cls_Tarski_O_91_124_AS1_A_60_61_AA_59_AS1_A_126_61_A_123_125_59_AALL_Ax_58S1_O_A_Ia1_M_Ax_J_A_58_Ar_59_AALL_Ay_58S1_O_A_Iy_M_AL1_J_A_58_Ar_A_124_93_A_61_61_62_A_Ia1_M_AL1_J_A_58_Ar_A_61_61_ATrue_0]) ).
cnf(c85,plain,
( c_in(v_sko__4mj(v_S,X579,v_r),v_S,t_a)
| c_in(v_sko__4mk(X578,v_S,v_r),v_S,t_a)
| v_S = c_emptyset
| ~ c_in(c_Pair(X578,X580,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(X578,c_Tarski_Ointerval(v_r,X579,X580,t_a),t_a) ),
inference(resolution,[status(thm)],[c14,cls_Tarski_O_91_124_A_Ia1_M_Ax1_J_A_58_Ar_59_A_Ix1_M_Ab1_J_A_58_Ar_A_124_93_A_61_61_62_Ax1_A_58_Ainterval_Ar_Aa1_Ab1_A_61_61_ATrue_0]) ).
cnf(c762,plain,
( c_in(v_sko__4mj(v_S,X941,v_r),v_S,t_a)
| c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a)
| v_S = c_emptyset
| c_in(v_L,c_Tarski_Ointerval(v_r,X941,v_b,t_a),t_a) ),
inference(resolution,[status(thm)],[c759,c85]) ).
cnf(c873,plain,
( c_in(v_sko__4mj(v_S,v_a,v_r),v_S,t_a)
| c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a)
| v_S = c_emptyset ),
inference(resolution,[status(thm)],[c762,cls_conjecture_6]) ).
cnf(c941,plain,
( c_in(v_sko__4mj(v_S,v_a,v_r),v_S,t_a)
| c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a) ),
inference(resolution,[status(thm)],[c873,cls_conjecture_3]) ).
cnf(c966,plain,
( c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a)
| c_in(c_Pair(v_a,v_sko__4mj(v_S,v_a,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a)) ),
inference(resolution,[status(thm)],[c941,c27]) ).
cnf(c988,plain,
( c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a)
| ~ c_lessequals(v_S,X2380,tc_set(t_a))
| c_in(c_Pair(v_a,X2379,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_sko__4mk(X2379,v_S,v_r),v_S,t_a)
| v_S = c_emptyset ),
inference(resolution,[status(thm)],[c966,cls_Tarski_O_91_124_AS1_A_60_61_AA_59_AS1_A_126_61_A_123_125_59_AALL_Ax_58S1_O_A_Ia1_M_Ax_J_A_58_Ar_59_AALL_Ay_58S1_O_A_Iy_M_AL1_J_A_58_Ar_A_124_93_A_61_61_62_A_Ia1_M_AL1_J_A_58_Ar_A_61_61_ATrue_2]) ).
cnf(c2220,plain,
( c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a)
| c_in(c_Pair(v_a,X2381,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_sko__4mk(X2381,v_S,v_r),v_S,t_a)
| v_S = c_emptyset ),
inference(resolution,[status(thm)],[c988,cls_conjecture_2]) ).
cnf(c2221,plain,
( c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a)
| c_in(c_Pair(v_a,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))
| v_S = c_emptyset ),
inference(factor,[status(thm)],[c2220]) ).
cnf(c2423,plain,
( c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a)
| c_in(c_Pair(v_a,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a)) ),
inference(resolution,[status(thm)],[c2221,cls_conjecture_3]) ).
cnf(c2456,plain,
( c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a)
| ~ c_in(c_Pair(v_L,X2428,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_L,c_Tarski_Ointerval(v_r,v_a,X2428,t_a),t_a) ),
inference(resolution,[status(thm)],[c2423,cls_Tarski_O_91_124_A_Ia1_M_Ax1_J_A_58_Ar_59_A_Ix1_M_Ab1_J_A_58_Ar_A_124_93_A_61_61_62_Ax1_A_58_Ainterval_Ar_Aa1_Ab1_A_61_61_ATrue_0]) ).
cnf(c2514,plain,
( c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a)
| c_in(v_L,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),t_a) ),
inference(resolution,[status(thm)],[c2456,c759]) ).
cnf(c2526,plain,
c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a),
inference(resolution,[status(thm)],[c2514,cls_conjecture_6]) ).
cnf(c2527,plain,
c_in(c_Pair(v_sko__4mk(v_L,v_S,v_r),v_L,t_a,t_a),v_r,tc_prod(t_a,t_a)),
inference(resolution,[status(thm)],[c2526,c41]) ).
cnf(c2531,plain,
( ~ c_lessequals(v_S,X2527,tc_set(t_a))
| c_in(c_Pair(X2528,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_sko__4mj(v_S,X2528,v_r),v_S,t_a)
| v_S = c_emptyset ),
inference(resolution,[status(thm)],[c2527,cls_Tarski_O_91_124_AS1_A_60_61_AA_59_AS1_A_126_61_A_123_125_59_AALL_Ax_58S1_O_A_Ia1_M_Ax_J_A_58_Ar_59_AALL_Ay_58S1_O_A_Iy_M_AL1_J_A_58_Ar_A_124_93_A_61_61_62_A_Ia1_M_AL1_J_A_58_Ar_A_61_61_ATrue_1]) ).
cnf(c2599,plain,
( c_in(c_Pair(X2529,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_sko__4mj(v_S,X2529,v_r),v_S,t_a)
| v_S = c_emptyset ),
inference(resolution,[status(thm)],[c2531,cls_conjecture_2]) ).
cnf(c2635,plain,
( c_in(c_Pair(X2530,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_sko__4mj(v_S,X2530,v_r),v_S,t_a) ),
inference(resolution,[status(thm)],[c2599,cls_conjecture_3]) ).
cnf(c2710,plain,
( c_in(v_sko__4mj(v_S,X2650,v_r),v_S,t_a)
| ~ c_in(c_Pair(v_L,X2649,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_L,c_Tarski_Ointerval(v_r,X2650,X2649,t_a),t_a) ),
inference(resolution,[status(thm)],[c2635,cls_Tarski_O_91_124_A_Ia1_M_Ax1_J_A_58_Ar_59_A_Ix1_M_Ab1_J_A_58_Ar_A_124_93_A_61_61_62_Ax1_A_58_Ainterval_Ar_Aa1_Ab1_A_61_61_ATrue_0]) ).
cnf(c2835,plain,
( c_in(v_sko__4mj(v_S,X2651,v_r),v_S,t_a)
| c_in(v_L,c_Tarski_Ointerval(v_r,X2651,v_b,t_a),t_a) ),
inference(resolution,[status(thm)],[c2710,c759]) ).
cnf(c2849,plain,
c_in(v_sko__4mj(v_S,v_a,v_r),v_S,t_a),
inference(resolution,[status(thm)],[c2835,cls_conjecture_6]) ).
cnf(c2851,plain,
c_in(c_Pair(v_a,v_sko__4mj(v_S,v_a,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a)),
inference(resolution,[status(thm)],[c2849,c27]) ).
cnf(cls_Tarski_O_91_124_AS1_A_60_61_AA_59_AS1_A_126_61_A_123_125_59_AALL_Ax_58S1_O_A_Ia1_M_Ax_J_A_58_Ar_59_AALL_Ay_58S1_O_A_Iy_M_AL1_J_A_58_Ar_A_124_93_A_61_61_62_A_Ia1_M_AL1_J_A_58_Ar_A_61_61_ATrue_3,axiom,
( ~ c_in(c_Pair(X52,v_sko__4mj(X53,X52,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))
| ~ c_in(c_Pair(v_sko__4mk(X54,X53,v_r),X54,t_a,t_a),v_r,tc_prod(t_a,t_a))
| ~ c_lessequals(X53,X51,tc_set(t_a))
| c_in(c_Pair(X52,X54,t_a,t_a),v_r,tc_prod(t_a,t_a))
| X53 = c_emptyset ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_O_91_124_AS1_A_60_61_AA_59_AS1_A_126_61_A_123_125_59_AALL_Ax_58S1_O_A_Ia1_M_Ax_J_A_58_Ar_59_AALL_Ay_58S1_O_A_Iy_M_AL1_J_A_58_Ar_A_124_93_A_61_61_62_A_Ia1_M_AL1_J_A_58_Ar_A_61_61_ATrue_3) ).
cnf(c2534,plain,
( ~ c_in(c_Pair(X4744,v_sko__4mj(v_S,X4744,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))
| ~ c_lessequals(v_S,X4745,tc_set(t_a))
| c_in(c_Pair(X4744,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))
| v_S = c_emptyset ),
inference(resolution,[status(thm)],[c2527,cls_Tarski_O_91_124_AS1_A_60_61_AA_59_AS1_A_126_61_A_123_125_59_AALL_Ax_58S1_O_A_Ia1_M_Ax_J_A_58_Ar_59_AALL_Ay_58S1_O_A_Iy_M_AL1_J_A_58_Ar_A_124_93_A_61_61_62_A_Ia1_M_AL1_J_A_58_Ar_A_61_61_ATrue_3]) ).
cnf(c8769,plain,
( ~ c_lessequals(v_S,X4746,tc_set(t_a))
| c_in(c_Pair(v_a,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))
| v_S = c_emptyset ),
inference(resolution,[status(thm)],[c2534,c2851]) ).
cnf(c8793,plain,
( c_in(c_Pair(v_a,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))
| v_S = c_emptyset ),
inference(resolution,[status(thm)],[c8769,cls_conjecture_2]) ).
cnf(c8828,plain,
c_in(c_Pair(v_a,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a)),
inference(resolution,[status(thm)],[c8793,cls_conjecture_3]) ).
cnf(c8923,plain,
( ~ c_in(c_Pair(v_L,X4773,t_a,t_a),v_r,tc_prod(t_a,t_a))
| c_in(v_L,c_Tarski_Ointerval(v_r,v_a,X4773,t_a),t_a) ),
inference(resolution,[status(thm)],[c8828,cls_Tarski_O_91_124_A_Ia1_M_Ax1_J_A_58_Ar_59_A_Ix1_M_Ab1_J_A_58_Ar_A_124_93_A_61_61_62_Ax1_A_58_Ainterval_Ar_Aa1_Ab1_A_61_61_ATrue_0]) ).
cnf(c8963,plain,
c_in(v_L,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),t_a),
inference(resolution,[status(thm)],[c8923,c759]) ).
cnf(c8968,plain,
$false,
inference(resolution,[status(thm)],[c8963,cls_conjecture_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : LAT274-2 : TPTP v8.1.2. Released v3.2.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n017.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 13:06:37 EDT 2024
% 0.13/0.35 % CPUTime :
% 16.45/16.66 % Version: 1.5
% 16.45/16.66 % SZS status Unsatisfiable
% 16.45/16.66 % SZS output start CNFRefutation
% See solution above
% 16.45/16.66
% 16.45/16.66 % Initial clauses : 28
% 16.45/16.66 % Processed clauses : 1129
% 16.45/16.66 % Factors computed : 103
% 16.45/16.66 % Resolvents computed: 8882
% 16.45/16.66 % Tautologies deleted: 2
% 16.45/16.66 % Forward subsumed : 1221
% 16.45/16.66 % Backward subsumed : 354
% 16.45/16.66 % -------- CPU Time ---------
% 16.45/16.66 % User time : 16.257 s
% 16.45/16.66 % System time : 0.046 s
% 16.45/16.66 % Total time : 16.303 s
%------------------------------------------------------------------------------