%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : CSR114+10 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% 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 02:49:06 EDT 2022
% Result : Theorem 4.97s 2.77s
% Output : CNFRefutation 4.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 10
% Syntax : Number of clauses : 28 ( 6 unt; 0 nHn; 28 RR)
% Number of literals : 81 ( 0 equ; 62 neg)
% Maximal clause size : 7 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-3 aty)
% Number of variables : 77 ( 10 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_938,negated_conjecture,
( ~ in(X1,X2)
| ~ loc(X3,X1)
| ~ scar(X3,X4)
| ~ attr(X2,X5)
| ~ subs(X3,stehen_1_1)
| ~ sub(X5,name_1_1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-6rwanliw/input.p',i_0_938) ).
cnf(i_0_894,plain,
( sub(esk49_3(X1,X2,X3),name_1_1)
| ~ prop(X1,X2)
| ~ state_adjective_state_binding(X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-6rwanliw/input.p',i_0_894) ).
cnf(i_0_897,plain,
( attr(esk48_3(X1,X2,X3),esk49_3(X1,X2,X3))
| ~ prop(X1,X2)
| ~ state_adjective_state_binding(X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-6rwanliw/input.p',i_0_897) ).
cnf(i_0_898,plain,
( in(esk50_3(X1,X2,X3),esk48_3(X1,X2,X3))
| ~ prop(X1,X2)
| ~ state_adjective_state_binding(X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-6rwanliw/input.p',i_0_898) ).
cnf(i_0_807,plain,
( loc(esk27_2(X1,X2),X2)
| ~ loc(X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-6rwanliw/input.p',i_0_807) ).
cnf(i_0_805,plain,
( subs(esk27_2(X1,X2),stehen_1_1)
| ~ loc(X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-6rwanliw/input.p',i_0_805) ).
cnf(i_0_806,plain,
( scar(esk27_2(X1,X2),X1)
| ~ loc(X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-6rwanliw/input.p',i_0_806) ).
cnf(i_0_896,plain,
( loc(X1,esk50_3(X1,X2,X3))
| ~ prop(X1,X2)
| ~ state_adjective_state_binding(X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-6rwanliw/input.p',i_0_896) ).
cnf(i_0_697,plain,
state_adjective_state_binding(italienisch__1_1,italien_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-6rwanliw/input.p',i_0_697) ).
cnf(i_0_421,hypothesis,
prop(c40954,italienisch__1_1),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-6rwanliw/input.p',i_0_421) ).
cnf(c_0_949,negated_conjecture,
( ~ in(X1,X2)
| ~ loc(X3,X1)
| ~ scar(X3,X4)
| ~ attr(X2,X5)
| ~ subs(X3,stehen_1_1)
| ~ sub(X5,name_1_1) ),
i_0_938 ).
cnf(c_0_950,plain,
( sub(esk49_3(X1,X2,X3),name_1_1)
| ~ prop(X1,X2)
| ~ state_adjective_state_binding(X2,X3) ),
i_0_894 ).
cnf(c_0_951,negated_conjecture,
( ~ scar(X1,X2)
| ~ loc(X1,X3)
| ~ in(X3,X4)
| ~ state_adjective_state_binding(X5,X6)
| ~ attr(X4,esk49_3(X7,X5,X6))
| ~ prop(X7,X5)
| ~ subs(X1,stehen_1_1) ),
inference(spm,[status(thm)],[c_0_949,c_0_950]) ).
cnf(c_0_952,plain,
( attr(esk48_3(X1,X2,X3),esk49_3(X1,X2,X3))
| ~ prop(X1,X2)
| ~ state_adjective_state_binding(X2,X3) ),
i_0_897 ).
cnf(c_0_953,plain,
( ~ scar(X1,X2)
| ~ loc(X1,X3)
| ~ in(X3,esk48_3(X4,X5,X6))
| ~ state_adjective_state_binding(X5,X6)
| ~ prop(X4,X5)
| ~ subs(X1,stehen_1_1) ),
inference(spm,[status(thm)],[c_0_951,c_0_952]) ).
cnf(c_0_954,plain,
( in(esk50_3(X1,X2,X3),esk48_3(X1,X2,X3))
| ~ prop(X1,X2)
| ~ state_adjective_state_binding(X2,X3) ),
i_0_898 ).
cnf(c_0_955,plain,
( ~ scar(X1,X2)
| ~ loc(X1,esk50_3(X3,X4,X5))
| ~ state_adjective_state_binding(X4,X5)
| ~ prop(X3,X4)
| ~ subs(X1,stehen_1_1) ),
inference(spm,[status(thm)],[c_0_953,c_0_954]) ).
cnf(c_0_956,plain,
( loc(esk27_2(X1,X2),X2)
| ~ loc(X1,X2) ),
i_0_807 ).
cnf(c_0_957,plain,
( subs(esk27_2(X1,X2),stehen_1_1)
| ~ loc(X1,X2) ),
i_0_805 ).
cnf(c_0_958,plain,
( ~ scar(esk27_2(X1,esk50_3(X2,X3,X4)),X5)
| ~ loc(X1,esk50_3(X2,X3,X4))
| ~ state_adjective_state_binding(X3,X4)
| ~ prop(X2,X3) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_955,c_0_956]),c_0_957]) ).
cnf(c_0_959,plain,
( scar(esk27_2(X1,X2),X1)
| ~ loc(X1,X2) ),
i_0_806 ).
cnf(c_0_960,plain,
( ~ loc(X1,esk50_3(X2,X3,X4))
| ~ state_adjective_state_binding(X3,X4)
| ~ prop(X2,X3) ),
inference(spm,[status(thm)],[c_0_958,c_0_959]) ).
cnf(c_0_961,plain,
( loc(X1,esk50_3(X1,X2,X3))
| ~ prop(X1,X2)
| ~ state_adjective_state_binding(X2,X3) ),
i_0_896 ).
cnf(c_0_962,plain,
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X3,X1) ),
inference(spm,[status(thm)],[c_0_960,c_0_961]) ).
cnf(c_0_963,plain,
state_adjective_state_binding(italienisch__1_1,italien_0),
i_0_697 ).
cnf(c_0_964,hypothesis,
prop(c40954,italienisch__1_1),
i_0_421 ).
cnf(c_0_965,plain,
~ prop(X1,italienisch__1_1),
inference(spm,[status(thm)],[c_0_962,c_0_963]) ).
cnf(c_0_966,hypothesis,
$false,
inference(sr,[status(thm)],[c_0_964,c_0_965]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : CSR114+10 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.12/0.33 % Computer : n018.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Thu Jun 9 20:34:10 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.19/0.44 # ENIGMATIC: Selected SinE mode:
% 0.37/0.58 # Parsing /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/0.58 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.37/0.58 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.37/0.58 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 4.97/2.77 # ENIGMATIC: Solved by G_E___302_C18_F1_URBAN_S5PRR_RG_S04BN:
% 4.97/2.77 # Version: 2.1pre011
% 4.97/2.77 # Preprocessing time : 0.029 s
% 4.97/2.77
% 4.97/2.77 # Proof found!
% 4.97/2.77 # SZS status Theorem
% 4.97/2.77 # SZS output start CNFRefutation
% See solution above
% 4.97/2.77 # Proof object total steps : 28
% 4.97/2.77 # Proof object clause steps : 18
% 4.97/2.77 # Proof object formula steps : 10
% 4.97/2.77 # Proof object conjectures : 3
% 4.97/2.77 # Proof object clause conjectures : 2
% 4.97/2.77 # Proof object formula conjectures : 1
% 4.97/2.77 # Proof object initial clauses used : 10
% 4.97/2.77 # Proof object initial formulas used : 10
% 4.97/2.77 # Proof object generating inferences : 7
% 4.97/2.77 # Proof object simplifying inferences : 2
% 4.97/2.77 # Training examples: 0 positive, 0 negative
% 4.97/2.77 # Parsed axioms : 958
% 4.97/2.77 # Removed by relevancy pruning/SinE : 0
% 4.97/2.77 # Initial clauses : 958
% 4.97/2.77 # Removed in clause preprocessing : 0
% 4.97/2.77 # Initial clauses in saturation : 958
% 4.97/2.77 # Processed clauses : 1141
% 4.97/2.77 # ...of these trivial : 1
% 4.97/2.77 # ...subsumed : 0
% 4.97/2.77 # ...remaining for further processing : 1140
% 4.97/2.77 # Other redundant clauses eliminated : 0
% 4.97/2.77 # Clauses deleted for lack of memory : 0
% 4.97/2.77 # Backward-subsumed : 43
% 4.97/2.77 # Backward-rewritten : 0
% 4.97/2.77 # Generated clauses : 1031
% 4.97/2.77 # ...of the previous two non-trivial : 1030
% 4.97/2.77 # Contextual simplify-reflections : 13
% 4.97/2.77 # Paramodulations : 1030
% 4.97/2.77 # Factorizations : 0
% 4.97/2.77 # Equation resolutions : 0
% 4.97/2.77 # Propositional unsat checks : 0
% 4.97/2.77 # Propositional unsat check successes : 0
% 4.97/2.77 # Current number of processed clauses : 1096
% 4.97/2.77 # Positive orientable unit clauses : 692
% 4.97/2.77 # Positive unorientable unit clauses: 0
% 4.97/2.77 # Negative unit clauses : 4
% 4.97/2.77 # Non-unit-clauses : 400
% 4.97/2.77 # Current number of unprocessed clauses: 758
% 4.97/2.77 # ...number of literals in the above : 3286
% 4.97/2.77 # Current number of archived formulas : 0
% 4.97/2.77 # Current number of archived clauses : 44
% 4.97/2.77 # Clause-clause subsumption calls (NU) : 37610
% 4.97/2.77 # Rec. Clause-clause subsumption calls : 10351
% 4.97/2.77 # Non-unit clause-clause subsumptions : 56
% 4.97/2.77 # Unit Clause-clause subsumption calls : 2579
% 4.97/2.77 # Rewrite failures with RHS unbound : 0
% 4.97/2.77 # BW rewrite match attempts : 0
% 4.97/2.77 # BW rewrite match successes : 0
% 4.97/2.77 # Condensation attempts : 0
% 4.97/2.77 # Condensation successes : 0
% 4.97/2.77 # Termbank termtop insertions : 31819
% 4.97/2.77
% 4.97/2.77 # -------------------------------------------------
% 4.97/2.77 # User time : 0.071 s
% 4.97/2.77 # System time : 0.008 s
% 4.97/2.77 # Total time : 0.079 s
% 4.97/2.77 # ...preprocessing : 0.029 s
% 4.97/2.77 # ...main loop : 0.051 s
% 4.97/2.77 # Maximum resident set size: 10500 pages
% 4.97/2.77
%------------------------------------------------------------------------------