%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : COM127+1 : TPTP v8.1.0. Released v6.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %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 : 600s
% DateTime : Fri Jul 15 01:44:41 EDT 2022
% Result : Theorem 3.51s 3.67s
% Output : Refutation 3.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 22
% Syntax : Number of clauses : 49 ( 18 unt; 7 nHn; 49 RR)
% Number of literals : 96 ( 0 equ; 44 neg)
% Maximal clause size : 7 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 44 ( 44 usr; 11 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(11,axiom,
~ visFreeVar(skc8,vvar(skc6)),
file('COM127+1.p',unknown),
[] ).
cnf(12,axiom,
vtcheck(skc5,vvar(skc6),skc7),
file('COM127+1.p',unknown),
[] ).
cnf(15,axiom,
~ equal(vsomeType(u),vnoType),
file('COM127+1.p',unknown),
[] ).
cnf(22,axiom,
~ equal(vvar(u),vapp(v,w)),
file('COM127+1.p',unknown),
[] ).
cnf(25,axiom,
equal(vsubst(u,v,vvar(u)),v),
file('COM127+1.p',unknown),
[] ).
cnf(33,axiom,
~ equal(vvar(u),vabs(v,w,x)),
file('COM127+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ equal(u,v)
| visFreeVar(v,vvar(u)) ),
file('COM127+1.p',unknown),
[] ).
cnf(38,axiom,
( ~ skP7(u)
| equal(vvar(skf77(u)),u) ),
file('COM127+1.p',unknown),
[] ).
cnf(41,axiom,
~ vtcheck(vbind(skc8,skc9,skc5),vvar(skc6),skc7),
file('COM127+1.p',unknown),
[] ).
cnf(55,axiom,
( ~ skP12(u)
| equal(vapp(skf96(u),skf97(u)),u) ),
file('COM127+1.p',unknown),
[] ).
cnf(60,axiom,
( equal(u,v)
| equal(vsubst(u,w,vvar(v)),vvar(v)) ),
file('COM127+1.p',unknown),
[] ).
cnf(72,axiom,
( ~ skP8(u)
| equal(vabs(skf78(u),skf79(u),skf80(u)),u) ),
file('COM127+1.p',unknown),
[] ).
cnf(73,axiom,
( ~ equal(vlookup(u,v),vsomeType(w))
| vtcheck(v,vvar(u),w) ),
file('COM127+1.p',unknown),
[] ).
cnf(74,axiom,
( ~ skP13(u,v,w)
| equal(vvar(skf101(w,x,y)),w) ),
file('COM127+1.p',unknown),
[] ).
cnf(82,axiom,
( equal(u,v)
| equal(vlookup(u,vbind(v,w,x)),vlookup(u,x)) ),
file('COM127+1.p',unknown),
[] ).
cnf(87,axiom,
( ~ skP13(u,v,w)
| equal(vlookup(skf101(w,u,v),v),vsomeType(u)) ),
file('COM127+1.p',unknown),
[] ).
cnf(92,axiom,
( ~ skP9(u)
| equal(vapp(vabs(skf82(u),skf83(u),skf84(u)),skf81(u)),u) ),
file('COM127+1.p',unknown),
[] ).
cnf(93,axiom,
( ~ skP10(u)
| equal(vapp(vabs(skf86(u),skf88(u),skf87(u)),skf85(u)),u) ),
file('COM127+1.p',unknown),
[] ).
cnf(94,axiom,
( ~ skP11(u)
| equal(vapp(vabs(skf90(u),skf91(u),skf92(u)),skf89(u)),u) ),
file('COM127+1.p',unknown),
[] ).
cnf(109,axiom,
( skP12(u)
| skP11(u)
| skP10(u)
| skP9(u)
| skP8(u)
| skP7(u)
| equal(vapp(skf75(u),skf76(u)),u) ),
file('COM127+1.p',unknown),
[] ).
cnf(111,axiom,
( ~ skP14(u,v,w)
| equal(vabs(skf104(w,u,v),skf103(v,u,w),skf105(w,u,v)),w) ),
file('COM127+1.p',unknown),
[] ).
cnf(119,axiom,
( ~ vtcheck(u,v,w)
| equal(vapp(skf100(v,w,u),skf98(w,u,v)),v)
| skP14(u,w,v)
| skP13(w,u,v) ),
file('COM127+1.p',unknown),
[] ).
cnf(137,plain,
~ equal(skc8,skc6),
inference(res,[status(thm),theory(equality)],[34,11]),
[iquote('0:Res:34.1,11.0')] ).
cnf(181,plain,
( ~ skP7(u)
| equal(vsubst(skf77(u),v,u),v) ),
inference(spr,[status(thm),theory(equality)],[38,25]),
[iquote('0:SpR:38.1,25.0')] ).
cnf(344,plain,
( ~ skP12(u)
| ~ equal(vvar(v),u) ),
inference(spl,[status(thm),theory(equality)],[55,22]),
[iquote('0:SpL:55.1,22.0')] ).
cnf(389,plain,
( ~ skP7(vvar(u))
| equal(skf77(vvar(u)),u)
| equal(vvar(u),v) ),
inference(spr,[status(thm),theory(equality)],[60,181]),
[iquote('0:SpR:60.1,181.1')] ).
cnf(394,plain,
( ~ skP7(vvar(u))
| equal(skf77(vvar(u)),u) ),
inference(aed,[status(thm),theory(equality)],[15,389]),
[iquote('0:AED:15.0,389.2')] ).
cnf(553,plain,
( ~ skP8(u)
| ~ equal(vvar(v),u) ),
inference(spl,[status(thm),theory(equality)],[72,33]),
[iquote('0:SpL:72.1,33.0')] ).
cnf(575,plain,
~ equal(vlookup(skc6,vbind(skc8,skc9,skc5)),vsomeType(skc7)),
inference(res,[status(thm),theory(equality)],[73,41]),
[iquote('0:Res:73.1,41.0')] ).
cnf(709,plain,
( ~ equal(vlookup(skc6,skc5),vsomeType(skc7))
| equal(skc8,skc6) ),
inference(spl,[status(thm),theory(equality)],[82,575]),
[iquote('0:SpL:82.1,575.0')] ).
cnf(710,plain,
~ equal(vlookup(skc6,skc5),vsomeType(skc7)),
inference(mrr,[status(thm)],[709,137]),
[iquote('0:MRR:709.1,137.0')] ).
cnf(1039,plain,
( ~ skP11(u)
| ~ equal(vvar(v),u) ),
inference(spl,[status(thm),theory(equality)],[94,22]),
[iquote('0:SpL:94.1,22.0')] ).
cnf(1097,plain,
( ~ skP10(u)
| ~ equal(vvar(v),u) ),
inference(spl,[status(thm),theory(equality)],[93,22]),
[iquote('0:SpL:93.1,22.0')] ).
cnf(1161,plain,
( ~ skP9(u)
| ~ equal(vvar(v),u) ),
inference(spl,[status(thm),theory(equality)],[92,22]),
[iquote('0:SpL:92.1,22.0')] ).
cnf(2424,plain,
( ~ equal(vvar(u),v)
| skP12(v)
| skP11(v)
| skP10(v)
| skP9(v)
| skP8(v)
| skP7(v) ),
inference(spl,[status(thm),theory(equality)],[109,22]),
[iquote('0:SpL:109.6,22.0')] ).
cnf(2464,plain,
( ~ equal(vvar(u),v)
| skP7(v) ),
inference(mrr,[status(thm)],[2424,344,1039,1097,1161,553]),
[iquote('0:MRR:2424.1,2424.2,2424.3,2424.4,2424.5,344.0,1039.0,1097.0,1161.0,553.0')] ).
cnf(2515,plain,
skP7(vvar(u)),
inference(eqr,[status(thm),theory(equality)],[2464]),
[iquote('0:EqR:2464.0')] ).
cnf(2519,plain,
equal(skf77(vvar(u)),u),
inference(mrr,[status(thm)],[394,2515]),
[iquote('0:MRR:394.0,2515.0')] ).
cnf(2600,plain,
( ~ skP14(u,v,w)
| ~ equal(vvar(x),w) ),
inference(spl,[status(thm),theory(equality)],[111,33]),
[iquote('0:SpL:111.1,33.0')] ).
cnf(3161,plain,
( ~ vtcheck(u,v,w)
| ~ equal(vvar(x),v)
| skP14(u,w,v)
| skP13(w,u,v) ),
inference(spl,[status(thm),theory(equality)],[119,22]),
[iquote('0:SpL:119.1,22.0')] ).
cnf(3200,plain,
( ~ vtcheck(u,v,w)
| ~ equal(vvar(x),v)
| skP13(w,u,v) ),
inference(mrr,[status(thm)],[3161,2600]),
[iquote('0:MRR:3161.2,2600.0')] ).
cnf(9232,plain,
( ~ equal(vvar(u),vvar(skc6))
| skP13(skc7,skc5,vvar(skc6)) ),
inference(res,[status(thm),theory(equality)],[12,3200]),
[iquote('0:Res:12.0,3200.0')] ).
cnf(9243,plain,
skP13(skc7,skc5,vvar(skc6)),
inference(eqr,[status(thm),theory(equality)],[9232]),
[iquote('0:EqR:9232.0')] ).
cnf(9256,plain,
equal(vvar(skf101(vvar(skc6),u,v)),vvar(skc6)),
inference(res,[status(thm),theory(equality)],[9243,74]),
[iquote('0:Res:9243.0,74.0')] ).
cnf(9275,plain,
equal(skf101(vvar(skc6),u,v),skf77(vvar(skc6))),
inference(spr,[status(thm),theory(equality)],[9256,2519]),
[iquote('0:SpR:9256.0,2519.0')] ).
cnf(9369,plain,
equal(skf101(vvar(skc6),u,v),skc6),
inference(rew,[status(thm),theory(equality)],[2519,9275]),
[iquote('0:Rew:2519.0,9275.0')] ).
cnf(9468,plain,
( ~ skP13(u,v,vvar(skc6))
| equal(vlookup(skc6,v),vsomeType(u)) ),
inference(spr,[status(thm),theory(equality)],[9369,87]),
[iquote('0:SpR:9369.0,87.1')] ).
cnf(9565,plain,
equal(vlookup(skc6,skc5),vsomeType(skc7)),
inference(res,[status(thm),theory(equality)],[9243,9468]),
[iquote('0:Res:9243.0,9468.0')] ).
cnf(9568,plain,
$false,
inference(mrr,[status(thm)],[9565,710]),
[iquote('0:MRR:9565.0,710.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : COM127+1 : TPTP v8.1.0. Released v6.4.0.
% 0.00/0.12 % Command : run_spass %d %s
% 0.11/0.33 % Computer : n018.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Thu Jun 16 17:19:31 EDT 2022
% 0.11/0.33 % CPUTime :
% 3.51/3.67
% 3.51/3.67 SPASS V 3.9
% 3.51/3.67 SPASS beiseite: Proof found.
% 3.51/3.67 % SZS status Theorem
% 3.51/3.67 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.51/3.67 SPASS derived 7730 clauses, backtracked 0 clauses, performed 0 splits and kept 3476 clauses.
% 3.51/3.67 SPASS allocated 108355 KBytes.
% 3.51/3.67 SPASS spent 0:00:03.22 on the problem.
% 3.51/3.67 0:00:00.04 for the input.
% 3.51/3.67 0:00:00.26 for the FLOTTER CNF translation.
% 3.51/3.67 0:00:00.12 for inferences.
% 3.51/3.67 0:00:00.00 for the backtracking.
% 3.51/3.67 0:00:02.73 for the reduction.
% 3.51/3.67
% 3.51/3.67
% 3.51/3.67 Here is a proof with depth 7, length 49 :
% 3.51/3.67 % SZS output start Refutation
% See solution above
% 3.51/3.67 Formulae used in the proof : T_a45_Weak_a45_FreeVar_a45_var DIFF_a45_noType_a45_someType DIFF_a45_var_a45_app subst0 DIFF_a45_var_a45_abs isFreeVar0 reduce_a45_INV DIFF_a45_abs_a45_app isValue0 isValue1 subst1 T_a45_var T_a45_inv lookup1 T_a45_abs lookup2
% 3.51/3.67
%------------------------------------------------------------------------------