%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV252-2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.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:12:38 PM UTC 2026
% Result : Unsatisfiable 96.48s 13.03s
% Output : Proof 96.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 26
% Syntax : Number of formulae : 316 ( 276 unt; 0 def)
% Number of atoms : 368 ( 268 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 119 ( 67 ~; 52 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 12 con; 0-4 aty)
% Number of variables : 492 ( 75 sgn 84 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t19,axiom,
sFlat0 = c_insert(v_X,v_H,tc_Message_Omsg),
introduced(definition) ).
cnf(t96,plain,
c_insert(v_X,v_H,tc_Message_Omsg) = sFlat0,
inference(orient,[status(thm)],[t19]) ).
cnf(t20,axiom,
sFlat1 = c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),
introduced(definition) ).
cnf(t75,plain,
c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)) = sFlat1,
inference(orient,[status(thm)],[t20]) ).
cnf(t46903,plain,
c_Message_Oparts(sFlat0) = sFlat1,
inference(step,[status(thm)],[t75,t96]) ).
cnf(t100,plain,
c_Message_Oparts(sFlat0) = sFlat1,
inference(rw,[status(thm)],[t46903]) ).
cnf(t106,plain,
c_Message_Oparts(sFlat0) = sFlat1,
inference(orient,[status(thm)],[t100]) ).
cnf(f17,axiom,
( V_A = V_B
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_Osubset__antisym_0) ).
fof(f17_nnf,plain,
! [V_B,V_A,T_a] :
( V_A = V_B
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [V_B,V_A,T_a] :
( V_A = V_B
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( X1 = X0
| ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(t16,plain,
ifeq(c_lessequals(X1,X2,tc_set(X3)),true,ifeq(c_lessequals(X2,X1,tc_set(X3)),true,X2,X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t28,plain,
ifeq(c_lessequals(X1,X2,tc_set(X3)),true,ifeq(c_lessequals(X2,X1,tc_set(X3)),true,X2,X1),X1) = X1,
inference(orient,[status(thm)],[t16]) ).
cnf(f13,axiom,
( c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a))
| ~ c_lessequals(V_A,V_C,tc_set(T_a))
| ~ c_lessequals(V_B,V_C,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OUn__subset__iff_2) ).
fof(f13_nnf,plain,
! [V_B,V_C,T_a,V_A] :
( c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a))
| ~ c_lessequals(V_A,V_C,tc_set(T_a))
| ~ c_lessequals(V_B,V_C,tc_set(T_a)) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [V_B,V_C,T_a,V_A] :
( c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a))
| ~ c_lessequals(V_A,V_C,tc_set(T_a))
| ~ c_lessequals(V_B,V_C,tc_set(T_a)) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( c_lessequals(c_union(X3,X0,X2),X1,tc_set(X2))
| ~ c_lessequals(X3,X1,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t18,plain,
ifeq(c_lessequals(X1,X2,tc_set(X3)),true,ifeq(c_lessequals(X4,X2,tc_set(X3)),true,c_lessequals(c_union(X4,X1,X3),X2,tc_set(X3)),true),true) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t29,plain,
ifeq(c_lessequals(X1,X2,tc_set(X3)),true,ifeq(c_lessequals(X4,X2,tc_set(X3)),true,c_lessequals(c_union(X4,X1,X3),X2,tc_set(X3)),true),true) = true,
inference(orient,[status(thm)],[t18]) ).
cnf(f10,axiom,
c_union(V_A,c_minus(V_B,V_A,tc_set(T_a)),T_a) = c_union(V_A,V_B,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OUn__Diff__cancel_0) ).
fof(f10_nnf,plain,
! [V_A,V_B,T_a] : c_union(V_A,c_minus(V_B,V_A,tc_set(T_a)),T_a) = c_union(V_A,V_B,T_a),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [V_A,V_B,T_a] : c_union(V_A,c_minus(V_B,V_A,tc_set(T_a)),T_a) = c_union(V_A,V_B,T_a),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
c_union(X0,c_minus(X1,X0,tc_set(X2)),X2) = c_union(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t7,plain,
c_union(X1,c_minus(X2,X1,tc_set(X3)),X3) = c_union(X1,X2,X3),
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t81,plain,
c_union(X1,c_minus(X2,X1,tc_set(X3)),X3) = c_union(X1,X2,X3),
inference(orient,[status(thm)],[t7]) ).
cnf(t84,plain,
true = ifeq(c_lessequals(c_minus(X1,X2,tc_set(X3)),X4,tc_set(X3)),true,ifeq(c_lessequals(X2,X4,tc_set(X3)),true,c_lessequals(c_union(X2,X1,X3),X4,tc_set(X3)),true),true),
inference(cp,[status(thm)],[t29,t81]) ).
cnf(t9038,plain,
ifeq(c_lessequals(c_minus(X1,X2,tc_set(X3)),X4,tc_set(X3)),true,ifeq(c_lessequals(X2,X4,tc_set(X3)),true,c_lessequals(c_union(X2,X1,X3),X4,tc_set(X3)),true),true) = true,
inference(orient,[status(thm)],[t84]) ).
cnf(f11,axiom,
( c_lessequals(V_A,V_C,tc_set(T_a))
| ~ c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OUn__subset__iff_0) ).
fof(f11_nnf,plain,
! [V_A,V_B,T_a,V_C] :
( c_lessequals(V_A,V_C,tc_set(T_a))
| ~ c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a)) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [V_A,V_B,T_a,V_C] :
( c_lessequals(V_A,V_C,tc_set(T_a))
| ~ c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a)) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( c_lessequals(X0,X3,tc_set(X2))
| ~ c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2)) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t14,plain,
ifeq(c_lessequals(c_union(X1,X2,X3),X4,tc_set(X3)),true,c_lessequals(X1,X4,tc_set(X3)),true) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t34,plain,
ifeq(c_lessequals(c_union(X1,X2,X3),X4,tc_set(X3)),true,c_lessequals(X1,X4,tc_set(X3)),true) = true,
inference(orient,[status(thm)],[t14]) ).
cnf(f8,axiom,
( c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Orderings_Oorder__class_Oaxioms__1_0) ).
fof(f8_nnf,plain,
! [T_a,V_x] :
( c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [T_a,V_x] :
( c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( c_lessequals(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t6,plain,
ifeq(class_Orderings_Oorder(X1),true,c_lessequals(X2,X2,X1),true) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t38,plain,
ifeq(class_Orderings_Oorder(X1),true,c_lessequals(X2,X2,X1),true) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(f18,axiom,
class_Orderings_Oorder(tc_set(T_1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_set_2) ).
fof(f18_nnf,plain,
! [T_1] : class_Orderings_Oorder(tc_set(T_1)),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [T_1] : class_Orderings_Oorder(tc_set(T_1)),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
class_Orderings_Oorder(tc_set(X0)),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(t0,plain,
class_Orderings_Oorder(tc_set(X1)) = true,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t42,plain,
class_Orderings_Oorder(tc_set(X1)) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t43,plain,
true = ifeq(true,true,c_lessequals(X1,X1,tc_set(X2)),true),
inference(cp,[status(thm)],[t38,t42]) ).
cnf(t3,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t27,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t3]) ).
cnf(t46910,plain,
true = c_lessequals(X1,X1,tc_set(X2)),
inference(step,[status(thm)],[t43,t27]) ).
cnf(t119,plain,
c_lessequals(X1,X1,tc_set(X2)) = true,
inference(orient,[status(thm)],[t46910]) ).
cnf(t123,plain,
true = ifeq(true,true,c_lessequals(X1,c_union(X1,X2,X3),tc_set(X3)),true),
inference(cp,[status(thm)],[t34,t119]) ).
cnf(t46915,plain,
true = c_lessequals(X1,c_union(X1,X2,X3),tc_set(X3)),
inference(step,[status(thm)],[t123,t27]) ).
cnf(t169,plain,
c_lessequals(X1,c_union(X1,X2,X3),tc_set(X3)) = true,
inference(orient,[status(thm)],[t46915]) ).
cnf(f9,axiom,
c_union(c_minus(V_B,V_A,tc_set(T_a)),V_A,T_a) = c_union(V_B,V_A,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OUn__Diff__cancel2_0) ).
fof(f9_nnf,plain,
! [V_B,V_A,T_a] : c_union(c_minus(V_B,V_A,tc_set(T_a)),V_A,T_a) = c_union(V_B,V_A,T_a),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [V_B,V_A,T_a] : c_union(c_minus(V_B,V_A,tc_set(T_a)),V_A,T_a) = c_union(V_B,V_A,T_a),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
c_union(c_minus(X0,X1,tc_set(X2)),X1,X2) = c_union(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t8,plain,
c_union(c_minus(X1,X2,tc_set(X3)),X2,X3) = c_union(X1,X2,X3),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t85,plain,
c_union(c_minus(X1,X2,tc_set(X3)),X2,X3) = c_union(X1,X2,X3),
inference(orient,[status(thm)],[t8]) ).
cnf(t174,plain,
true = c_lessequals(c_minus(X1,X2,tc_set(X3)),c_union(X1,X2,X3),tc_set(X3)),
inference(cp,[status(thm)],[t169,t85]) ).
cnf(t3344,plain,
c_lessequals(c_minus(X1,X2,tc_set(X3)),c_union(X1,X2,X3),tc_set(X3)) = true,
inference(orient,[status(thm)],[t174]) ).
cnf(t9039,plain,
true = ifeq(true,true,ifeq(c_lessequals(X1,c_union(X2,X1,X3),tc_set(X3)),true,c_lessequals(c_union(X1,X2,X3),c_union(X2,X1,X3),tc_set(X3)),true),true),
inference(cp,[status(thm)],[t9038,t3344]) ).
cnf(t48724,plain,
true = ifeq(c_lessequals(X1,c_union(X2,X1,X3),tc_set(X3)),true,c_lessequals(c_union(X1,X2,X3),c_union(X2,X1,X3),tc_set(X3)),true),
inference(step,[status(thm)],[t9039,t27]) ).
cnf(f12,axiom,
( c_lessequals(V_B,V_C,tc_set(T_a))
| ~ c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OUn__subset__iff_1) ).
fof(f12_nnf,plain,
! [V_A,V_B,T_a,V_C] :
( c_lessequals(V_B,V_C,tc_set(T_a))
| ~ c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a)) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [V_A,V_B,T_a,V_C] :
( c_lessequals(V_B,V_C,tc_set(T_a))
| ~ c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a)) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( c_lessequals(X1,X3,tc_set(X2))
| ~ c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2)) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t15,plain,
ifeq(c_lessequals(c_union(X1,X2,X3),X4,tc_set(X3)),true,c_lessequals(X2,X4,tc_set(X3)),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t33,plain,
ifeq(c_lessequals(c_union(X1,X2,X3),X4,tc_set(X3)),true,c_lessequals(X2,X4,tc_set(X3)),true) = true,
inference(orient,[status(thm)],[t15]) ).
cnf(t125,plain,
true = ifeq(true,true,c_lessequals(X1,c_union(X2,X1,X3),tc_set(X3)),true),
inference(cp,[status(thm)],[t33,t119]) ).
cnf(t46921,plain,
true = c_lessequals(X1,c_union(X2,X1,X3),tc_set(X3)),
inference(step,[status(thm)],[t125,t27]) ).
cnf(t206,plain,
c_lessequals(X1,c_union(X2,X1,X3),tc_set(X3)) = true,
inference(orient,[status(thm)],[t46921]) ).
cnf(t48725,plain,
true = ifeq(true,true,c_lessequals(c_union(X1,X2,X3),c_union(X2,X1,X3),tc_set(X3)),true),
inference(step,[status(thm)],[t48724,t206]) ).
cnf(t48726,plain,
true = c_lessequals(c_union(X1,X2,X3),c_union(X2,X1,X3),tc_set(X3)),
inference(step,[status(thm)],[t48725,t27]) ).
cnf(t29506,plain,
c_lessequals(c_union(X1,X2,X3),c_union(X2,X1,X3),tc_set(X3)) = true,
inference(orient,[status(thm)],[t48726]) ).
cnf(t29553,plain,
c_union(X1,X2,X3) = ifeq(true,true,ifeq(c_lessequals(c_union(X2,X1,X3),c_union(X1,X2,X3),tc_set(X3)),true,c_union(X2,X1,X3),c_union(X1,X2,X3)),c_union(X1,X2,X3)),
inference(cp,[status(thm)],[t28,t29506]) ).
cnf(t48727,plain,
c_union(X1,X2,X3) = ifeq(c_lessequals(c_union(X2,X1,X3),c_union(X1,X2,X3),tc_set(X3)),true,c_union(X2,X1,X3),c_union(X1,X2,X3)),
inference(step,[status(thm)],[t29553,t27]) ).
cnf(t48728,plain,
c_union(X1,X2,X3) = ifeq(true,true,c_union(X2,X1,X3),c_union(X1,X2,X3)),
inference(step,[status(thm)],[t48727,t29506]) ).
cnf(t48729,plain,
c_union(X1,X2,X3) = c_union(X2,X1,X3),
inference(step,[status(thm)],[t48728,t27]) ).
cnf(t29560,plain,
c_union(X1,X2,X3) = c_union(X2,X1,X3),
inference(orient,[status(thm)],[t48729]) ).
cnf(f7,axiom,
c_Message_Oparts(c_Message_Osynth(V_H)) = c_union(c_Message_Oparts(V_H),c_Message_Osynth(V_H),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Message_Oparts__synth_0) ).
fof(f7_nnf,plain,
! [V_H] : c_Message_Oparts(c_Message_Osynth(V_H)) = c_union(c_Message_Oparts(V_H),c_Message_Osynth(V_H),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [V_H] : c_Message_Oparts(c_Message_Osynth(V_H)) = c_union(c_Message_Oparts(V_H),c_Message_Osynth(V_H),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
c_Message_Oparts(c_Message_Osynth(X0)) = c_union(c_Message_Oparts(X0),c_Message_Osynth(X0),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t5,plain,
c_union(c_Message_Oparts(X1),c_Message_Osynth(X1),tc_Message_Omsg) = c_Message_Oparts(c_Message_Osynth(X1)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t69,plain,
c_union(c_Message_Oparts(X1),c_Message_Osynth(X1),tc_Message_Omsg) = c_Message_Oparts(c_Message_Osynth(X1)),
inference(orient,[status(thm)],[t5]) ).
cnf(f4,axiom,
c_Message_Oparts(c_Message_Oanalz(V_H)) = c_Message_Oparts(V_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Message_Oparts__analz_0) ).
fof(f4_nnf,plain,
! [V_H] : c_Message_Oparts(c_Message_Oanalz(V_H)) = c_Message_Oparts(V_H),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [V_H] : c_Message_Oparts(c_Message_Oanalz(V_H)) = c_Message_Oparts(V_H),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
c_Message_Oparts(c_Message_Oanalz(X0)) = c_Message_Oparts(X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t2,plain,
c_Message_Oparts(c_Message_Oanalz(X1)) = c_Message_Oparts(X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t64,plain,
c_Message_Oparts(c_Message_Oanalz(X1)) = c_Message_Oparts(X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t70,plain,
c_Message_Oparts(c_Message_Osynth(c_Message_Oanalz(X1))) = c_union(c_Message_Oparts(X1),c_Message_Osynth(c_Message_Oanalz(X1)),tc_Message_Omsg),
inference(cp,[status(thm)],[t69,t64]) ).
cnf(t242,plain,
c_union(c_Message_Oparts(X1),c_Message_Osynth(c_Message_Oanalz(X1)),tc_Message_Omsg) = c_Message_Oparts(c_Message_Osynth(c_Message_Oanalz(X1))),
inference(orient,[status(thm)],[t70]) ).
cnf(t21,axiom,
sFlat2 = c_Message_Oanalz(v_H),
introduced(definition) ).
cnf(t78,plain,
c_Message_Oanalz(v_H) = sFlat2,
inference(orient,[status(thm)],[t21]) ).
cnf(t22,axiom,
sFlat3 = c_Message_Osynth(c_Message_Oanalz(v_H)),
introduced(definition) ).
cnf(t46901,plain,
sFlat3 = c_Message_Osynth(sFlat2),
inference(step,[status(thm)],[t22,t78]) ).
cnf(t93,plain,
c_Message_Osynth(sFlat2) = sFlat3,
inference(orient,[status(thm)],[t46901]) ).
cnf(t25,axiom,
sFlat6 = tc_set(tc_Message_Omsg),
introduced(definition) ).
cnf(t44,plain,
tc_set(tc_Message_Omsg) = sFlat6,
inference(orient,[status(thm)],[t25]) ).
cnf(t53,plain,
X1 = ifeq(c_lessequals(X1,X2,sFlat6),true,ifeq(c_lessequals(X2,X1,tc_set(tc_Message_Omsg)),true,X2,X1),X1),
inference(cp,[status(thm)],[t28,t44]) ).
cnf(t47019,plain,
X1 = ifeq(c_lessequals(X1,X2,sFlat6),true,ifeq(c_lessequals(X2,X1,sFlat6),true,X2,X1),X1),
inference(step,[status(thm)],[t53,t44]) ).
cnf(t1443,plain,
ifeq(c_lessequals(X1,X2,sFlat6),true,ifeq(c_lessequals(X2,X1,sFlat6),true,X2,X1),X1) = X1,
inference(orient,[status(thm)],[t47019]) ).
cnf(t79,plain,
c_Message_Oparts(v_H) = c_Message_Oparts(sFlat2),
inference(cp,[status(thm)],[t64,t78]) ).
cnf(t23,axiom,
sFlat4 = c_Message_Oparts(v_H),
introduced(definition) ).
cnf(t66,plain,
c_Message_Oparts(v_H) = sFlat4,
inference(orient,[status(thm)],[t23]) ).
cnf(t46905,plain,
sFlat4 = c_Message_Oparts(sFlat2),
inference(step,[status(thm)],[t79,t66]) ).
cnf(t104,plain,
c_Message_Oparts(sFlat2) = sFlat4,
inference(orient,[status(thm)],[t46905]) ).
cnf(t105,plain,
c_Message_Oparts(c_Message_Osynth(sFlat2)) = c_union(sFlat4,c_Message_Osynth(sFlat2),tc_Message_Omsg),
inference(cp,[status(thm)],[t69,t104]) ).
cnf(t46908,plain,
c_Message_Oparts(sFlat3) = c_union(sFlat4,c_Message_Osynth(sFlat2),tc_Message_Omsg),
inference(step,[status(thm)],[t105,t93]) ).
cnf(t46909,plain,
c_Message_Oparts(sFlat3) = c_union(sFlat4,sFlat3,tc_Message_Omsg),
inference(step,[status(thm)],[t46908,t93]) ).
cnf(t115,plain,
c_union(sFlat4,sFlat3,tc_Message_Omsg) = c_Message_Oparts(sFlat3),
inference(orient,[status(thm)],[t46909]) ).
cnf(t118,plain,
true = ifeq(c_lessequals(sFlat3,X1,tc_set(tc_Message_Omsg)),true,ifeq(c_lessequals(sFlat4,X1,tc_set(tc_Message_Omsg)),true,c_lessequals(c_Message_Oparts(sFlat3),X1,tc_set(tc_Message_Omsg)),true),true),
inference(cp,[status(thm)],[t29,t115]) ).
cnf(t47720,plain,
true = ifeq(c_lessequals(sFlat3,X1,sFlat6),true,ifeq(c_lessequals(sFlat4,X1,tc_set(tc_Message_Omsg)),true,c_lessequals(c_Message_Oparts(sFlat3),X1,tc_set(tc_Message_Omsg)),true),true),
inference(step,[status(thm)],[t118,t44]) ).
cnf(t47721,plain,
true = ifeq(c_lessequals(sFlat3,X1,sFlat6),true,ifeq(c_lessequals(sFlat4,X1,sFlat6),true,c_lessequals(c_Message_Oparts(sFlat3),X1,tc_set(tc_Message_Omsg)),true),true),
inference(step,[status(thm)],[t47720,t44]) ).
cnf(t47722,plain,
true = ifeq(c_lessequals(sFlat3,X1,sFlat6),true,ifeq(c_lessequals(sFlat4,X1,sFlat6),true,c_lessequals(c_Message_Oparts(sFlat3),X1,sFlat6),true),true),
inference(step,[status(thm)],[t47721,t44]) ).
cnf(t12751,plain,
ifeq(c_lessequals(sFlat3,X1,sFlat6),true,ifeq(c_lessequals(sFlat4,X1,sFlat6),true,c_lessequals(c_Message_Oparts(sFlat3),X1,sFlat6),true),true) = true,
inference(orient,[status(thm)],[t47722]) ).
cnf(t24,axiom,
sFlat5 = c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),c_Message_Oparts(v_H),tc_Message_Omsg),
introduced(definition) ).
cnf(t46899,plain,
sFlat5 = c_union(c_Message_Osynth(sFlat2),c_Message_Oparts(v_H),tc_Message_Omsg),
inference(step,[status(thm)],[t24,t78]) ).
cnf(t46900,plain,
sFlat5 = c_union(c_Message_Osynth(sFlat2),sFlat4,tc_Message_Omsg),
inference(step,[status(thm)],[t46899,t66]) ).
cnf(t89,plain,
c_union(c_Message_Osynth(sFlat2),sFlat4,tc_Message_Omsg) = sFlat5,
inference(orient,[status(thm)],[t46900]) ).
cnf(t46902,plain,
c_union(sFlat3,sFlat4,tc_Message_Omsg) = sFlat5,
inference(step,[status(thm)],[t89,t93]) ).
cnf(t95,plain,
c_union(sFlat3,sFlat4,tc_Message_Omsg) = sFlat5,
inference(rw,[status(thm)],[t46902]) ).
cnf(t110,plain,
c_union(sFlat3,sFlat4,tc_Message_Omsg) = sFlat5,
inference(orient,[status(thm)],[t95]) ).
cnf(t173,plain,
true = c_lessequals(sFlat3,sFlat5,tc_set(tc_Message_Omsg)),
inference(cp,[status(thm)],[t169,t110]) ).
cnf(t46916,plain,
true = c_lessequals(sFlat3,sFlat5,sFlat6),
inference(step,[status(thm)],[t173,t44]) ).
cnf(t191,plain,
c_lessequals(sFlat3,sFlat5,sFlat6) = true,
inference(orient,[status(thm)],[t46916]) ).
cnf(t12781,plain,
true = ifeq(true,true,ifeq(c_lessequals(sFlat4,sFlat5,sFlat6),true,c_lessequals(c_Message_Oparts(sFlat3),sFlat5,sFlat6),true),true),
inference(cp,[status(thm)],[t12751,t191]) ).
cnf(t47723,plain,
true = ifeq(c_lessequals(sFlat4,sFlat5,sFlat6),true,c_lessequals(c_Message_Oparts(sFlat3),sFlat5,sFlat6),true),
inference(step,[status(thm)],[t12781,t27]) ).
cnf(t211,plain,
true = c_lessequals(sFlat4,sFlat5,tc_set(tc_Message_Omsg)),
inference(cp,[status(thm)],[t206,t110]) ).
cnf(t46922,plain,
true = c_lessequals(sFlat4,sFlat5,sFlat6),
inference(step,[status(thm)],[t211,t44]) ).
cnf(t228,plain,
c_lessequals(sFlat4,sFlat5,sFlat6) = true,
inference(orient,[status(thm)],[t46922]) ).
cnf(t47724,plain,
true = ifeq(true,true,c_lessequals(c_Message_Oparts(sFlat3),sFlat5,sFlat6),true),
inference(step,[status(thm)],[t47723,t228]) ).
cnf(t47725,plain,
true = c_lessequals(c_Message_Oparts(sFlat3),sFlat5,sFlat6),
inference(step,[status(thm)],[t47724,t27]) ).
cnf(t12906,plain,
c_lessequals(c_Message_Oparts(sFlat3),sFlat5,sFlat6) = true,
inference(orient,[status(thm)],[t47725]) ).
cnf(t12907,plain,
c_Message_Oparts(sFlat3) = ifeq(true,true,ifeq(c_lessequals(sFlat5,c_Message_Oparts(sFlat3),sFlat6),true,sFlat5,c_Message_Oparts(sFlat3)),c_Message_Oparts(sFlat3)),
inference(cp,[status(thm)],[t1443,t12906]) ).
cnf(t47726,plain,
c_Message_Oparts(sFlat3) = ifeq(c_lessequals(sFlat5,c_Message_Oparts(sFlat3),sFlat6),true,sFlat5,c_Message_Oparts(sFlat3)),
inference(step,[status(thm)],[t12907,t27]) ).
cnf(t113,plain,
true = ifeq(c_lessequals(sFlat4,X1,tc_set(tc_Message_Omsg)),true,ifeq(c_lessequals(sFlat3,X1,tc_set(tc_Message_Omsg)),true,c_lessequals(sFlat5,X1,tc_set(tc_Message_Omsg)),true),true),
inference(cp,[status(thm)],[t29,t110]) ).
cnf(t47622,plain,
true = ifeq(c_lessequals(sFlat4,X1,sFlat6),true,ifeq(c_lessequals(sFlat3,X1,tc_set(tc_Message_Omsg)),true,c_lessequals(sFlat5,X1,tc_set(tc_Message_Omsg)),true),true),
inference(step,[status(thm)],[t113,t44]) ).
cnf(t47623,plain,
true = ifeq(c_lessequals(sFlat4,X1,sFlat6),true,ifeq(c_lessequals(sFlat3,X1,sFlat6),true,c_lessequals(sFlat5,X1,tc_set(tc_Message_Omsg)),true),true),
inference(step,[status(thm)],[t47622,t44]) ).
cnf(t47624,plain,
true = ifeq(c_lessequals(sFlat4,X1,sFlat6),true,ifeq(c_lessequals(sFlat3,X1,sFlat6),true,c_lessequals(sFlat5,X1,sFlat6),true),true),
inference(step,[status(thm)],[t47623,t44]) ).
cnf(t11857,plain,
ifeq(c_lessequals(sFlat4,X1,sFlat6),true,ifeq(c_lessequals(sFlat3,X1,sFlat6),true,c_lessequals(sFlat5,X1,sFlat6),true),true) = true,
inference(orient,[status(thm)],[t47624]) ).
cnf(t171,plain,
true = c_lessequals(sFlat4,c_Message_Oparts(sFlat3),tc_set(tc_Message_Omsg)),
inference(cp,[status(thm)],[t169,t115]) ).
cnf(t46917,plain,
true = c_lessequals(sFlat4,c_Message_Oparts(sFlat3),sFlat6),
inference(step,[status(thm)],[t171,t44]) ).
cnf(t192,plain,
c_lessequals(sFlat4,c_Message_Oparts(sFlat3),sFlat6) = true,
inference(orient,[status(thm)],[t46917]) ).
cnf(t11987,plain,
true = ifeq(true,true,ifeq(c_lessequals(sFlat3,c_Message_Oparts(sFlat3),sFlat6),true,c_lessequals(sFlat5,c_Message_Oparts(sFlat3),sFlat6),true),true),
inference(cp,[status(thm)],[t11857,t192]) ).
cnf(t47625,plain,
true = ifeq(c_lessequals(sFlat3,c_Message_Oparts(sFlat3),sFlat6),true,c_lessequals(sFlat5,c_Message_Oparts(sFlat3),sFlat6),true),
inference(step,[status(thm)],[t11987,t27]) ).
cnf(t209,plain,
true = c_lessequals(sFlat3,c_Message_Oparts(sFlat3),tc_set(tc_Message_Omsg)),
inference(cp,[status(thm)],[t206,t115]) ).
cnf(t46923,plain,
true = c_lessequals(sFlat3,c_Message_Oparts(sFlat3),sFlat6),
inference(step,[status(thm)],[t209,t44]) ).
cnf(t229,plain,
c_lessequals(sFlat3,c_Message_Oparts(sFlat3),sFlat6) = true,
inference(orient,[status(thm)],[t46923]) ).
cnf(t47626,plain,
true = ifeq(true,true,c_lessequals(sFlat5,c_Message_Oparts(sFlat3),sFlat6),true),
inference(step,[status(thm)],[t47625,t229]) ).
cnf(t47627,plain,
true = c_lessequals(sFlat5,c_Message_Oparts(sFlat3),sFlat6),
inference(step,[status(thm)],[t47626,t27]) ).
cnf(t12185,plain,
c_lessequals(sFlat5,c_Message_Oparts(sFlat3),sFlat6) = true,
inference(orient,[status(thm)],[t47627]) ).
cnf(t47727,plain,
c_Message_Oparts(sFlat3) = ifeq(true,true,sFlat5,c_Message_Oparts(sFlat3)),
inference(step,[status(thm)],[t47726,t12185]) ).
cnf(t47728,plain,
c_Message_Oparts(sFlat3) = sFlat5,
inference(step,[status(thm)],[t47727,t27]) ).
cnf(t12917,plain,
c_Message_Oparts(sFlat3) = sFlat5,
inference(orient,[status(thm)],[t47728]) ).
cnf(t26,axiom,
sFlat7 = c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),c_Message_Oparts(v_H),tc_Message_Omsg),tc_set(tc_Message_Omsg)),
introduced(definition) ).
cnf(t46896,plain,
sFlat7 = c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),c_Message_Oparts(v_H),tc_Message_Omsg),sFlat6),
inference(step,[status(thm)],[t26,t44]) ).
cnf(t63,plain,
c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),c_Message_Oparts(v_H),tc_Message_Omsg),sFlat6) = sFlat7,
inference(orient,[status(thm)],[t46896]) ).
cnf(t46897,plain,
c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),sFlat4,tc_Message_Omsg),sFlat6) = sFlat7,
inference(step,[status(thm)],[t63,t66]) ).
cnf(t68,plain,
c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),sFlat4,tc_Message_Omsg),sFlat6) = sFlat7,
inference(rw,[status(thm)],[t46897]) ).
cnf(t47222,plain,
c_lessequals(c_Message_Oparts(sFlat0),c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),sFlat4,tc_Message_Omsg),sFlat6) = sFlat7,
inference(step,[status(thm)],[t68,t96]) ).
cnf(t47223,plain,
c_lessequals(sFlat1,c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),sFlat4,tc_Message_Omsg),sFlat6) = sFlat7,
inference(step,[status(thm)],[t47222,t106]) ).
cnf(t47224,plain,
c_lessequals(sFlat1,c_union(c_Message_Osynth(sFlat2),sFlat4,tc_Message_Omsg),sFlat6) = sFlat7,
inference(step,[status(thm)],[t47223,t78]) ).
cnf(t47225,plain,
c_lessequals(sFlat1,c_union(sFlat3,sFlat4,tc_Message_Omsg),sFlat6) = sFlat7,
inference(step,[status(thm)],[t47224,t93]) ).
cnf(t47226,plain,
c_lessequals(sFlat1,sFlat5,sFlat6) = sFlat7,
inference(step,[status(thm)],[t47225,t110]) ).
cnf(t5380,plain,
c_lessequals(sFlat1,sFlat5,sFlat6) = sFlat7,
inference(orient,[status(thm)],[t47226]) ).
cnf(f6,axiom,
( c_lessequals(c_Message_Oparts(V_G),c_Message_Oparts(V_H),tc_set(tc_Message_Omsg))
| ~ c_lessequals(V_G,c_Message_Oparts(V_H),tc_set(tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Message_Oparts__subset__iff_1) ).
fof(f6_nnf,plain,
! [V_G,V_H] :
( c_lessequals(c_Message_Oparts(V_G),c_Message_Oparts(V_H),tc_set(tc_Message_Omsg))
| ~ c_lessequals(V_G,c_Message_Oparts(V_H),tc_set(tc_Message_Omsg)) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [V_G,V_H] :
( c_lessequals(c_Message_Oparts(V_G),c_Message_Oparts(V_H),tc_set(tc_Message_Omsg))
| ~ c_lessequals(V_G,c_Message_Oparts(V_H),tc_set(tc_Message_Omsg)) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( c_lessequals(c_Message_Oparts(X0),c_Message_Oparts(X1),tc_set(tc_Message_Omsg))
| ~ c_lessequals(X0,c_Message_Oparts(X1),tc_set(tc_Message_Omsg)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t10,plain,
ifeq(c_lessequals(X1,c_Message_Oparts(X2),tc_set(tc_Message_Omsg)),true,c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(X2),tc_set(tc_Message_Omsg)),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t30,plain,
ifeq(c_lessequals(X1,c_Message_Oparts(X2),tc_set(tc_Message_Omsg)),true,c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(X2),tc_set(tc_Message_Omsg)),true) = true,
inference(orient,[status(thm)],[t10]) ).
cnf(t46890,plain,
ifeq(c_lessequals(X1,c_Message_Oparts(X2),sFlat6),true,c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(X2),tc_set(tc_Message_Omsg)),true) = true,
inference(step,[status(thm)],[t30,t44]) ).
cnf(t46891,plain,
ifeq(c_lessequals(X1,c_Message_Oparts(X2),sFlat6),true,c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(X2),sFlat6),true) = true,
inference(step,[status(thm)],[t46890,t44]) ).
cnf(t60,plain,
ifeq(c_lessequals(X1,c_Message_Oparts(X2),sFlat6),true,c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(X2),sFlat6),true) = true,
inference(rw,[status(thm)],[t46891]) ).
cnf(t3473,plain,
ifeq(c_lessequals(X1,c_Message_Oparts(X2),sFlat6),true,c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(X2),sFlat6),true) = true,
inference(orient,[status(thm)],[t60]) ).
cnf(f16,axiom,
( c_lessequals(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a))
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(V_x,V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_Oinsert__subset_2) ).
fof(f16_nnf,plain,
! [V_x,V_B,T_a,V_A] :
( c_lessequals(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a))
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(V_x,V_B,T_a) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [V_x,V_B,T_a,V_A] :
( c_lessequals(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a))
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(V_x,V_B,T_a) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( c_lessequals(c_insert(X0,X3,X2),X1,tc_set(X2))
| ~ c_lessequals(X3,X1,tc_set(X2))
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t17,plain,
ifeq(c_in(X1,X2,X3),true,ifeq(c_lessequals(X4,X2,tc_set(X3)),true,c_lessequals(c_insert(X1,X4,X3),X2,tc_set(X3)),true),true) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t37,plain,
ifeq(c_in(X1,X2,X3),true,ifeq(c_lessequals(X4,X2,tc_set(X3)),true,c_lessequals(c_insert(X1,X4,X3),X2,tc_set(X3)),true),true) = true,
inference(orient,[status(thm)],[t17]) ).
cnf(t99,plain,
true = ifeq(c_in(v_X,X1,tc_Message_Omsg),true,ifeq(c_lessequals(v_H,X1,tc_set(tc_Message_Omsg)),true,c_lessequals(sFlat0,X1,tc_set(tc_Message_Omsg)),true),true),
inference(cp,[status(thm)],[t37,t96]) ).
cnf(t47575,plain,
true = ifeq(c_in(v_X,X1,tc_Message_Omsg),true,ifeq(c_lessequals(v_H,X1,sFlat6),true,c_lessequals(sFlat0,X1,tc_set(tc_Message_Omsg)),true),true),
inference(step,[status(thm)],[t99,t44]) ).
cnf(t47576,plain,
true = ifeq(c_in(v_X,X1,tc_Message_Omsg),true,ifeq(c_lessequals(v_H,X1,sFlat6),true,c_lessequals(sFlat0,X1,sFlat6),true),true),
inference(step,[status(thm)],[t47575,t44]) ).
cnf(t11098,plain,
ifeq(c_in(v_X,X1,tc_Message_Omsg),true,ifeq(c_lessequals(v_H,X1,sFlat6),true,c_lessequals(sFlat0,X1,sFlat6),true),true) = true,
inference(orient,[status(thm)],[t47576]) ).
cnf(f5,axiom,
( c_lessequals(V_G,c_Message_Oparts(V_H),tc_set(tc_Message_Omsg))
| ~ c_lessequals(c_Message_Oparts(V_G),c_Message_Oparts(V_H),tc_set(tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Message_Oparts__subset__iff_0) ).
fof(f5_nnf,plain,
! [V_G,V_H] :
( c_lessequals(V_G,c_Message_Oparts(V_H),tc_set(tc_Message_Omsg))
| ~ c_lessequals(c_Message_Oparts(V_G),c_Message_Oparts(V_H),tc_set(tc_Message_Omsg)) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [V_G,V_H] :
( c_lessequals(V_G,c_Message_Oparts(V_H),tc_set(tc_Message_Omsg))
| ~ c_lessequals(c_Message_Oparts(V_G),c_Message_Oparts(V_H),tc_set(tc_Message_Omsg)) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( c_lessequals(X0,c_Message_Oparts(X1),tc_set(tc_Message_Omsg))
| ~ c_lessequals(c_Message_Oparts(X0),c_Message_Oparts(X1),tc_set(tc_Message_Omsg)) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t12,plain,
ifeq(c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(X2),tc_set(tc_Message_Omsg)),true,c_lessequals(X1,c_Message_Oparts(X2),tc_set(tc_Message_Omsg)),true) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t31,plain,
ifeq(c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(X2),tc_set(tc_Message_Omsg)),true,c_lessequals(X1,c_Message_Oparts(X2),tc_set(tc_Message_Omsg)),true) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t46894,plain,
ifeq(c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(X2),sFlat6),true,c_lessequals(X1,c_Message_Oparts(X2),tc_set(tc_Message_Omsg)),true) = true,
inference(step,[status(thm)],[t31,t44]) ).
cnf(t46895,plain,
ifeq(c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(X2),sFlat6),true,c_lessequals(X1,c_Message_Oparts(X2),sFlat6),true) = true,
inference(step,[status(thm)],[t46894,t44]) ).
cnf(t62,plain,
ifeq(c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(X2),sFlat6),true,c_lessequals(X1,c_Message_Oparts(X2),sFlat6),true) = true,
inference(rw,[status(thm)],[t46895]) ).
cnf(t4629,plain,
ifeq(c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(X2),sFlat6),true,c_lessequals(X1,c_Message_Oparts(X2),sFlat6),true) = true,
inference(orient,[status(thm)],[t62]) ).
cnf(t72,plain,
true = ifeq(c_lessequals(c_Message_Oparts(c_Message_Osynth(X1)),X2,tc_set(tc_Message_Omsg)),true,c_lessequals(c_Message_Oparts(X1),X2,tc_set(tc_Message_Omsg)),true),
inference(cp,[status(thm)],[t34,t69]) ).
cnf(t47275,plain,
true = ifeq(c_lessequals(c_Message_Oparts(c_Message_Osynth(X1)),X2,sFlat6),true,c_lessequals(c_Message_Oparts(X1),X2,tc_set(tc_Message_Omsg)),true),
inference(step,[status(thm)],[t72,t44]) ).
cnf(t47276,plain,
true = ifeq(c_lessequals(c_Message_Oparts(c_Message_Osynth(X1)),X2,sFlat6),true,c_lessequals(c_Message_Oparts(X1),X2,sFlat6),true),
inference(step,[status(thm)],[t47275,t44]) ).
cnf(t5985,plain,
ifeq(c_lessequals(c_Message_Oparts(c_Message_Osynth(X1)),X2,sFlat6),true,c_lessequals(c_Message_Oparts(X1),X2,sFlat6),true) = true,
inference(orient,[status(thm)],[t47276]) ).
cnf(t51,plain,
true = ifeq(c_lessequals(c_union(X1,X2,tc_Message_Omsg),X3,sFlat6),true,c_lessequals(X2,X3,tc_set(tc_Message_Omsg)),true),
inference(cp,[status(thm)],[t33,t44]) ).
cnf(t47002,plain,
true = ifeq(c_lessequals(c_union(X1,X2,tc_Message_Omsg),X3,sFlat6),true,c_lessequals(X2,X3,sFlat6),true),
inference(step,[status(thm)],[t51,t44]) ).
cnf(t1056,plain,
ifeq(c_lessequals(c_union(X1,X2,tc_Message_Omsg),X3,sFlat6),true,c_lessequals(X2,X3,sFlat6),true) = true,
inference(orient,[status(thm)],[t47002]) ).
cnf(t45,plain,
true = class_Orderings_Oorder(sFlat6),
inference(cp,[status(thm)],[t42,t44]) ).
cnf(t101,plain,
class_Orderings_Oorder(sFlat6) = true,
inference(orient,[status(thm)],[t45]) ).
cnf(t102,plain,
true = ifeq(true,true,c_lessequals(X1,X1,sFlat6),true),
inference(cp,[status(thm)],[t38,t101]) ).
cnf(t46907,plain,
true = c_lessequals(X1,X1,sFlat6),
inference(step,[status(thm)],[t102,t27]) ).
cnf(t114,plain,
c_lessequals(X1,X1,sFlat6) = true,
inference(orient,[status(thm)],[t46907]) ).
cnf(t4645,plain,
true = ifeq(true,true,c_lessequals(X1,c_Message_Oparts(X1),sFlat6),true),
inference(cp,[status(thm)],[t4629,t114]) ).
cnf(t47183,plain,
true = c_lessequals(X1,c_Message_Oparts(X1),sFlat6),
inference(step,[status(thm)],[t4645,t27]) ).
cnf(t4738,plain,
c_lessequals(X1,c_Message_Oparts(X1),sFlat6) = true,
inference(orient,[status(thm)],[t47183]) ).
cnf(t4756,plain,
true = ifeq(true,true,c_lessequals(X1,c_Message_Oparts(c_union(X2,X1,tc_Message_Omsg)),sFlat6),true),
inference(cp,[status(thm)],[t1056,t4738]) ).
cnf(t47266,plain,
true = c_lessequals(X1,c_Message_Oparts(c_union(X2,X1,tc_Message_Omsg)),sFlat6),
inference(step,[status(thm)],[t4756,t27]) ).
cnf(t5844,plain,
c_lessequals(X1,c_Message_Oparts(c_union(X2,X1,tc_Message_Omsg)),sFlat6) = true,
inference(orient,[status(thm)],[t47266]) ).
cnf(t5856,plain,
true = ifeq(true,true,c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(c_union(X2,X1,tc_Message_Omsg)),sFlat6),true),
inference(cp,[status(thm)],[t3473,t5844]) ).
cnf(t47450,plain,
true = c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(c_union(X2,X1,tc_Message_Omsg)),sFlat6),
inference(step,[status(thm)],[t5856,t27]) ).
cnf(t8912,plain,
c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(c_union(X2,X1,tc_Message_Omsg)),sFlat6) = true,
inference(orient,[status(thm)],[t47450]) ).
cnf(t8927,plain,
true = ifeq(true,true,c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(c_union(X2,c_Message_Osynth(X1),tc_Message_Omsg)),sFlat6),true),
inference(cp,[status(thm)],[t5985,t8912]) ).
cnf(t48211,plain,
true = c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(c_union(X2,c_Message_Osynth(X1),tc_Message_Omsg)),sFlat6),
inference(step,[status(thm)],[t8927,t27]) ).
cnf(t20270,plain,
c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(c_union(X2,c_Message_Osynth(X1),tc_Message_Omsg)),sFlat6) = true,
inference(orient,[status(thm)],[t48211]) ).
cnf(t20276,plain,
true = c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(c_union(X2,c_Message_Osynth(c_Message_Oanalz(X1)),tc_Message_Omsg)),sFlat6),
inference(cp,[status(thm)],[t20270,t64]) ).
cnf(t42413,plain,
c_lessequals(c_Message_Oparts(X1),c_Message_Oparts(c_union(X2,c_Message_Osynth(c_Message_Oanalz(X1)),tc_Message_Omsg)),sFlat6) = true,
inference(orient,[status(thm)],[t20276]) ).
cnf(t42418,plain,
true = ifeq(true,true,c_lessequals(X1,c_Message_Oparts(c_union(X2,c_Message_Osynth(c_Message_Oanalz(X1)),tc_Message_Omsg)),sFlat6),true),
inference(cp,[status(thm)],[t4629,t42413]) ).
cnf(t49319,plain,
true = c_lessequals(X1,c_Message_Oparts(c_union(X2,c_Message_Osynth(c_Message_Oanalz(X1)),tc_Message_Omsg)),sFlat6),
inference(step,[status(thm)],[t42418,t27]) ).
cnf(t42466,plain,
c_lessequals(X1,c_Message_Oparts(c_union(X2,c_Message_Osynth(c_Message_Oanalz(X1)),tc_Message_Omsg)),sFlat6) = true,
inference(orient,[status(thm)],[t49319]) ).
cnf(t42475,plain,
true = ifeq(c_in(v_X,c_Message_Oparts(c_union(X1,c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg)),tc_Message_Omsg),true,ifeq(true,true,c_lessequals(sFlat0,c_Message_Oparts(c_union(X1,c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg)),sFlat6),true),true),
inference(cp,[status(thm)],[t11098,t42466]) ).
cnf(t49321,plain,
true = ifeq(c_in(v_X,c_Message_Oparts(c_union(X1,c_Message_Osynth(sFlat2),tc_Message_Omsg)),tc_Message_Omsg),true,ifeq(true,true,c_lessequals(sFlat0,c_Message_Oparts(c_union(X1,c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg)),sFlat6),true),true),
inference(step,[status(thm)],[t42475,t78]) ).
cnf(t49322,plain,
true = ifeq(c_in(v_X,c_Message_Oparts(c_union(X1,sFlat3,tc_Message_Omsg)),tc_Message_Omsg),true,ifeq(true,true,c_lessequals(sFlat0,c_Message_Oparts(c_union(X1,c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg)),sFlat6),true),true),
inference(step,[status(thm)],[t49321,t93]) ).
cnf(f14,axiom,
( c_in(V_x,V_B,T_a)
| ~ c_lessequals(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_Oinsert__subset_0) ).
fof(f14_nnf,plain,
! [V_x,V_A,T_a,V_B] :
( c_in(V_x,V_B,T_a)
| ~ c_lessequals(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a)) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [V_x,V_A,T_a,V_B] :
( c_in(V_x,V_B,T_a)
| ~ c_lessequals(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a)) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( c_in(X0,X3,X2)
| ~ c_lessequals(c_insert(X0,X1,X2),X3,tc_set(X2)) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(t9,plain,
ifeq(c_lessequals(c_insert(X1,X2,X3),X4,tc_set(X3)),true,c_in(X1,X4,X3),true) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t36,plain,
ifeq(c_lessequals(c_insert(X1,X2,X3),X4,tc_set(X3)),true,c_in(X1,X4,X3),true) = true,
inference(orient,[status(thm)],[t9]) ).
cnf(t46,plain,
true = ifeq(c_lessequals(c_insert(X1,X2,tc_Message_Omsg),X3,sFlat6),true,c_in(X1,X3,tc_Message_Omsg),true),
inference(cp,[status(thm)],[t36,t44]) ).
cnf(t199,plain,
ifeq(c_lessequals(c_insert(X1,X2,tc_Message_Omsg),X3,sFlat6),true,c_in(X1,X3,tc_Message_Omsg),true) = true,
inference(orient,[status(thm)],[t46]) ).
cnf(t5870,plain,
true = ifeq(true,true,c_in(X1,c_Message_Oparts(c_union(X2,c_insert(X1,X3,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg),true),
inference(cp,[status(thm)],[t199,t5844]) ).
cnf(t48621,plain,
true = c_in(X1,c_Message_Oparts(c_union(X2,c_insert(X1,X3,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg),
inference(step,[status(thm)],[t5870,t27]) ).
cnf(t27160,plain,
c_in(X1,c_Message_Oparts(c_union(X2,c_insert(X1,X3,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg) = true,
inference(orient,[status(thm)],[t48621]) ).
cnf(t127,plain,
true = ifeq(c_in(X1,X2,X3),true,ifeq(true,true,c_lessequals(c_insert(X1,X2,X3),X2,tc_set(X3)),true),true),
inference(cp,[status(thm)],[t37,t119]) ).
cnf(t47807,plain,
true = ifeq(c_in(X1,X2,X3),true,c_lessequals(c_insert(X1,X2,X3),X2,tc_set(X3)),true),
inference(step,[status(thm)],[t127,t27]) ).
cnf(t13461,plain,
ifeq(c_in(X1,X2,X3),true,c_lessequals(c_insert(X1,X2,X3),X2,tc_set(X3)),true) = true,
inference(orient,[status(thm)],[t47807]) ).
cnf(f0,negated_conjecture,
c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f0_nnf,plain,
c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f0]) ).
cnf(c0,plain,
c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f0_nnf]) ).
cnf(t4,plain,
c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t39,plain,
c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t46898,plain,
c_in(v_X,c_Message_Osynth(sFlat2),tc_Message_Omsg) = true,
inference(step,[status(thm)],[t39,t78]) ).
cnf(t80,plain,
c_in(v_X,c_Message_Osynth(sFlat2),tc_Message_Omsg) = true,
inference(rw,[status(thm)],[t46898]) ).
cnf(t46911,plain,
c_in(v_X,sFlat3,tc_Message_Omsg) = true,
inference(step,[status(thm)],[t80,t93]) ).
cnf(t132,plain,
c_in(v_X,sFlat3,tc_Message_Omsg) = true,
inference(orient,[status(thm)],[t46911]) ).
cnf(t13533,plain,
true = ifeq(true,true,c_lessequals(c_insert(v_X,sFlat3,tc_Message_Omsg),sFlat3,tc_set(tc_Message_Omsg)),true),
inference(cp,[status(thm)],[t13461,t132]) ).
cnf(t47813,plain,
true = c_lessequals(c_insert(v_X,sFlat3,tc_Message_Omsg),sFlat3,tc_set(tc_Message_Omsg)),
inference(step,[status(thm)],[t13533,t27]) ).
cnf(t47814,plain,
true = c_lessequals(c_insert(v_X,sFlat3,tc_Message_Omsg),sFlat3,sFlat6),
inference(step,[status(thm)],[t47813,t44]) ).
cnf(t13558,plain,
c_lessequals(c_insert(v_X,sFlat3,tc_Message_Omsg),sFlat3,sFlat6) = true,
inference(orient,[status(thm)],[t47814]) ).
cnf(t13559,plain,
c_insert(v_X,sFlat3,tc_Message_Omsg) = ifeq(true,true,ifeq(c_lessequals(sFlat3,c_insert(v_X,sFlat3,tc_Message_Omsg),sFlat6),true,sFlat3,c_insert(v_X,sFlat3,tc_Message_Omsg)),c_insert(v_X,sFlat3,tc_Message_Omsg)),
inference(cp,[status(thm)],[t1443,t13558]) ).
cnf(t47815,plain,
c_insert(v_X,sFlat3,tc_Message_Omsg) = ifeq(c_lessequals(sFlat3,c_insert(v_X,sFlat3,tc_Message_Omsg),sFlat6),true,sFlat3,c_insert(v_X,sFlat3,tc_Message_Omsg)),
inference(step,[status(thm)],[t13559,t27]) ).
cnf(f15,axiom,
( c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_Oinsert__subset_1) ).
fof(f15_nnf,plain,
! [V_x,V_A,T_a,V_B] :
( c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a)) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [V_x,V_A,T_a,V_B] :
( c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a)) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( c_lessequals(X1,X3,tc_set(X2))
| ~ c_lessequals(c_insert(X0,X1,X2),X3,tc_set(X2)) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(t13,plain,
ifeq(c_lessequals(c_insert(X1,X2,X3),X4,tc_set(X3)),true,c_lessequals(X2,X4,tc_set(X3)),true) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t35,plain,
ifeq(c_lessequals(c_insert(X1,X2,X3),X4,tc_set(X3)),true,c_lessequals(X2,X4,tc_set(X3)),true) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t121,plain,
true = ifeq(true,true,c_lessequals(X1,c_insert(X2,X1,X3),tc_set(X3)),true),
inference(cp,[status(thm)],[t35,t119]) ).
cnf(t46913,plain,
true = c_lessequals(X1,c_insert(X2,X1,X3),tc_set(X3)),
inference(step,[status(thm)],[t121,t27]) ).
cnf(t150,plain,
c_lessequals(X1,c_insert(X2,X1,X3),tc_set(X3)) = true,
inference(orient,[status(thm)],[t46913]) ).
cnf(t152,plain,
true = c_lessequals(X1,c_insert(X2,X1,tc_Message_Omsg),sFlat6),
inference(cp,[status(thm)],[t150,t44]) ).
cnf(t168,plain,
c_lessequals(X1,c_insert(X2,X1,tc_Message_Omsg),sFlat6) = true,
inference(orient,[status(thm)],[t152]) ).
cnf(t47816,plain,
c_insert(v_X,sFlat3,tc_Message_Omsg) = ifeq(true,true,sFlat3,c_insert(v_X,sFlat3,tc_Message_Omsg)),
inference(step,[status(thm)],[t47815,t168]) ).
cnf(t47817,plain,
c_insert(v_X,sFlat3,tc_Message_Omsg) = sFlat3,
inference(step,[status(thm)],[t47816,t27]) ).
cnf(t13567,plain,
c_insert(v_X,sFlat3,tc_Message_Omsg) = sFlat3,
inference(orient,[status(thm)],[t47817]) ).
cnf(t27163,plain,
true = c_in(v_X,c_Message_Oparts(c_union(X1,sFlat3,tc_Message_Omsg)),tc_Message_Omsg),
inference(cp,[status(thm)],[t27160,t13567]) ).
cnf(t27179,plain,
c_in(v_X,c_Message_Oparts(c_union(X1,sFlat3,tc_Message_Omsg)),tc_Message_Omsg) = true,
inference(orient,[status(thm)],[t27163]) ).
cnf(t49323,plain,
true = ifeq(true,true,ifeq(true,true,c_lessequals(sFlat0,c_Message_Oparts(c_union(X1,c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg)),sFlat6),true),true),
inference(step,[status(thm)],[t49322,t27179]) ).
cnf(t49324,plain,
true = ifeq(true,true,c_lessequals(sFlat0,c_Message_Oparts(c_union(X1,c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg)),sFlat6),true),
inference(step,[status(thm)],[t49323,t27]) ).
cnf(t49325,plain,
true = c_lessequals(sFlat0,c_Message_Oparts(c_union(X1,c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg)),sFlat6),
inference(step,[status(thm)],[t49324,t27]) ).
cnf(t49326,plain,
true = c_lessequals(sFlat0,c_Message_Oparts(c_union(X1,c_Message_Osynth(sFlat2),tc_Message_Omsg)),sFlat6),
inference(step,[status(thm)],[t49325,t78]) ).
cnf(t49327,plain,
true = c_lessequals(sFlat0,c_Message_Oparts(c_union(X1,sFlat3,tc_Message_Omsg)),sFlat6),
inference(step,[status(thm)],[t49326,t93]) ).
cnf(t42521,plain,
c_lessequals(sFlat0,c_Message_Oparts(c_union(X1,sFlat3,tc_Message_Omsg)),sFlat6) = true,
inference(orient,[status(thm)],[t49327]) ).
cnf(t42524,plain,
true = ifeq(true,true,c_lessequals(c_Message_Oparts(sFlat0),c_Message_Oparts(c_union(X1,sFlat3,tc_Message_Omsg)),sFlat6),true),
inference(cp,[status(thm)],[t3473,t42521]) ).
cnf(t49328,plain,
true = c_lessequals(c_Message_Oparts(sFlat0),c_Message_Oparts(c_union(X1,sFlat3,tc_Message_Omsg)),sFlat6),
inference(step,[status(thm)],[t42524,t27]) ).
cnf(t49329,plain,
true = c_lessequals(sFlat1,c_Message_Oparts(c_union(X1,sFlat3,tc_Message_Omsg)),sFlat6),
inference(step,[status(thm)],[t49328,t106]) ).
cnf(t42555,plain,
c_lessequals(sFlat1,c_Message_Oparts(c_union(X1,sFlat3,tc_Message_Omsg)),sFlat6) = true,
inference(orient,[status(thm)],[t49329]) ).
cnf(t129,plain,
true = ifeq(true,true,ifeq(c_lessequals(X1,X2,tc_set(X3)),true,c_lessequals(c_union(X1,X2,X3),X2,tc_set(X3)),true),true),
inference(cp,[status(thm)],[t29,t119]) ).
cnf(t47858,plain,
true = ifeq(c_lessequals(X1,X2,tc_set(X3)),true,c_lessequals(c_union(X1,X2,X3),X2,tc_set(X3)),true),
inference(step,[status(thm)],[t129,t27]) ).
cnf(t13973,plain,
ifeq(c_lessequals(X1,X2,tc_set(X3)),true,c_lessequals(c_union(X1,X2,X3),X2,tc_set(X3)),true) = true,
inference(orient,[status(thm)],[t47858]) ).
cnf(t13974,plain,
true = ifeq(true,true,c_lessequals(c_union(X1,X1,X2),X1,tc_set(X2)),true),
inference(cp,[status(thm)],[t13973,t119]) ).
cnf(t47859,plain,
true = c_lessequals(c_union(X1,X1,X2),X1,tc_set(X2)),
inference(step,[status(thm)],[t13974,t27]) ).
cnf(t14014,plain,
c_lessequals(c_union(X1,X1,X2),X1,tc_set(X2)) = true,
inference(orient,[status(thm)],[t47859]) ).
cnf(t14020,plain,
c_union(X1,X1,X2) = ifeq(true,true,ifeq(c_lessequals(X1,c_union(X1,X1,X2),tc_set(X2)),true,X1,c_union(X1,X1,X2)),c_union(X1,X1,X2)),
inference(cp,[status(thm)],[t28,t14014]) ).
cnf(t47860,plain,
c_union(X1,X1,X2) = ifeq(c_lessequals(X1,c_union(X1,X1,X2),tc_set(X2)),true,X1,c_union(X1,X1,X2)),
inference(step,[status(thm)],[t14020,t27]) ).
cnf(t47861,plain,
c_union(X1,X1,X2) = ifeq(true,true,X1,c_union(X1,X1,X2)),
inference(step,[status(thm)],[t47860,t206]) ).
cnf(t47862,plain,
c_union(X1,X1,X2) = X1,
inference(step,[status(thm)],[t47861,t27]) ).
cnf(t14031,plain,
c_union(X1,X1,X2) = X1,
inference(orient,[status(thm)],[t47862]) ).
cnf(t42556,plain,
true = c_lessequals(sFlat1,c_Message_Oparts(sFlat3),sFlat6),
inference(cp,[status(thm)],[t42555,t14031]) ).
cnf(t49330,plain,
true = c_lessequals(sFlat1,sFlat5,sFlat6),
inference(step,[status(thm)],[t42556,t12917]) ).
cnf(t49331,plain,
true = sFlat7,
inference(step,[status(thm)],[t49330,t5380]) ).
cnf(t42568,plain,
true = sFlat7,
inference(orient,[status(thm)],[t49331]) ).
cnf(f1,negated_conjecture,
~ c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),c_Message_Oparts(v_H),tc_Message_Omsg),tc_set(tc_Message_Omsg)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1_nnf,plain,
~ c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),c_Message_Oparts(v_H),tc_Message_Omsg),tc_set(tc_Message_Omsg)),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
~ c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),c_Message_Oparts(v_H),tc_Message_Omsg),tc_set(tc_Message_Omsg)),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
~ c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),c_Message_Oparts(v_H),tc_Message_Omsg),tc_set(tc_Message_Omsg)),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(goal_0,negated_conjecture,
c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),c_Message_Oparts(v_H),tc_Message_Omsg),tc_set(tc_Message_Omsg)) != true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(g0_0,plain,
c_lessequals(c_Message_Oparts(sFlat0),c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),c_Message_Oparts(v_H),tc_Message_Omsg),tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[goal_0,t96]) ).
cnf(g0_1,plain,
c_lessequals(sFlat1,c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),c_Message_Oparts(v_H),tc_Message_Omsg),tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[g0_0,t106]) ).
cnf(g0_2,plain,
c_lessequals(sFlat1,c_union(c_Message_Oparts(v_H),c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg),tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[g0_1,t29560]) ).
cnf(g0_3,plain,
c_lessequals(sFlat1,c_Message_Oparts(c_Message_Osynth(c_Message_Oanalz(v_H))),tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[g0_2,t242]) ).
cnf(g0_4,plain,
c_lessequals(sFlat1,c_Message_Oparts(c_Message_Osynth(sFlat2)),tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[g0_3,t78]) ).
cnf(g0_5,plain,
c_lessequals(sFlat1,c_Message_Oparts(sFlat3),tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[g0_4,t93]) ).
cnf(g0_6,plain,
c_lessequals(sFlat1,sFlat5,tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[g0_5,t12917]) ).
cnf(g0_7,plain,
c_lessequals(sFlat1,sFlat5,sFlat6) != true,
inference(rw,[status(thm)],[g0_6,t44]) ).
cnf(g0_8,plain,
sFlat7 != true,
inference(rw,[status(thm)],[g0_7,t5380]) ).
cnf(g0_9,plain,
sFlat7 != sFlat7,
inference(rw,[status(thm)],[g0_8,t42568]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV252-2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n015.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 18:56:41 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 96.48/13.03 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 96.48/13.03 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------