%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN008-6 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n018.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 : Mon Jun 24 07:26:51 EDT 2024
% Result : Unsatisfiable 10.75s 10.80s
% Output : CNFRefutation 10.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : HEN008-6 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n018.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Sat Jun 22 05:36:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.20/0.57 start to proof:theBenchmark
% 10.75/10.80 %-------------------------------------------
% 10.75/10.80 % File :CSE---1.7
% 10.75/10.80 % Problem :theBenchmark
% 10.75/10.80 % Transform :cnf
% 10.75/10.80 % Format :tptp:raw
% 10.75/10.80 % Command :java -jar mcs_scs.jar %d %s
% 10.75/10.80
% 10.75/10.80 % Result :Theorem 10.200000s
% 10.75/10.80 % Output :CNFRefutation 10.200000s
% 10.75/10.80 %-------------------------------------------
% 10.75/10.80 %--------------------------------------------------------------------------
% 10.75/10.80 % File : HEN008-6 : TPTP v8.2.0. Released v1.0.0.
% 10.75/10.80 % Domain : Henkin Models
% 10.75/10.80 % Problem : X <= Y => X/Z <= Y/Z
% 10.75/10.80 % Version : [MOW76] axioms : Augmented.
% 10.75/10.80 % English :
% 10.75/10.80
% 10.75/10.80 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 10.75/10.80 % Source : [ANL]
% 10.75/10.80 % Names : hp8.ver2.in [ANL]
% 10.75/10.80
% 10.75/10.80 % Status : Unsatisfiable
% 10.75/10.80 % Rating : 0.00 v5.5.0, 0.06 v5.4.0, 0.07 v5.3.0, 0.08 v5.2.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.00 v3.1.0, 0.11 v2.7.0, 0.00 v2.6.0, 0.14 v2.5.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.20 v2.0.0
% 10.75/10.80 % Syntax : Number of clauses : 12 ( 9 unt; 0 nHn; 5 RR)
% 10.75/10.80 % Number of literals : 16 ( 6 equ; 5 neg)
% 10.75/10.80 % Maximal clause size : 3 ( 1 avg)
% 10.75/10.80 % Maximal term depth : 3 ( 1 avg)
% 10.75/10.80 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)
% 10.75/10.80 % Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% 10.75/10.80 % Number of variables : 16 ( 5 sgn)
% 10.75/10.80 % SPC : CNF_UNS_RFO_SEQ_HRN
% 10.75/10.80
% 10.75/10.80 % Comments :
% 10.75/10.80 %--------------------------------------------------------------------------
% 10.75/10.80 %----Include Henkin model axioms for equality formulation
% 10.75/10.80 include('Axioms/HEN002-0.ax').
% 10.75/10.80 %--------------------------------------------------------------------------
% 10.75/10.80 cnf(everything_divide_id_is_zero,axiom,
% 10.75/10.80 divide(X,identity) = zero ).
% 10.75/10.80
% 10.75/10.80 cnf(zero_divide_anything_is_zero,axiom,
% 10.75/10.80 divide(zero,X) = zero ).
% 10.75/10.80
% 10.75/10.80 cnf(x_divide_x_is_zero,axiom,
% 10.75/10.80 divide(X,X) = zero ).
% 10.75/10.80
% 10.75/10.80 cnf(a_LE_b,hypothesis,
% 10.75/10.80 less_equal(a,b) ).
% 10.75/10.80
% 10.75/10.80 cnf(prove_a_divide_c_LE_b_divide_c,negated_conjecture,
% 10.75/10.80 ~ less_equal(divide(a,c),divide(b,c)) ).
% 10.75/10.80
% 10.75/10.80 %--------------------------------------------------------------------------
% 10.75/10.80 %-------------------------------------------
% 10.75/10.80 % Proof found
% 10.75/10.80 % SZS status Theorem for theBenchmark
% 10.75/10.80 % SZS output start Proof
% 10.75/10.81 %ClaNum:19(EqnAxiom:7)
% 10.77/10.81 %VarNum:30(SingletonVarNum:16)
% 10.77/10.81 %MaxLitNum:3
% 10.77/10.81 %MaxfuncDepth:2
% 10.77/10.81 %SharedTerms:9
% 10.77/10.81 %goalClause: 16
% 10.77/10.81 %singleGoalClaCount:1
% 10.77/10.81 [8]P1(a1,a2)
% 10.77/10.81 [16]~P1(f4(a1,a5),f4(a2,a5))
% 10.77/10.81 [11]P1(x111,a3)
% 10.77/10.81 [12]P1(a6,x121)
% 10.77/10.81 [9]E(f4(x91,a3),a6)
% 10.77/10.81 [10]E(f4(a6,x101),a6)
% 10.77/10.81 [13]E(f4(x131,x131),a6)
% 10.77/10.81 [14]P1(f4(x141,x142),x141)
% 10.77/10.81 [15]P1(f4(f4(x151,x152),f4(x153,x152)),f4(f4(x151,x153),x152))
% 10.77/10.81 [17]~P1(x171,x172)+E(f4(x171,x172),a6)
% 10.77/10.81 [18]P1(x181,x182)+~E(f4(x181,x182),a6)
% 10.77/10.81 [19]~P1(x192,x191)+~P1(x191,x192)+E(x191,x192)
% 10.77/10.81 %EqnAxiom
% 10.77/10.81 [1]E(x11,x11)
% 10.77/10.81 [2]E(x22,x21)+~E(x21,x22)
% 10.77/10.81 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 10.77/10.81 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43))
% 10.77/10.81 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52))
% 10.77/10.81 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 10.77/10.81 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 10.77/10.81
% 10.77/10.81 %-------------------------------------------
% 10.77/10.81 cnf(20,plain,
% 10.77/10.81 (P1(x201,x201)),
% 10.77/10.81 inference(scs_inference,[],[13,18])).
% 10.77/10.81 cnf(22,plain,
% 10.77/10.81 (E(a6,f4(x221,x221))),
% 10.77/10.81 inference(scs_inference,[],[13,18,2])).
% 10.77/10.81 cnf(24,plain,
% 10.77/10.81 (P1(a6,x241)),
% 10.77/10.81 inference(rename_variables,[],[12])).
% 10.77/10.81 cnf(27,plain,
% 10.77/10.81 (~P1(f4(a1,a5),a6)),
% 10.77/10.81 inference(scs_inference,[],[16,11,12,24,13,18,2,6,7,19])).
% 10.77/10.81 cnf(30,plain,
% 10.77/10.81 (E(a6,f4(x301,a3))),
% 10.77/10.81 inference(scs_inference,[],[9,2])).
% 10.77/10.81 cnf(31,plain,
% 10.77/10.81 (E(f4(x311,a3),f4(x312,x312))),
% 10.77/10.81 inference(scs_inference,[],[22,9,2,3])).
% 10.77/10.81 cnf(33,plain,
% 10.77/10.81 (P1(x331,x331)),
% 10.77/10.81 inference(rename_variables,[],[20])).
% 10.77/10.81 cnf(34,plain,
% 10.77/10.81 (~E(f4(a2,a5),f4(a1,a5))),
% 10.77/10.81 inference(scs_inference,[],[16,20,33,22,9,2,3,7,6])).
% 10.77/10.81 cnf(41,plain,
% 10.77/10.81 (E(f4(a6,x411),f4(x412,a3))),
% 10.77/10.81 inference(scs_inference,[],[34,31,30,10,4,2,3])).
% 10.77/10.81 cnf(43,plain,
% 10.77/10.81 (P1(f4(x431,x432),x431)),
% 10.77/10.81 inference(rename_variables,[],[14])).
% 10.77/10.81 cnf(44,plain,
% 10.77/10.81 (~E(f4(f4(a2,a5),x441),f4(a1,a5))),
% 10.77/10.81 inference(scs_inference,[],[16,34,31,14,43,30,10,4,2,3,7,6])).
% 10.77/10.81 cnf(50,plain,
% 10.77/10.81 (E(a6,f4(a6,x501))),
% 10.77/10.81 inference(scs_inference,[],[44,10,4,2])).
% 10.77/10.81 cnf(52,plain,
% 10.77/10.81 (P1(x521,a2)+~E(a1,x521)),
% 10.77/10.81 inference(scs_inference,[],[44,10,22,8,4,2,3,6])).
% 10.77/10.81 cnf(69,plain,
% 10.77/10.81 (E(f4(f4(x691,a3),f4(x692,a3)),a6)),
% 10.77/10.81 inference(scs_inference,[],[12,15,9,41,30,2,3,7,19])).
% 10.77/10.81 cnf(72,plain,
% 10.77/10.81 (~E(f4(f4(x721,a3),f4(x722,a3)),f4(a1,a5))),
% 10.77/10.81 inference(scs_inference,[],[12,15,9,27,41,30,2,3,7,19,6])).
% 10.77/10.81 cnf(73,plain,
% 10.77/10.81 (P1(f4(x731,a3),f4(x732,a3))),
% 10.77/10.81 inference(scs_inference,[],[12,15,9,27,41,30,2,3,7,19,6,18])).
% 10.77/10.81 cnf(75,plain,
% 10.77/10.81 (E(a6,f4(f4(x751,a3),f4(x752,a3)))),
% 10.77/10.81 inference(scs_inference,[],[69,2])).
% 10.77/10.81 cnf(80,plain,
% 10.77/10.81 (~E(f4(x801,a3),f4(a1,a5))),
% 10.77/10.81 inference(scs_inference,[],[73,13,69,27,2,3,7,6])).
% 10.77/10.81 cnf(98,plain,
% 10.77/10.81 (~E(a1,x981)+E(f4(x981,a2),a6)),
% 10.77/10.81 inference(scs_inference,[],[17,52])).
% 10.77/10.81 cnf(99,plain,
% 10.77/10.81 (E(f4(a1,a2),a6)),
% 10.77/10.81 inference(equality_inference,[],[98])).
% 10.77/10.82 cnf(100,plain,
% 10.77/10.82 (E(a6,f4(a1,a2))),
% 10.77/10.82 inference(scs_inference,[],[99,2])).
% 10.77/10.82 cnf(222,plain,
% 10.77/10.82 (P1(f4(f4(x2221,a3),f4(x2222,a3)),x2223)),
% 10.77/10.82 inference(scs_inference,[],[12,75,6])).
% 10.77/10.82 cnf(229,plain,
% 10.77/10.82 (P1(f4(x2291,a3),x2292)),
% 10.77/10.82 inference(scs_inference,[],[222,72,12,30,19,6])).
% 10.77/10.82 cnf(234,plain,
% 10.77/10.82 (P1(f4(a6,x2341),x2342)),
% 10.77/10.82 inference(scs_inference,[],[44,229,12,50,19,6])).
% 10.77/10.82 cnf(240,plain,
% 10.77/10.82 (P1(f4(a1,a2),x2401)),
% 10.77/10.82 inference(scs_inference,[],[80,234,12,100,19,6])).
% 10.77/10.82 cnf(967,plain,
% 10.77/10.82 (E(a6,f4(f4(a1,a2),x9671))),
% 10.77/10.82 inference(scs_inference,[],[240,17,2])).
% 10.77/10.82 cnf(968,plain,
% 10.77/10.82 (E(f4(f4(a1,a2),x9681),a6)),
% 10.77/10.82 inference(scs_inference,[],[967,2])).
% 10.77/10.82 cnf(986,plain,
% 10.77/10.82 (~P1(f4(f4(a1,a5),f4(a2,a5)),a6)),
% 10.77/10.82 inference(scs_inference,[],[16,12,18,19])).
% 10.77/10.82 cnf(987,plain,
% 10.77/10.82 ($false),
% 10.77/10.82 inference(scs_inference,[],[15,986,968,7]),
% 10.77/10.82 ['proof']).
% 10.77/10.82 % SZS output end Proof
% 10.77/10.82 % Total time :10.200000s
%------------------------------------------------------------------------------