%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL434-2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:58:29 PM UTC 2026
% Result : Unsatisfiable 175.21s 175.53s
% Output : CNFRefutation 175.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 9
% Syntax : Number of clauses : 21 ( 8 unt; 4 nHn; 12 RR)
% Number of literals : 44 ( 25 equ; 20 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 54 ( 7 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_conjecture_1,negated_conjecture,
~ c_in(c_PropLog_Opl_Oop_A_N_62(v_p,v_pa,t_a),c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c2,axiom,
( X58 != X60
| X56 != X55
| X57 != X59
| c_PropLog_Opl_Oop_A_N_62(X58,X56,X57) = c_PropLog_Opl_Oop_A_N_62(X60,X55,X59) ),
theory(equality) ).
cnf(c52,plain,
( X139 != X136
| X138 != X135
| c_PropLog_Opl_Oop_A_N_62(X139,X138,X137) = c_PropLog_Opl_Oop_A_N_62(X136,X135,X137) ),
inference(resolution,[status(thm)],[c2,reflexivity]) ).
cnf(c259,plain,
( X148 != X146
| c_PropLog_Opl_Oop_A_N_62(X148,X147,X145) = c_PropLog_Opl_Oop_A_N_62(X146,X147,X145) ),
inference(resolution,[status(thm)],[c52,reflexivity]) ).
cnf(cls_PropLog_Oweaken__right_0,axiom,
( ~ c_in(X31,c_PropLog_Othms(X29,X28),tc_PropLog_Opl(X28))
| c_in(c_PropLog_Opl_Oop_A_N_62(X30,X31,X28),c_PropLog_Othms(X29,X28),tc_PropLog_Opl(X28)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_PropLog_Oweaken__right_0) ).
cnf(cls_PropLog_Othms_OH_0,axiom,
( ~ c_in(X20,X19,tc_PropLog_Opl(X18))
| c_in(X20,c_PropLog_Othms(X19,X18),tc_PropLog_Opl(X18)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_PropLog_Othms_OH_0) ).
cnf(cls_conjecture_0,negated_conjecture,
c_in(v_pa,c_insert(v_p,v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(cls_Set_OinsertE_0,axiom,
( ~ c_in(X27,c_insert(X26,X24,X25),X25)
| c_in(X27,X24,X25)
| X27 = X26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OinsertE_0) ).
cnf(c11,plain,
( c_in(v_pa,v_H,tc_PropLog_Opl(t_a))
| v_pa = v_p ),
inference(resolution,[status(thm)],[cls_Set_OinsertE_0,cls_conjecture_0]) ).
cnf(c12,plain,
( v_pa = v_p
| c_in(v_pa,c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a)) ),
inference(resolution,[status(thm)],[c11,cls_PropLog_Othms_OH_0]) ).
cnf(c45,plain,
( v_pa = v_p
| c_in(c_PropLog_Opl_Oop_A_N_62(X190,v_pa,t_a),c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a)) ),
inference(resolution,[status(thm)],[c12,cls_PropLog_Oweaken__right_0]) ).
cnf(c830,plain,
v_pa = v_p,
inference(resolution,[status(thm)],[c45,cls_conjecture_1]) ).
cnf(c833,plain,
c_PropLog_Opl_Oop_A_N_62(v_pa,X210,X209) = c_PropLog_Opl_Oop_A_N_62(v_p,X210,X209),
inference(resolution,[status(thm)],[c830,c259]) ).
cnf(cls_PropLog_Othms__I_0,axiom,
c_in(c_PropLog_Opl_Oop_A_N_62(X17,X17,X15),c_PropLog_Othms(X16,X15),tc_PropLog_Opl(X15)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_PropLog_Othms__I_0) ).
cnf(c4,axiom,
( X65 != X67
| X63 != X62
| X64 != X66
| ~ c_in(X65,X63,X64)
| c_in(X67,X62,X66) ),
theory(equality) ).
cnf(c81,plain,
( c_PropLog_Opl_Oop_A_N_62(X306,X306,X309) != X308
| c_PropLog_Othms(X307,X309) != X311
| tc_PropLog_Opl(X309) != X310
| c_in(X308,X311,X310) ),
inference(resolution,[status(thm)],[c4,cls_PropLog_Othms__I_0]) ).
cnf(c2252,plain,
( c_PropLog_Othms(X6067,X6065) != X6066
| tc_PropLog_Opl(X6065) != X6064
| c_in(c_PropLog_Opl_Oop_A_N_62(v_p,v_pa,X6065),X6066,X6064) ),
inference(resolution,[status(thm)],[c81,c833]) ).
cnf(c300322,plain,
( tc_PropLog_Opl(X6068) != X6069
| c_in(c_PropLog_Opl_Oop_A_N_62(v_p,v_pa,X6068),c_PropLog_Othms(X6070,X6068),X6069) ),
inference(resolution,[status(thm)],[c2252,reflexivity]) ).
cnf(c300456,plain,
c_in(c_PropLog_Opl_Oop_A_N_62(v_p,v_pa,X6071),c_PropLog_Othms(X6072,X6071),tc_PropLog_Opl(X6071)),
inference(resolution,[status(thm)],[c300322,reflexivity]) ).
cnf(c300484,plain,
$false,
inference(resolution,[status(thm)],[c300456,cls_conjecture_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL434-2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.35 % Computer : n026.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 6 01:33:26 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.42 (re.compile("\."), Token.FullStop),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.42 (re.compile("\("), Token.OpenPar),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.42 (re.compile("\)"), Token.ClosePar),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.42 (re.compile("\["), Token.OpenSquare),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.42 (re.compile("~\|"), Token.Nor),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.42 (re.compile("\|"), Token.Or),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.42 (re.compile("\?"), Token.Existential),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.22/0.49 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.32/0.58 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.58 """
% 175.21/175.53 % Version: 1.5
% 175.21/175.53 % SZS status Unsatisfiable
% 175.21/175.53 % SZS output start CNFRefutation
% See solution above
% 175.21/175.53
% 175.21/175.53 % Initial clauses : 14
% 175.21/175.53 % Processed clauses : 1548
% 175.21/175.53 % Factors computed : 70
% 175.21/175.53 % Resolvents computed: 300412
% 175.21/175.53 % Tautologies deleted: 2
% 175.21/175.53 % Forward subsumed : 4208
% 175.21/175.53 % Backward subsumed : 388
% 175.21/175.53 % -------- CPU Time ---------
% 175.21/175.53 % User time : 174.251 s
% 175.21/175.53 % System time : 0.878 s
% 175.21/175.53 % Total time : 175.129 s
%------------------------------------------------------------------------------