%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV888-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n012.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 : Fri Sep 25 03:14:23 PM UTC 2026
% Result : Unsatisfiable 2.65s 0.78s
% Output : Proof 2.65s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t78,axiom,
sF4 = c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_x,v_xa),
introduced(definition) ).
cnf(t76,axiom,
sF2 = c_Com_Obody(v_pn),
introduced(definition) ).
cnf(t82,plain,
c_Com_Obody(v_pn) = sF2,
inference(orient,[status(thm)],[t76]) ).
cnf(t947,plain,
sF4 = c_Natural_Oevalc(c_Option_Othe(sF2,tc_Com_Ocom),v_x,v_xa),
inference(step,[status(thm)],[t78,t82]) ).
cnf(t77,axiom,
sF3 = c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),
introduced(definition) ).
cnf(t910,plain,
sF3 = c_Option_Othe(sF2,tc_Com_Ocom),
inference(step,[status(thm)],[t77,t82]) ).
cnf(t97,plain,
c_Option_Othe(sF2,tc_Com_Ocom) = sF3,
inference(orient,[status(thm)],[t910]) ).
cnf(t948,plain,
sF4 = c_Natural_Oevalc(sF3,v_x,v_xa),
inference(step,[status(thm)],[t947,t97]) ).
cnf(f53,negated_conjecture,
c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_x,v_xa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f53_nnf,plain,
c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_x,v_xa),
inference(nnf_transformation,[status(thm)],[f53]) ).
cnf(c53,plain,
c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_x,v_xa),
inference(cnf_transformation,[status(esa)],[f53_nnf]) ).
cnf(t28,plain,
c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_x,v_xa) = true,
inference(equality_encoding,[status(esa)],[c53]) ).
cnf(t942,plain,
c_Natural_Oevalc(c_Option_Othe(sF2,tc_Com_Ocom),v_x,v_xa) = true,
inference(step,[status(thm)],[t28,t82]) ).
cnf(t943,plain,
c_Natural_Oevalc(sF3,v_x,v_xa) = true,
inference(step,[status(thm)],[t942,t97]) ).
cnf(t143,plain,
c_Natural_Oevalc(sF3,v_x,v_xa) = true,
inference(orient,[status(thm)],[t943]) ).
cnf(t949,plain,
sF4 = true,
inference(step,[status(thm)],[t948,t143]) ).
cnf(t175,plain,
true = sF4,
inference(orient,[status(thm)],[t949]) ).
cnf(f37,axiom,
( ~ c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(V_pn),tc_Com_Ocom),V_s0,V_s1)
| c_Natural_Oevalc(c_Com_Ocom_OBODY(V_pn),V_s0,V_s1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evalc_OBody_0) ).
fof(f37_nnf,plain,
! [V_pn,V_s0,V_s1] :
( ~ c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(V_pn),tc_Com_Ocom),V_s0,V_s1)
| c_Natural_Oevalc(c_Com_Ocom_OBODY(V_pn),V_s0,V_s1) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [V_pn,V_s0,V_s1] :
( ~ c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(V_pn),tc_Com_Ocom),V_s0,V_s1)
| c_Natural_Oevalc(c_Com_Ocom_OBODY(V_pn),V_s0,V_s1) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
( ~ c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(X0),tc_Com_Ocom),X1,X2)
| c_Natural_Oevalc(c_Com_Ocom_OBODY(X0),X1,X2) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(t64,plain,
ifeq(c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom),X2,X3),true,c_Natural_Oevalc(c_Com_Ocom_OBODY(X1),X2,X3),true) = true,
inference(equality_encoding,[status(esa)],[c37]) ).
cnf(t1112,plain,
ifeq(c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom),X2,X3),sF4,c_Natural_Oevalc(c_Com_Ocom_OBODY(X1),X2,X3),true) = true,
inference(step,[status(thm)],[t64,t175]) ).
cnf(t1113,plain,
ifeq(c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom),X2,X3),sF4,c_Natural_Oevalc(c_Com_Ocom_OBODY(X1),X2,X3),sF4) = true,
inference(step,[status(thm)],[t1112,t175]) ).
cnf(t1114,plain,
ifeq(c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom),X2,X3),sF4,c_Natural_Oevalc(c_Com_Ocom_OBODY(X1),X2,X3),sF4) = sF4,
inference(step,[status(thm)],[t1113,t175]) ).
cnf(t733,plain,
ifeq(c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom),X2,X3),sF4,c_Natural_Oevalc(c_Com_Ocom_OBODY(X1),X2,X3),sF4) = sF4,
inference(orient,[status(thm)],[t1114]) ).
cnf(t74,axiom,
sF0 = c_Com_Ocom_OBODY(v_pn),
introduced(definition) ).
cnf(t81,plain,
c_Com_Ocom_OBODY(v_pn) = sF0,
inference(orient,[status(thm)],[t74]) ).
cnf(t734,plain,
sF4 = ifeq(c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),X1,X2),sF4,c_Natural_Oevalc(sF0,X1,X2),sF4),
inference(cp,[status(thm)],[t733,t81]) ).
cnf(t1115,plain,
sF4 = ifeq(c_Natural_Oevalc(c_Option_Othe(sF2,tc_Com_Ocom),X1,X2),sF4,c_Natural_Oevalc(sF0,X1,X2),sF4),
inference(step,[status(thm)],[t734,t82]) ).
cnf(t1116,plain,
sF4 = ifeq(c_Natural_Oevalc(sF3,X1,X2),sF4,c_Natural_Oevalc(sF0,X1,X2),sF4),
inference(step,[status(thm)],[t1115,t97]) ).
cnf(t736,plain,
ifeq(c_Natural_Oevalc(sF3,X1,X2),sF4,c_Natural_Oevalc(sF0,X1,X2),sF4) = sF4,
inference(orient,[status(thm)],[t1116]) ).
cnf(f54,negated_conjecture,
~ c_Natural_Oevalc(c_Com_Ocom_OBODY(v_pn),v_x,v_xa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f54_nnf,plain,
~ c_Natural_Oevalc(c_Com_Ocom_OBODY(v_pn),v_x,v_xa),
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
~ c_Natural_Oevalc(c_Com_Ocom_OBODY(v_pn),v_x,v_xa),
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c54,plain,
~ c_Natural_Oevalc(c_Com_Ocom_OBODY(v_pn),v_x,v_xa),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(t12,plain,
c_Natural_Oevalc(c_Com_Ocom_OBODY(v_pn),v_x,v_xa) = false,
inference(equality_encoding,[status(esa)],[c54]) ).
cnf(t911,plain,
c_Natural_Oevalc(sF0,v_x,v_xa) = false,
inference(step,[status(thm)],[t12,t81]) ).
cnf(t98,plain,
c_Natural_Oevalc(sF0,v_x,v_xa) = false,
inference(orient,[status(thm)],[t911]) ).
cnf(t75,axiom,
sF1 = c_Natural_Oevalc(c_Com_Ocom_OBODY(v_pn),v_x,v_xa),
introduced(definition) ).
cnf(t912,plain,
sF1 = c_Natural_Oevalc(sF0,v_x,v_xa),
inference(step,[status(thm)],[t75,t81]) ).
cnf(t913,plain,
sF1 = false,
inference(step,[status(thm)],[t912,t98]) ).
cnf(t104,plain,
false = sF1,
inference(orient,[status(thm)],[t913]) ).
cnf(t928,plain,
c_Natural_Oevalc(sF0,v_x,v_xa) = sF1,
inference(step,[status(thm)],[t98,t104]) ).
cnf(t119,plain,
c_Natural_Oevalc(sF0,v_x,v_xa) = sF1,
inference(orient,[status(thm)],[t928]) ).
cnf(t737,plain,
sF4 = ifeq(c_Natural_Oevalc(sF3,v_x,v_xa),sF4,sF1,sF4),
inference(cp,[status(thm)],[t736,t119]) ).
cnf(t958,plain,
c_Natural_Oevalc(sF3,v_x,v_xa) = sF4,
inference(step,[status(thm)],[t143,t175]) ).
cnf(t192,plain,
c_Natural_Oevalc(sF3,v_x,v_xa) = sF4,
inference(orient,[status(thm)],[t958]) ).
cnf(t1117,plain,
sF4 = ifeq(sF4,sF4,sF1,sF4),
inference(step,[status(thm)],[t737,t192]) ).
cnf(t17,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t103,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t17]) ).
cnf(t1118,plain,
sF4 = sF1,
inference(step,[status(thm)],[t1117,t103]) ).
cnf(t739,plain,
sF4 = sF1,
inference(orient,[status(thm)],[t1118]) ).
cnf(t1129,plain,
true = sF1,
inference(step,[status(thm)],[t175,t739]) ).
cnf(t750,plain,
true = sF1,
inference(orient,[status(thm)],[t1129]) ).
cnf(f8,axiom,
c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_a_H,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_option_Osimps_I2_J_0) ).
fof(f8_nnf,plain,
! [T_a,V_a_H] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_a_H,T_a),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [T_a,V_a_H] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_a_H,T_a),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(f9,axiom,
c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Some__eq_1) ).
fof(f9_nnf,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(f14,axiom,
c_Option_Ooption_OSome(V_a_H,T_a) != c_Option_Ooption_ONone(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_option_Osimps_I3_J_0) ).
fof(f14_nnf,plain,
! [V_a_H,T_a] : c_Option_Ooption_OSome(V_a_H,T_a) != c_Option_Ooption_ONone(T_a),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [V_a_H,T_a] : c_Option_Ooption_OSome(V_a_H,T_a) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(f15,axiom,
c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__None__eq_1) ).
fof(f15_nnf,plain,
! [V_xa,T_a] : c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [V_xa,T_a] : c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(f26,axiom,
c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I13_J_0) ).
fof(f26_nnf,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(f30,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f30_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(f31,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f31_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(f33,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I12_J_0) ).
fof(f33_nnf,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X0,X1),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(f36,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I19_J_0) ).
fof(f36_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [V_pname_H] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(f44,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I49_J_0) ).
fof(f44_nnf,plain,
! [V_pname_H,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [V_pname_H,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c44,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OSemi(X1,X2),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(f45,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I48_J_0) ).
fof(f45_nnf,plain,
! [V_com1,V_com2,V_pname_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [V_com1,V_com2,V_pname_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c45,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OBODY(X2),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(f49,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I18_J_0) ).
fof(f49_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c49,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(X0),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c8,c9,c14,c15,c26,c30,c31,c33,c36,c44,c45,c49,c54]) ).
cnf(g0_0,plain,
sF1 != false,
inference(rw,[status(thm)],[goal_0,t750]) ).
cnf(g0_1,plain,
sF1 != sF1,
inference(rw,[status(thm)],[g0_0,t104]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV888-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Thu Sep 24 21:14:20 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 2.65/0.78 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.65/0.78 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------