%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : KRS040+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n032.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 : Sun Jul 17 03:30:22 EDT 2022
% Result : Satisfiable 0.48s 0.69s
% Output : Saturation 0.48s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 7418)
% Comments :
%------------------------------------------------------------------------------
cnf(7517,plain,
equal(iplus9,iplus3),
inference(spt,[],[7418]),
[iquote('10:Spt:7418.0')] ).
cnf(7511,plain,
equal(iminus8,iplus3),
inference(spt,[],[7417]),
[iquote('9:Spt:7417.0')] ).
cnf(7499,plain,
equal(iminus4,iminus3),
inference(mrr,[status(thm)],[7496,7356]),
[iquote('8:MRR:7496.1,7356.0')] ).
cnf(7487,plain,
equal(iplus4,iplus3),
inference(spt,[],[7416]),
[iquote('8:Spt:7416.0')] ).
cnf(7469,plain,
equal(iminus6,iplus3),
inference(spt,[],[7415]),
[iquote('7:Spt:7415.0')] ).
cnf(7433,plain,
equal(iminus7,iplus3),
inference(mrr,[status(thm)],[7432,7354]),
[iquote('6:MRR:7432.1,7354.0')] ).
cnf(7427,plain,
equal(iF,iplus3),
inference(mrr,[status(thm)],[7426,7355]),
[iquote('6:MRR:7426.1,7355.0')] ).
cnf(7421,plain,
equal(iplus5,iplus3),
inference(mrr,[status(thm)],[7420,7353]),
[iquote('6:MRR:7420.1,7353.0')] ).
cnf(46,axiom,
( ~ cTorF(u)
| equal(u,iplus3)
| equal(u,iminus3) ),
file('KRS040+1.p',unknown),
[] ).
cnf(7414,plain,
equal(iminus2,iplus3),
inference(rew,[status(thm),theory(equality)],[7409,7404]),
[iquote('6:Rew:7409.0,7404.0')] ).
cnf(7409,plain,
equal(iplus1,iplus3),
inference(mrr,[status(thm)],[7386,7356]),
[iquote('6:MRR:7386.1,7356.0')] ).
cnf(7356,plain,
~ equal(iplus3,iminus3),
inference(rew,[status(thm),theory(equality)],[7346,6483]),
[iquote('6:Rew:7346.0,6483.0')] ).
cnf(7352,plain,
equal(iminus5,iminus3),
inference(rew,[status(thm),theory(equality)],[7346,6913]),
[iquote('6:Rew:7346.0,6913.0')] ).
cnf(7351,plain,
equal(iT,iminus3),
inference(rew,[status(thm),theory(equality)],[7346,6482]),
[iquote('6:Rew:7346.0,6482.0')] ).
cnf(7350,plain,
equal(iplus2,iminus3),
inference(rew,[status(thm),theory(equality)],[7346,6476]),
[iquote('6:Rew:7346.0,6476.0')] ).
cnf(7349,plain,
equal(iminus9,iminus3),
inference(rew,[status(thm),theory(equality)],[7346,6481]),
[iquote('6:Rew:7346.0,6481.0')] ).
cnf(7348,plain,
equal(iplus8,iminus3),
inference(rew,[status(thm),theory(equality)],[7346,6479]),
[iquote('6:Rew:7346.0,6479.0')] ).
cnf(7346,plain,
equal(iplus6,iminus3),
inference(mrr,[status(thm)],[6492,7340]),
[iquote('6:MRR:6492.1,7340.0')] ).
cnf(7341,plain,
equal(iplus7,iminus3),
inference(spt,[],[7339,6495]),
[iquote('6:Spt:7339.0,6495.1')] ).
cnf(27,axiom,
( ~ equal(u,iplus3)
| cTorF(u) ),
file('KRS040+1.p',unknown),
[] ).
cnf(244,plain,
cTorF(iplus3),
inference(eqr,[status(thm),theory(equality)],[27]),
[iquote('0:EqR:27.0')] ).
cnf(6933,plain,
equal(iminus1,iminus3),
inference(spt,[],[6493]),
[iquote('5:Spt:6493.0')] ).
cnf(245,plain,
cTorF(iminus3),
inference(eqr,[status(thm),theory(equality)],[26]),
[iquote('0:EqR:26.0')] ).
cnf(26,axiom,
( ~ equal(u,iminus3)
| cTorF(u) ),
file('KRS040+1.p',unknown),
[] ).
cnf(25,axiom,
( ~ xsd_integer(u)
| ~ xsd_string(u) ),
file('KRS040+1.p',unknown),
[] ).
cnf(23,axiom,
( xsd_string(u)
| xsd_integer(u) ),
file('KRS040+1.p',unknown),
[] ).
cnf(22,axiom,
~ cowlNothing(u),
file('KRS040+1.p',unknown),
[] ).
cnf(1,axiom,
cowlThing(u),
file('KRS040+1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.10 % Problem : KRS040+1 : TPTP v8.1.0. Released v3.1.0.
% 0.06/0.10 % Command : run_spass %d %s
% 0.09/0.30 % Computer : n032.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 600
% 0.09/0.30 % DateTime : Tue Jun 7 18:09:36 EDT 2022
% 0.09/0.30 % CPUTime :
% 0.48/0.69
% 0.48/0.69 SPASS V 3.9
% 0.48/0.69 SPASS beiseite: Completion found.
% 0.48/0.69 % SZS status CounterSatisfiable
% 0.48/0.69 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.69 SPASS derived 5372 clauses, backtracked 2980 clauses, performed 171 splits and kept 5191 clauses.
% 0.48/0.69 SPASS allocated 100046 KBytes.
% 0.48/0.69 SPASS spent 0:00:00.36 on the problem.
% 0.48/0.69 0:00:00.03 for the input.
% 0.48/0.69 0:00:00.02 for the FLOTTER CNF translation.
% 0.48/0.69 0:00:00.02 for inferences.
% 0.48/0.69 0:00:00.01 for the backtracking.
% 0.48/0.69 0:00:00.24 for the reduction.
% 0.48/0.69
% 0.48/0.69
% 0.48/0.69 The saturated set of worked-off clauses is :
% 0.48/0.69 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------