%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV957-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 : n002.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:33 PM UTC 2026
% Result : Unsatisfiable 7.25s 11.34s
% Output : Proof 7.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 44
% Syntax : Number of formulae : 187 ( 187 unt; 0 def)
% Number of atoms : 187 ( 179 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 166 ( 166 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-5 aty)
% Number of functors : 19 ( 19 usr; 13 con; 0-5 aty)
% Number of variables : 496 ( 208 sgn 248 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f253,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/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f253_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)],[f253]) ).
fof(f253_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)],[f253_nnf]) ).
cnf(c253,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)],[f253_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)],[c253]) ).
cnf(f219,axiom,
v_U____ = c_Type_Oty_OClass(v_C_H____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_UClass_0) ).
fof(f219_nnf,plain,
v_U____ = c_Type_Oty_OClass(v_C_H____),
inference(nnf_transformation,[status(thm)],[f219]) ).
cnf(c219,plain,
v_U____ = c_Type_Oty_OClass(v_C_H____),
inference(cnf_transformation,[status(esa)],[f219_nnf]) ).
cnf(t1,plain,
c_Type_Oty_OClass(v_C_H____) = v_U____,
inference(equality_encoding,[status(esa)],[c219]) ).
cnf(t128,plain,
c_Type_Oty_OClass(v_C_H____) = v_U____,
inference(orient,[status(thm)],[t1]) ).
cnf(t125,axiom,
sF0 = c_Type_Oty_OClass(v_C_H____),
introduced(definition) ).
cnf(t298,plain,
sF0 = v_U____,
inference(step,[status(thm)],[t125,t128]) ).
cnf(t129,plain,
v_U____ = sF0,
inference(orient,[status(thm)],[t298]) ).
cnf(t299,plain,
c_Type_Oty_OClass(v_C_H____) = sF0,
inference(step,[status(thm)],[t128,t129]) ).
cnf(t130,plain,
c_Type_Oty_OClass(v_C_H____) = sF0,
inference(orient,[status(thm)],[t299]) ).
cnf(t302,plain,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,sF0) = false,
inference(step,[status(thm)],[t51,t130]) ).
cnf(f230,axiom,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_U____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_wt_092_060_094isub_0621_H_0) ).
fof(f230_nnf,plain,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_U____),
inference(nnf_transformation,[status(thm)],[f230]) ).
cnf(c230,plain,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_U____),
inference(cnf_transformation,[status(esa)],[f230_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)],[c230]) ).
cnf(t301,plain,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,sF0) = true,
inference(step,[status(thm)],[t41,t129]) ).
cnf(t186,plain,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,sF0) = true,
inference(orient,[status(thm)],[t301]) ).
cnf(t303,plain,
true = false,
inference(step,[status(thm)],[t302,t186]) ).
cnf(t211,plain,
false = true,
inference(orient,[status(thm)],[t303]) ).
cnf(f128,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I61_J_0) ).
fof(f128_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)],[f128]) ).
fof(f128_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)],[f128_nnf]) ).
cnf(c128,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != c_Expr_Oexp_OCast(X3,X4,X2),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
cnf(f129,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I175_J_0) ).
fof(f129_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)],[f129]) ).
fof(f129_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)],[f129_nnf]) ).
cnf(c129,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != c_Expr_Oexp_OFAss(X3,X4,X5,X6,X2),
inference(cnf_transformation,[status(esa)],[f129_sk]) ).
cnf(f135,axiom,
c_Type_Oty_OVoid != c_Type_Oty_ONT,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I6_J_0) ).
fof(f135_nnf,plain,
c_Type_Oty_OVoid != c_Type_Oty_ONT,
inference(nnf_transformation,[status(thm)],[f135]) ).
fof(f135_sk,plain,
c_Type_Oty_OVoid != c_Type_Oty_ONT,
inference(skolemisation,[status(esa)],[f135_nnf]) ).
cnf(c135,plain,
c_Type_Oty_OVoid != c_Type_Oty_ONT,
inference(cnf_transformation,[status(esa)],[f135_sk]) ).
cnf(f136,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I27_J_0) ).
fof(f136_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)],[f136]) ).
fof(f136_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)],[f136_nnf]) ).
cnf(c136,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != c_Expr_Oexp_Onew(X4,X3),
inference(cnf_transformation,[status(esa)],[f136_sk]) ).
cnf(f137,axiom,
c_Type_Oty_OBoolean != c_Type_Oty_ONT,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I12_J_0) ).
fof(f137_nnf,plain,
c_Type_Oty_OBoolean != c_Type_Oty_ONT,
inference(nnf_transformation,[status(thm)],[f137]) ).
fof(f137_sk,plain,
c_Type_Oty_OBoolean != c_Type_Oty_ONT,
inference(skolemisation,[status(esa)],[f137_nnf]) ).
cnf(c137,plain,
c_Type_Oty_OBoolean != c_Type_Oty_ONT,
inference(cnf_transformation,[status(esa)],[f137_sk]) ).
cnf(f141,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I26_J_0) ).
fof(f141_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)],[f141]) ).
fof(f141_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)],[f141_nnf]) ).
cnf(c141,plain,
c_Expr_Oexp_Onew(X0,X1) != c_Expr_Oexp_OFAcc(X2,X3,X4,X1),
inference(cnf_transformation,[status(esa)],[f141_sk]) ).
cnf(f143,axiom,
c_Type_Oty_OInteger != c_Type_Oty_OBoolean,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I11_J_0) ).
fof(f143_nnf,plain,
c_Type_Oty_OInteger != c_Type_Oty_OBoolean,
inference(nnf_transformation,[status(thm)],[f143]) ).
fof(f143_sk,plain,
c_Type_Oty_OInteger != c_Type_Oty_OBoolean,
inference(skolemisation,[status(esa)],[f143_nnf]) ).
cnf(c143,plain,
c_Type_Oty_OInteger != c_Type_Oty_OBoolean,
inference(cnf_transformation,[status(esa)],[f143_sk]) ).
cnf(f144,axiom,
c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I16_J_0) ).
fof(f144_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)],[f144]) ).
fof(f144_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)],[f144_nnf]) ).
cnf(c144,plain,
c_Expr_Oexp_Onew(X0,X1) != c_Expr_Oexp_OCast(X2,X3,X1),
inference(cnf_transformation,[status(esa)],[f144_sk]) ).
cnf(f145,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I29_J_0) ).
fof(f145_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)],[f145]) ).
fof(f145_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)],[f145_nnf]) ).
cnf(c145,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != c_Expr_Oexp_Onew(X5,X4),
inference(cnf_transformation,[status(esa)],[f145_sk]) ).
cnf(f146,axiom,
c_Type_Oty_OVoid != c_Type_Oty_OInteger,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I4_J_0) ).
fof(f146_nnf,plain,
c_Type_Oty_OVoid != c_Type_Oty_OInteger,
inference(nnf_transformation,[status(thm)],[f146]) ).
fof(f146_sk,plain,
c_Type_Oty_OVoid != c_Type_Oty_OInteger,
inference(skolemisation,[status(esa)],[f146_nnf]) ).
cnf(c146,plain,
c_Type_Oty_OVoid != c_Type_Oty_OInteger,
inference(cnf_transformation,[status(esa)],[f146_sk]) ).
cnf(f148,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I28_J_0) ).
fof(f148_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)],[f148]) ).
fof(f148_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)],[f148_nnf]) ).
cnf(c148,plain,
c_Expr_Oexp_Onew(X0,X1) != c_Expr_Oexp_OFAss(X2,X3,X4,X5,X1),
inference(cnf_transformation,[status(esa)],[f148_sk]) ).
cnf(f154,axiom,
c_Type_Oty_ONT != c_Type_Oty_OBoolean,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I13_J_0) ).
fof(f154_nnf,plain,
c_Type_Oty_ONT != c_Type_Oty_OBoolean,
inference(nnf_transformation,[status(thm)],[f154]) ).
fof(f154_sk,plain,
c_Type_Oty_ONT != c_Type_Oty_OBoolean,
inference(skolemisation,[status(esa)],[f154_nnf]) ).
cnf(c154,plain,
c_Type_Oty_ONT != c_Type_Oty_OBoolean,
inference(cnf_transformation,[status(esa)],[f154_sk]) ).
cnf(f157,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I52_J_0) ).
fof(f157_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)],[f157]) ).
fof(f157_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)],[f157_nnf]) ).
cnf(c157,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != c_Expr_Oexp_OFAcc(X3,X4,X5,X2),
inference(cnf_transformation,[status(esa)],[f157_sk]) ).
cnf(f158,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I54_J_0) ).
fof(f158_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)],[f158]) ).
fof(f158_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)],[f158_nnf]) ).
cnf(c158,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != c_Expr_Oexp_OFAss(X3,X4,X5,X6,X2),
inference(cnf_transformation,[status(esa)],[f158_sk]) ).
cnf(f159,axiom,
c_Type_Oty_OInteger != c_Type_Oty_OVoid,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I5_J_0) ).
fof(f159_nnf,plain,
c_Type_Oty_OInteger != c_Type_Oty_OVoid,
inference(nnf_transformation,[status(thm)],[f159]) ).
fof(f159_sk,plain,
c_Type_Oty_OInteger != c_Type_Oty_OVoid,
inference(skolemisation,[status(esa)],[f159_nnf]) ).
cnf(c159,plain,
c_Type_Oty_OInteger != c_Type_Oty_OVoid,
inference(cnf_transformation,[status(esa)],[f159_sk]) ).
cnf(f161,axiom,
c_Type_Oty_OInteger != c_Type_Oty_ONT,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I16_J_0) ).
fof(f161_nnf,plain,
c_Type_Oty_OInteger != c_Type_Oty_ONT,
inference(nnf_transformation,[status(thm)],[f161]) ).
fof(f161_sk,plain,
c_Type_Oty_OInteger != c_Type_Oty_ONT,
inference(skolemisation,[status(esa)],[f161_nnf]) ).
cnf(c161,plain,
c_Type_Oty_OInteger != c_Type_Oty_ONT,
inference(cnf_transformation,[status(esa)],[f161_sk]) ).
cnf(f163,axiom,
c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I17_J_0) ).
fof(f163_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)],[f163]) ).
fof(f163_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)],[f163_nnf]) ).
cnf(c163,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != c_Expr_Oexp_Onew(X3,X2),
inference(cnf_transformation,[status(esa)],[f163_sk]) ).
cnf(f172,axiom,
c_Type_Oty_OVoid != c_Type_Oty_OBoolean,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I2_J_0) ).
fof(f172_nnf,plain,
c_Type_Oty_OVoid != c_Type_Oty_OBoolean,
inference(nnf_transformation,[status(thm)],[f172]) ).
fof(f172_sk,plain,
c_Type_Oty_OVoid != c_Type_Oty_OBoolean,
inference(skolemisation,[status(esa)],[f172_nnf]) ).
cnf(c172,plain,
c_Type_Oty_OVoid != c_Type_Oty_OBoolean,
inference(cnf_transformation,[status(esa)],[f172_sk]) ).
cnf(f175,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I160_J_0) ).
fof(f175_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)],[f175]) ).
fof(f175_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)],[f175_nnf]) ).
cnf(c175,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != c_Expr_Oexp_OSeq(X4,X5,X3),
inference(cnf_transformation,[status(esa)],[f175_sk]) ).
cnf(f185,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I174_J_0) ).
fof(f185_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)],[f185]) ).
fof(f185_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)],[f185_nnf]) ).
cnf(c185,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != c_Expr_Oexp_OSeq(X5,X6,X4),
inference(cnf_transformation,[status(esa)],[f185_sk]) ).
cnf(f188,axiom,
c_Type_Oty_ONT != c_Type_Oty_OVoid,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I7_J_0) ).
fof(f188_nnf,plain,
c_Type_Oty_ONT != c_Type_Oty_OVoid,
inference(nnf_transformation,[status(thm)],[f188]) ).
fof(f188_sk,plain,
c_Type_Oty_ONT != c_Type_Oty_OVoid,
inference(skolemisation,[status(esa)],[f188_nnf]) ).
cnf(c188,plain,
c_Type_Oty_ONT != c_Type_Oty_OVoid,
inference(cnf_transformation,[status(esa)],[f188_sk]) ).
cnf(f189,axiom,
c_Type_Oty_OBoolean != c_Type_Oty_OInteger,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I10_J_0) ).
fof(f189_nnf,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OInteger,
inference(nnf_transformation,[status(thm)],[f189]) ).
fof(f189_sk,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OInteger,
inference(skolemisation,[status(esa)],[f189_nnf]) ).
cnf(c189,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OInteger,
inference(cnf_transformation,[status(esa)],[f189_sk]) ).
cnf(f191,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I155_J_0) ).
fof(f191_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)],[f191]) ).
fof(f191_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)],[f191_nnf]) ).
cnf(c191,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != c_Expr_Oexp_OFAcc(X5,X6,X7,X4),
inference(cnf_transformation,[status(esa)],[f191_sk]) ).
cnf(f194,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I55_J_0) ).
fof(f194_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)],[f194]) ).
fof(f194_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)],[f194_nnf]) ).
cnf(c194,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != c_Expr_Oexp_OCast(X5,X6,X4),
inference(cnf_transformation,[status(esa)],[f194_sk]) ).
cnf(f197,axiom,
c_Type_Oty_OBoolean != c_Type_Oty_OVoid,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I3_J_0) ).
fof(f197_nnf,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OVoid,
inference(nnf_transformation,[status(thm)],[f197]) ).
fof(f197_sk,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OVoid,
inference(skolemisation,[status(esa)],[f197_nnf]) ).
cnf(c197,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OVoid,
inference(cnf_transformation,[status(esa)],[f197_sk]) ).
cnf(f199,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I53_J_0) ).
fof(f199_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)],[f199]) ).
fof(f199_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)],[f199_nnf]) ).
cnf(c199,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != c_Expr_Oexp_OCast(X4,X5,X3),
inference(cnf_transformation,[status(esa)],[f199_sk]) ).
cnf(f203,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I154_J_0) ).
fof(f203_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)],[f203]) ).
fof(f203_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)],[f203_nnf]) ).
cnf(c203,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != c_Expr_Oexp_OFAss(X4,X5,X6,X7,X3),
inference(cnf_transformation,[status(esa)],[f203_sk]) ).
cnf(f205,axiom,
c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I34_J_0) ).
fof(f205_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)],[f205]) ).
fof(f205_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)],[f205_nnf]) ).
cnf(c205,plain,
c_Expr_Oexp_Onew(X0,X1) != c_Expr_Oexp_OSeq(X2,X3,X1),
inference(cnf_transformation,[status(esa)],[f205_sk]) ).
cnf(f206,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I60_J_0) ).
fof(f206_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)],[f206]) ).
fof(f206_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)],[f206_nnf]) ).
cnf(c206,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != c_Expr_Oexp_OSeq(X3,X4,X2),
inference(cnf_transformation,[status(esa)],[f206_sk]) ).
cnf(f207,axiom,
c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I35_J_0) ).
fof(f207_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)],[f207]) ).
fof(f207_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)],[f207_nnf]) ).
cnf(c207,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != c_Expr_Oexp_Onew(X3,X2),
inference(cnf_transformation,[status(esa)],[f207_sk]) ).
cnf(f213,axiom,
c_Type_Oty_ONT != c_Type_Oty_OInteger,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I17_J_0) ).
fof(f213_nnf,plain,
c_Type_Oty_ONT != c_Type_Oty_OInteger,
inference(nnf_transformation,[status(thm)],[f213]) ).
fof(f213_sk,plain,
c_Type_Oty_ONT != c_Type_Oty_OInteger,
inference(skolemisation,[status(esa)],[f213_nnf]) ).
cnf(c213,plain,
c_Type_Oty_ONT != c_Type_Oty_OInteger,
inference(cnf_transformation,[status(esa)],[f213_sk]) ).
cnf(f216,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/sandbox/benchmark/theBenchmark.p',cls_exp_Osimps_I161_J_0) ).
fof(f216_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)],[f216]) ).
fof(f216_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)],[f216_nnf]) ).
cnf(c216,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != c_Expr_Oexp_OFAcc(X3,X4,X5,X2),
inference(cnf_transformation,[status(esa)],[f216_sk]) ).
cnf(f218,axiom,
c_Type_Oty_OVoid != c_Type_Oty_OClass(V_list_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I8_J_0) ).
fof(f218_nnf,plain,
! [V_list_H] : c_Type_Oty_OVoid != c_Type_Oty_OClass(V_list_H),
inference(nnf_transformation,[status(thm)],[f218]) ).
fof(f218_sk,plain,
! [V_list_H] : c_Type_Oty_OVoid != c_Type_Oty_OClass(V_list_H),
inference(skolemisation,[status(esa)],[f218_nnf]) ).
cnf(c218,plain,
c_Type_Oty_OVoid != c_Type_Oty_OClass(X0),
inference(cnf_transformation,[status(esa)],[f218_sk]) ).
cnf(f220,axiom,
c_Type_Oty_ONT != c_Type_Oty_OClass(V_list_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I20_J_0) ).
fof(f220_nnf,plain,
! [V_list_H] : c_Type_Oty_ONT != c_Type_Oty_OClass(V_list_H),
inference(nnf_transformation,[status(thm)],[f220]) ).
fof(f220_sk,plain,
! [V_list_H] : c_Type_Oty_ONT != c_Type_Oty_OClass(V_list_H),
inference(skolemisation,[status(esa)],[f220_nnf]) ).
cnf(c220,plain,
c_Type_Oty_ONT != c_Type_Oty_OClass(X0),
inference(cnf_transformation,[status(esa)],[f220_sk]) ).
cnf(f221,axiom,
c_Type_Oty_OInteger != c_Type_Oty_OClass(V_list_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I18_J_0) ).
fof(f221_nnf,plain,
! [V_list_H] : c_Type_Oty_OInteger != c_Type_Oty_OClass(V_list_H),
inference(nnf_transformation,[status(thm)],[f221]) ).
fof(f221_sk,plain,
! [V_list_H] : c_Type_Oty_OInteger != c_Type_Oty_OClass(V_list_H),
inference(skolemisation,[status(esa)],[f221_nnf]) ).
cnf(c221,plain,
c_Type_Oty_OInteger != c_Type_Oty_OClass(X0),
inference(cnf_transformation,[status(esa)],[f221_sk]) ).
cnf(f222,axiom,
c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OBoolean,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I15_J_0) ).
fof(f222_nnf,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OBoolean,
inference(nnf_transformation,[status(thm)],[f222]) ).
fof(f222_sk,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OBoolean,
inference(skolemisation,[status(esa)],[f222_nnf]) ).
cnf(c222,plain,
c_Type_Oty_OClass(X0) != c_Type_Oty_OBoolean,
inference(cnf_transformation,[status(esa)],[f222_sk]) ).
cnf(f229,axiom,
c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OVoid,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I9_J_0) ).
fof(f229_nnf,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OVoid,
inference(nnf_transformation,[status(thm)],[f229]) ).
fof(f229_sk,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OVoid,
inference(skolemisation,[status(esa)],[f229_nnf]) ).
cnf(c229,plain,
c_Type_Oty_OClass(X0) != c_Type_Oty_OVoid,
inference(cnf_transformation,[status(esa)],[f229_sk]) ).
cnf(f235,axiom,
c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OInteger,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I19_J_0) ).
fof(f235_nnf,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OInteger,
inference(nnf_transformation,[status(thm)],[f235]) ).
fof(f235_sk,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OInteger,
inference(skolemisation,[status(esa)],[f235_nnf]) ).
cnf(c235,plain,
c_Type_Oty_OClass(X0) != c_Type_Oty_OInteger,
inference(cnf_transformation,[status(esa)],[f235_sk]) ).
cnf(f239,axiom,
c_Type_Oty_OBoolean != c_Type_Oty_OClass(V_list_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I14_J_0) ).
fof(f239_nnf,plain,
! [V_list_H] : c_Type_Oty_OBoolean != c_Type_Oty_OClass(V_list_H),
inference(nnf_transformation,[status(thm)],[f239]) ).
fof(f239_sk,plain,
! [V_list_H] : c_Type_Oty_OBoolean != c_Type_Oty_OClass(V_list_H),
inference(skolemisation,[status(esa)],[f239_nnf]) ).
cnf(c239,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OClass(X0),
inference(cnf_transformation,[status(esa)],[f239_sk]) ).
cnf(f241,axiom,
c_Type_Oty_OClass(V_list_H) != c_Type_Oty_ONT,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ty_Osimps_I21_J_0) ).
fof(f241_nnf,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_ONT,
inference(nnf_transformation,[status(thm)],[f241]) ).
fof(f241_sk,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_ONT,
inference(skolemisation,[status(esa)],[f241_nnf]) ).
cnf(c241,plain,
c_Type_Oty_OClass(X0) != c_Type_Oty_ONT,
inference(cnf_transformation,[status(esa)],[f241_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c128,c129,c135,c136,c137,c141,c143,c144,c145,c146,c148,c154,c157,c158,c159,c161,c163,c172,c175,c185,c188,c189,c191,c194,c197,c199,c203,c205,c206,c207,c213,c216,c218,c220,c221,c222,c229,c235,c239,c241,c253]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t211]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV957-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/10.37 % Computer : n002.cluster.edu
% 0.11/10.37 % Model : x86_64 x86_64
% 0.11/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.37 % Memory : 8046.5625MB
% 0.11/10.37 % OS : Linux 6.8.0-71-generic
% 0.11/10.37 % CPULimit : 300
% 0.11/10.37 % WCLimit : 300
% 0.11/10.37 % DateTime : Thu Sep 24 21:26:46 UTC 2026
% 0.11/10.37 % CPUTime :
% 0.11/10.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 7.25/11.34 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.25/11.34 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------