%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV968-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n007.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:34 PM UTC 2026
% Result : Unsatisfiable 9.46s 1.82s
% Output : Proof 9.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 54
% Syntax : Number of formulae : 227 ( 227 unt; 0 def)
% Number of atoms : 227 ( 219 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 206 ( 206 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-5 aty)
% Number of functors : 20 ( 20 usr; 13 con; 0-5 aty)
% Number of variables : 752 ( 316 sgn 376 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f264,negated_conjecture,
~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,c_Type_Oty_OClass(v_C_H____)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f264_nnf,plain,
~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,c_Type_Oty_OClass(v_C_H____)),
inference(nnf_transformation,[status(thm)],[f264]) ).
fof(f264_sk,plain,
~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,c_Type_Oty_OClass(v_C_H____)),
inference(skolemisation,[status(esa)],[f264_nnf]) ).
cnf(c264,plain,
~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,c_Type_Oty_OClass(v_C_H____)),
inference(cnf_transformation,[status(esa)],[f264_sk]) ).
cnf(t51,plain,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,c_Type_Oty_OClass(v_C_H____)) = false,
inference(equality_encoding,[status(esa)],[c264]) ).
cnf(f232,axiom,
v_U____ = c_Type_Oty_OClass(v_C_H____),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_UClass_0) ).
fof(f232_nnf,plain,
v_U____ = c_Type_Oty_OClass(v_C_H____),
inference(nnf_transformation,[status(thm)],[f232]) ).
cnf(c232,plain,
v_U____ = c_Type_Oty_OClass(v_C_H____),
inference(cnf_transformation,[status(esa)],[f232_nnf]) ).
cnf(t1,plain,
c_Type_Oty_OClass(v_C_H____) = v_U____,
inference(equality_encoding,[status(esa)],[c232]) ).
cnf(t154,plain,
c_Type_Oty_OClass(v_C_H____) = v_U____,
inference(orient,[status(thm)],[t1]) ).
cnf(t151,axiom,
sF0 = c_Type_Oty_OClass(v_C_H____),
introduced(definition) ).
cnf(t324,plain,
sF0 = v_U____,
inference(step,[status(thm)],[t151,t154]) ).
cnf(t155,plain,
v_U____ = sF0,
inference(orient,[status(thm)],[t324]) ).
cnf(t325,plain,
c_Type_Oty_OClass(v_C_H____) = sF0,
inference(step,[status(thm)],[t154,t155]) ).
cnf(t156,plain,
c_Type_Oty_OClass(v_C_H____) = sF0,
inference(orient,[status(thm)],[t325]) ).
cnf(t328,plain,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,sF0) = false,
inference(step,[status(thm)],[t51,t156]) ).
cnf(f244,axiom,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_U____),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_wte_H_0) ).
fof(f244_nnf,plain,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_U____),
inference(nnf_transformation,[status(thm)],[f244]) ).
cnf(c244,plain,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_U____),
inference(cnf_transformation,[status(esa)],[f244_nnf]) ).
cnf(t41,plain,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_U____) = true,
inference(equality_encoding,[status(esa)],[c244]) ).
cnf(t327,plain,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,sF0) = true,
inference(step,[status(thm)],[t41,t155]) ).
cnf(t212,plain,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,sF0) = true,
inference(orient,[status(thm)],[t327]) ).
cnf(t329,plain,
true = false,
inference(step,[status(thm)],[t328,t212]) ).
cnf(t237,plain,
false = true,
inference(orient,[status(thm)],[t329]) ).
cnf(f10,axiom,
c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I175_J_0) ).
fof(f10_nnf,plain,
! [V_exp1_H,V_exp2_H,T_a,V_exp1,V_list1,V_list2,V_exp2] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [V_exp1_H,V_exp2_H,T_a,V_exp1,V_list1,V_list2,V_exp2] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != c_Expr_Oexp_OFAss(X3,X4,X5,X6,X2),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(f11,axiom,
c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I171_J_0) ).
fof(f11_nnf,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_exp1,V_list1,V_list2,V_exp2] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_exp1,V_list1,V_list2,V_exp2] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
c_Expr_Oexp_OCall(X0,X1,X2,X3) != c_Expr_Oexp_OFAss(X4,X5,X6,X7,X3),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(f12,axiom,
c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I29_J_0) ).
fof(f12_nnf,plain,
! [V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a,V_list] : c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a,V_list] : c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != c_Expr_Oexp_Onew(X5,X4),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(f13,axiom,
c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I28_J_0) ).
fof(f13_nnf,plain,
! [V_list,T_a,V_exp1_H,V_list1_H,V_list2_H,V_exp2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [V_list,T_a,V_exp1_H,V_list1_H,V_list2_H,V_exp2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
c_Expr_Oexp_Onew(X0,X1) != c_Expr_Oexp_OFAss(X2,X3,X4,X5,X1),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(f14,axiom,
c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I54_J_0) ).
fof(f14_nnf,plain,
! [V_list,V_exp,T_a,V_exp1_H,V_list1_H,V_list2_H,V_exp2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [V_list,V_exp,T_a,V_exp1_H,V_list1_H,V_list2_H,V_exp2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != c_Expr_Oexp_OFAss(X3,X4,X5,X6,X2),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(f19,axiom,
c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I174_J_0) ).
fof(f19_nnf,plain,
! [V_exp1,V_list1,V_list2,V_exp2,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [V_exp1,V_list1,V_list2,V_exp2,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != c_Expr_Oexp_OSeq(X5,X6,X4),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(f20,axiom,
c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I155_J_0) ).
fof(f20_nnf,plain,
! [V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != c_Expr_Oexp_OFAcc(X5,X6,X7,X4),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(f21,axiom,
c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I170_J_0) ).
fof(f21_nnf,plain,
! [V_exp1,V_list1,V_list2,V_exp2,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [V_exp1,V_list1,V_list2,V_exp2,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != c_Expr_Oexp_OCall(X5,X6,X7,X4),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(f22,axiom,
c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I55_J_0) ).
fof(f22_nnf,plain,
! [V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != c_Expr_Oexp_OCast(X5,X6,X4),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(f23,axiom,
c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I154_J_0) ).
fof(f23_nnf,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp1_H,V_list1_H,V_list2_H,V_exp2_H] : c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp1_H,V_list1_H,V_list2_H,V_exp2_H] : c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != c_Expr_Oexp_OFAss(X4,X5,X6,X7,X3),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(f148,axiom,
c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I61_J_0) ).
fof(f148_nnf,plain,
! [V_exp1_H,V_exp2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(nnf_transformation,[status(thm)],[f148]) ).
fof(f148_sk,plain,
! [V_exp1_H,V_exp2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(skolemisation,[status(esa)],[f148_nnf]) ).
cnf(c148,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != c_Expr_Oexp_OCast(X3,X4,X2),
inference(cnf_transformation,[status(esa)],[f148_sk]) ).
cnf(f149,axiom,
c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I157_J_0) ).
fof(f149_nnf,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
inference(nnf_transformation,[status(thm)],[f149]) ).
fof(f149_sk,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
inference(skolemisation,[status(esa)],[f149_nnf]) ).
cnf(c149,plain,
c_Expr_Oexp_OCall(X0,X1,X2,X3) != c_Expr_Oexp_OFAcc(X4,X5,X6,X3),
inference(cnf_transformation,[status(esa)],[f149_sk]) ).
cnf(f150,axiom,
c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I57_J_0) ).
fof(f150_nnf,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(nnf_transformation,[status(thm)],[f150]) ).
fof(f150_sk,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(skolemisation,[status(esa)],[f150_nnf]) ).
cnf(c150,plain,
c_Expr_Oexp_OCall(X0,X1,X2,X3) != c_Expr_Oexp_OCast(X4,X5,X3),
inference(cnf_transformation,[status(esa)],[f150_sk]) ).
cnf(f157,axiom,
c_Type_Oty_OVoid != c_Type_Oty_ONT,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I6_J_0) ).
fof(f157_nnf,plain,
c_Type_Oty_OVoid != c_Type_Oty_ONT,
inference(nnf_transformation,[status(thm)],[f157]) ).
fof(f157_sk,plain,
c_Type_Oty_OVoid != c_Type_Oty_ONT,
inference(skolemisation,[status(esa)],[f157_nnf]) ).
cnf(c157,plain,
c_Type_Oty_OVoid != c_Type_Oty_ONT,
inference(cnf_transformation,[status(esa)],[f157_sk]) ).
cnf(f158,axiom,
c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I27_J_0) ).
fof(f158_nnf,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list] : c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(nnf_transformation,[status(thm)],[f158]) ).
fof(f158_sk,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list] : c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(skolemisation,[status(esa)],[f158_nnf]) ).
cnf(c158,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != c_Expr_Oexp_Onew(X4,X3),
inference(cnf_transformation,[status(esa)],[f158_sk]) ).
cnf(f159,axiom,
c_Type_Oty_OBoolean != c_Type_Oty_ONT,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I12_J_0) ).
fof(f159_nnf,plain,
c_Type_Oty_OBoolean != c_Type_Oty_ONT,
inference(nnf_transformation,[status(thm)],[f159]) ).
fof(f159_sk,plain,
c_Type_Oty_OBoolean != c_Type_Oty_ONT,
inference(skolemisation,[status(esa)],[f159_nnf]) ).
cnf(c159,plain,
c_Type_Oty_OBoolean != c_Type_Oty_ONT,
inference(cnf_transformation,[status(esa)],[f159_sk]) ).
cnf(f163,axiom,
c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I26_J_0) ).
fof(f163_nnf,plain,
! [V_list,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(nnf_transformation,[status(thm)],[f163]) ).
fof(f163_sk,plain,
! [V_list,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(skolemisation,[status(esa)],[f163_nnf]) ).
cnf(c163,plain,
c_Expr_Oexp_Onew(X0,X1) != c_Expr_Oexp_OFAcc(X2,X3,X4,X1),
inference(cnf_transformation,[status(esa)],[f163_sk]) ).
cnf(f164,axiom,
c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I30_J_0) ).
fof(f164_nnf,plain,
! [V_list,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(nnf_transformation,[status(thm)],[f164]) ).
fof(f164_sk,plain,
! [V_list,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(skolemisation,[status(esa)],[f164_nnf]) ).
cnf(c164,plain,
c_Expr_Oexp_Onew(X0,X1) != c_Expr_Oexp_OCall(X2,X3,X4,X1),
inference(cnf_transformation,[status(esa)],[f164_sk]) ).
cnf(f165,axiom,
c_Type_Oty_OInteger != c_Type_Oty_OBoolean,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I11_J_0) ).
fof(f165_nnf,plain,
c_Type_Oty_OInteger != c_Type_Oty_OBoolean,
inference(nnf_transformation,[status(thm)],[f165]) ).
fof(f165_sk,plain,
c_Type_Oty_OInteger != c_Type_Oty_OBoolean,
inference(skolemisation,[status(esa)],[f165_nnf]) ).
cnf(c165,plain,
c_Type_Oty_OInteger != c_Type_Oty_OBoolean,
inference(cnf_transformation,[status(esa)],[f165_sk]) ).
cnf(f166,axiom,
c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I16_J_0) ).
fof(f166_nnf,plain,
! [V_list,T_a,V_list_H,V_exp_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a),
inference(nnf_transformation,[status(thm)],[f166]) ).
fof(f166_sk,plain,
! [V_list,T_a,V_list_H,V_exp_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a),
inference(skolemisation,[status(esa)],[f166_nnf]) ).
cnf(c166,plain,
c_Expr_Oexp_Onew(X0,X1) != c_Expr_Oexp_OCast(X2,X3,X1),
inference(cnf_transformation,[status(esa)],[f166_sk]) ).
cnf(f167,axiom,
c_Type_Oty_OVoid != c_Type_Oty_OInteger,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I4_J_0) ).
fof(f167_nnf,plain,
c_Type_Oty_OVoid != c_Type_Oty_OInteger,
inference(nnf_transformation,[status(thm)],[f167]) ).
fof(f167_sk,plain,
c_Type_Oty_OVoid != c_Type_Oty_OInteger,
inference(skolemisation,[status(esa)],[f167_nnf]) ).
cnf(c167,plain,
c_Type_Oty_OVoid != c_Type_Oty_OInteger,
inference(cnf_transformation,[status(esa)],[f167_sk]) ).
cnf(f176,axiom,
c_Type_Oty_ONT != c_Type_Oty_OBoolean,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I13_J_0) ).
fof(f176_nnf,plain,
c_Type_Oty_ONT != c_Type_Oty_OBoolean,
inference(nnf_transformation,[status(thm)],[f176]) ).
fof(f176_sk,plain,
c_Type_Oty_ONT != c_Type_Oty_OBoolean,
inference(skolemisation,[status(esa)],[f176_nnf]) ).
cnf(c176,plain,
c_Type_Oty_ONT != c_Type_Oty_OBoolean,
inference(cnf_transformation,[status(esa)],[f176_sk]) ).
cnf(f178,axiom,
c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I52_J_0) ).
fof(f178_nnf,plain,
! [V_list,V_exp,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(nnf_transformation,[status(thm)],[f178]) ).
fof(f178_sk,plain,
! [V_list,V_exp,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(skolemisation,[status(esa)],[f178_nnf]) ).
cnf(c178,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != c_Expr_Oexp_OFAcc(X3,X4,X5,X2),
inference(cnf_transformation,[status(esa)],[f178_sk]) ).
cnf(f179,axiom,
c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I56_J_0) ).
fof(f179_nnf,plain,
! [V_list,V_exp,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(nnf_transformation,[status(thm)],[f179]) ).
fof(f179_sk,plain,
! [V_list,V_exp,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(skolemisation,[status(esa)],[f179_nnf]) ).
cnf(c179,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != c_Expr_Oexp_OCall(X3,X4,X5,X2),
inference(cnf_transformation,[status(esa)],[f179_sk]) ).
cnf(f180,axiom,
c_Type_Oty_OInteger != c_Type_Oty_OVoid,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I5_J_0) ).
fof(f180_nnf,plain,
c_Type_Oty_OInteger != c_Type_Oty_OVoid,
inference(nnf_transformation,[status(thm)],[f180]) ).
fof(f180_sk,plain,
c_Type_Oty_OInteger != c_Type_Oty_OVoid,
inference(skolemisation,[status(esa)],[f180_nnf]) ).
cnf(c180,plain,
c_Type_Oty_OInteger != c_Type_Oty_OVoid,
inference(cnf_transformation,[status(esa)],[f180_sk]) ).
cnf(f182,axiom,
c_Type_Oty_OInteger != c_Type_Oty_ONT,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I16_J_0) ).
fof(f182_nnf,plain,
c_Type_Oty_OInteger != c_Type_Oty_ONT,
inference(nnf_transformation,[status(thm)],[f182]) ).
fof(f182_sk,plain,
c_Type_Oty_OInteger != c_Type_Oty_ONT,
inference(skolemisation,[status(esa)],[f182_nnf]) ).
cnf(c182,plain,
c_Type_Oty_OInteger != c_Type_Oty_ONT,
inference(cnf_transformation,[status(esa)],[f182_sk]) ).
cnf(f184,axiom,
c_Expr_Oexp_OCall(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I186_J_0) ).
fof(f184_nnf,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OCall(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f184]) ).
fof(f184_sk,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OCall(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f184_nnf]) ).
cnf(c184,plain,
c_Expr_Oexp_OCall(X0,X1,X2,X3) != c_Expr_Oexp_OSeq(X4,X5,X3),
inference(cnf_transformation,[status(esa)],[f184_sk]) ).
cnf(f185,axiom,
c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I17_J_0) ).
fof(f185_nnf,plain,
! [V_list_H,V_exp_H,T_a,V_list] : c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(nnf_transformation,[status(thm)],[f185]) ).
fof(f185_sk,plain,
! [V_list_H,V_exp_H,T_a,V_list] : c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(skolemisation,[status(esa)],[f185_nnf]) ).
cnf(c185,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != c_Expr_Oexp_Onew(X3,X2),
inference(cnf_transformation,[status(esa)],[f185_sk]) ).
cnf(f194,axiom,
c_Type_Oty_OVoid != c_Type_Oty_OBoolean,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I2_J_0) ).
fof(f194_nnf,plain,
c_Type_Oty_OVoid != c_Type_Oty_OBoolean,
inference(nnf_transformation,[status(thm)],[f194]) ).
fof(f194_sk,plain,
c_Type_Oty_OVoid != c_Type_Oty_OBoolean,
inference(skolemisation,[status(esa)],[f194_nnf]) ).
cnf(c194,plain,
c_Type_Oty_OVoid != c_Type_Oty_OBoolean,
inference(cnf_transformation,[status(esa)],[f194_sk]) ).
cnf(f197,axiom,
c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I160_J_0) ).
fof(f197_nnf,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f197]) ).
fof(f197_sk,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f197_nnf]) ).
cnf(c197,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != c_Expr_Oexp_OSeq(X4,X5,X3),
inference(cnf_transformation,[status(esa)],[f197_sk]) ).
cnf(f204,axiom,
c_Type_Oty_ONT != c_Type_Oty_OVoid,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I7_J_0) ).
fof(f204_nnf,plain,
c_Type_Oty_ONT != c_Type_Oty_OVoid,
inference(nnf_transformation,[status(thm)],[f204]) ).
fof(f204_sk,plain,
c_Type_Oty_ONT != c_Type_Oty_OVoid,
inference(skolemisation,[status(esa)],[f204_nnf]) ).
cnf(c204,plain,
c_Type_Oty_ONT != c_Type_Oty_OVoid,
inference(cnf_transformation,[status(esa)],[f204_sk]) ).
cnf(f205,axiom,
c_Type_Oty_OBoolean != c_Type_Oty_OInteger,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I10_J_0) ).
fof(f205_nnf,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OInteger,
inference(nnf_transformation,[status(thm)],[f205]) ).
fof(f205_sk,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OInteger,
inference(skolemisation,[status(esa)],[f205_nnf]) ).
cnf(c205,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OInteger,
inference(cnf_transformation,[status(esa)],[f205_sk]) ).
cnf(f210,axiom,
c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I156_J_0) ).
fof(f210_nnf,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(nnf_transformation,[status(thm)],[f210]) ).
fof(f210_sk,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(skolemisation,[status(esa)],[f210_nnf]) ).
cnf(c210,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != c_Expr_Oexp_OCall(X4,X5,X6,X3),
inference(cnf_transformation,[status(esa)],[f210_sk]) ).
cnf(f211,axiom,
c_Type_Oty_OBoolean != c_Type_Oty_OVoid,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I3_J_0) ).
fof(f211_nnf,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OVoid,
inference(nnf_transformation,[status(thm)],[f211]) ).
fof(f211_sk,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OVoid,
inference(skolemisation,[status(esa)],[f211_nnf]) ).
cnf(c211,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OVoid,
inference(cnf_transformation,[status(esa)],[f211_sk]) ).
cnf(f213,axiom,
c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I53_J_0) ).
fof(f213_nnf,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(nnf_transformation,[status(thm)],[f213]) ).
fof(f213_sk,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(skolemisation,[status(esa)],[f213_nnf]) ).
cnf(c213,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != c_Expr_Oexp_OCast(X4,X5,X3),
inference(cnf_transformation,[status(esa)],[f213_sk]) ).
cnf(f217,axiom,
c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I34_J_0) ).
fof(f217_nnf,plain,
! [V_list,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f217]) ).
fof(f217_sk,plain,
! [V_list,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f217_nnf]) ).
cnf(c217,plain,
c_Expr_Oexp_Onew(X0,X1) != c_Expr_Oexp_OSeq(X2,X3,X1),
inference(cnf_transformation,[status(esa)],[f217_sk]) ).
cnf(f218,axiom,
c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I60_J_0) ).
fof(f218_nnf,plain,
! [V_list,V_exp,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f218]) ).
fof(f218_sk,plain,
! [V_list,V_exp,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f218_nnf]) ).
cnf(c218,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != c_Expr_Oexp_OSeq(X3,X4,X2),
inference(cnf_transformation,[status(esa)],[f218_sk]) ).
cnf(f219,axiom,
c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I35_J_0) ).
fof(f219_nnf,plain,
! [V_exp1_H,V_exp2_H,T_a,V_list] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(nnf_transformation,[status(thm)],[f219]) ).
fof(f219_sk,plain,
! [V_exp1_H,V_exp2_H,T_a,V_list] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(skolemisation,[status(esa)],[f219_nnf]) ).
cnf(c219,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != c_Expr_Oexp_Onew(X3,X2),
inference(cnf_transformation,[status(esa)],[f219_sk]) ).
cnf(f225,axiom,
c_Type_Oty_ONT != c_Type_Oty_OInteger,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I17_J_0) ).
fof(f225_nnf,plain,
c_Type_Oty_ONT != c_Type_Oty_OInteger,
inference(nnf_transformation,[status(thm)],[f225]) ).
fof(f225_sk,plain,
c_Type_Oty_ONT != c_Type_Oty_OInteger,
inference(skolemisation,[status(esa)],[f225_nnf]) ).
cnf(c225,plain,
c_Type_Oty_ONT != c_Type_Oty_OInteger,
inference(cnf_transformation,[status(esa)],[f225_sk]) ).
cnf(f226,axiom,
c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I31_J_0) ).
fof(f226_nnf,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(nnf_transformation,[status(thm)],[f226]) ).
fof(f226_sk,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(skolemisation,[status(esa)],[f226_nnf]) ).
cnf(c226,plain,
c_Expr_Oexp_OCall(X0,X1,X2,X3) != c_Expr_Oexp_Onew(X4,X3),
inference(cnf_transformation,[status(esa)],[f226_sk]) ).
cnf(f228,axiom,
c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I161_J_0) ).
fof(f228_nnf,plain,
! [V_exp1_H,V_exp2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
inference(nnf_transformation,[status(thm)],[f228]) ).
fof(f228_sk,plain,
! [V_exp1_H,V_exp2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
inference(skolemisation,[status(esa)],[f228_nnf]) ).
cnf(c228,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != c_Expr_Oexp_OFAcc(X3,X4,X5,X2),
inference(cnf_transformation,[status(esa)],[f228_sk]) ).
cnf(f229,axiom,
c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OCall(V_exp,V_list1,V_list2,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I187_J_0) ).
fof(f229_nnf,plain,
! [V_exp1_H,V_exp2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OCall(V_exp,V_list1,V_list2,T_a),
inference(nnf_transformation,[status(thm)],[f229]) ).
fof(f229_sk,plain,
! [V_exp1_H,V_exp2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OCall(V_exp,V_list1,V_list2,T_a),
inference(skolemisation,[status(esa)],[f229_nnf]) ).
cnf(c229,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != c_Expr_Oexp_OCall(X3,X4,X5,X2),
inference(cnf_transformation,[status(esa)],[f229_sk]) ).
cnf(f231,axiom,
c_Type_Oty_OVoid != c_Type_Oty_OClass(V_list_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I8_J_0) ).
fof(f231_nnf,plain,
! [V_list_H] : c_Type_Oty_OVoid != c_Type_Oty_OClass(V_list_H),
inference(nnf_transformation,[status(thm)],[f231]) ).
fof(f231_sk,plain,
! [V_list_H] : c_Type_Oty_OVoid != c_Type_Oty_OClass(V_list_H),
inference(skolemisation,[status(esa)],[f231_nnf]) ).
cnf(c231,plain,
c_Type_Oty_OVoid != c_Type_Oty_OClass(X0),
inference(cnf_transformation,[status(esa)],[f231_sk]) ).
cnf(f233,axiom,
c_Type_Oty_ONT != c_Type_Oty_OClass(V_list_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I20_J_0) ).
fof(f233_nnf,plain,
! [V_list_H] : c_Type_Oty_ONT != c_Type_Oty_OClass(V_list_H),
inference(nnf_transformation,[status(thm)],[f233]) ).
fof(f233_sk,plain,
! [V_list_H] : c_Type_Oty_ONT != c_Type_Oty_OClass(V_list_H),
inference(skolemisation,[status(esa)],[f233_nnf]) ).
cnf(c233,plain,
c_Type_Oty_ONT != c_Type_Oty_OClass(X0),
inference(cnf_transformation,[status(esa)],[f233_sk]) ).
cnf(f235,axiom,
c_Type_Oty_OInteger != c_Type_Oty_OClass(V_list_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I18_J_0) ).
fof(f235_nnf,plain,
! [V_list_H] : c_Type_Oty_OInteger != c_Type_Oty_OClass(V_list_H),
inference(nnf_transformation,[status(thm)],[f235]) ).
fof(f235_sk,plain,
! [V_list_H] : c_Type_Oty_OInteger != c_Type_Oty_OClass(V_list_H),
inference(skolemisation,[status(esa)],[f235_nnf]) ).
cnf(c235,plain,
c_Type_Oty_OInteger != c_Type_Oty_OClass(X0),
inference(cnf_transformation,[status(esa)],[f235_sk]) ).
cnf(f236,axiom,
c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OBoolean,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I15_J_0) ).
fof(f236_nnf,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OBoolean,
inference(nnf_transformation,[status(thm)],[f236]) ).
fof(f236_sk,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OBoolean,
inference(skolemisation,[status(esa)],[f236_nnf]) ).
cnf(c236,plain,
c_Type_Oty_OClass(X0) != c_Type_Oty_OBoolean,
inference(cnf_transformation,[status(esa)],[f236_sk]) ).
cnf(f243,axiom,
c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OVoid,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I9_J_0) ).
fof(f243_nnf,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OVoid,
inference(nnf_transformation,[status(thm)],[f243]) ).
fof(f243_sk,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OVoid,
inference(skolemisation,[status(esa)],[f243_nnf]) ).
cnf(c243,plain,
c_Type_Oty_OClass(X0) != c_Type_Oty_OVoid,
inference(cnf_transformation,[status(esa)],[f243_sk]) ).
cnf(f249,axiom,
c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OInteger,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I19_J_0) ).
fof(f249_nnf,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OInteger,
inference(nnf_transformation,[status(thm)],[f249]) ).
fof(f249_sk,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OInteger,
inference(skolemisation,[status(esa)],[f249_nnf]) ).
cnf(c249,plain,
c_Type_Oty_OClass(X0) != c_Type_Oty_OInteger,
inference(cnf_transformation,[status(esa)],[f249_sk]) ).
cnf(f252,axiom,
c_Type_Oty_OBoolean != c_Type_Oty_OClass(V_list_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I14_J_0) ).
fof(f252_nnf,plain,
! [V_list_H] : c_Type_Oty_OBoolean != c_Type_Oty_OClass(V_list_H),
inference(nnf_transformation,[status(thm)],[f252]) ).
fof(f252_sk,plain,
! [V_list_H] : c_Type_Oty_OBoolean != c_Type_Oty_OClass(V_list_H),
inference(skolemisation,[status(esa)],[f252_nnf]) ).
cnf(c252,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OClass(X0),
inference(cnf_transformation,[status(esa)],[f252_sk]) ).
cnf(f253,axiom,
c_Type_Oty_OClass(V_list_H) != c_Type_Oty_ONT,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I21_J_0) ).
fof(f253_nnf,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_ONT,
inference(nnf_transformation,[status(thm)],[f253]) ).
fof(f253_sk,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_ONT,
inference(skolemisation,[status(esa)],[f253_nnf]) ).
cnf(c253,plain,
c_Type_Oty_OClass(X0) != c_Type_Oty_ONT,
inference(cnf_transformation,[status(esa)],[f253_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c10,c11,c12,c13,c14,c19,c20,c21,c22,c23,c148,c149,c150,c157,c158,c159,c163,c164,c165,c166,c167,c176,c178,c179,c180,c182,c184,c185,c194,c197,c204,c205,c210,c211,c213,c217,c218,c219,c225,c226,c228,c229,c231,c233,c235,c236,c243,c249,c252,c253,c264]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t237]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV968-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n007.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 : Thu Sep 24 21:23:37 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 9.46/1.82 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.46/1.82 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------