%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV249-2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n013.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:36 PM UTC 2026
% Result : Unsatisfiable 44.20s 6.28s
% Output : Proof 44.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 23
% Syntax : Number of formulae : 198 ( 166 unt; 0 def)
% Number of atoms : 242 ( 158 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 103 ( 59 ~; 44 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 10 con; 0-4 aty)
% Number of variables : 416 ( 41 sgn 92 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t17,axiom,
sFlat0 = c_insert(v_X,v_H,tc_Message_Omsg),
introduced(definition) ).
cnf(t110,plain,
c_insert(v_X,v_H,tc_Message_Omsg) = sFlat0,
inference(orient,[status(thm)],[t17]) ).
cnf(t18,axiom,
sFlat1 = c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),
introduced(definition) ).
cnf(t107,plain,
c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)) = sFlat1,
inference(orient,[status(thm)],[t18]) ).
cnf(t20519,plain,
c_Message_Oanalz(sFlat0) = sFlat1,
inference(step,[status(thm)],[t107,t110]) ).
cnf(t114,plain,
c_Message_Oanalz(sFlat0) = sFlat1,
inference(rw,[status(thm)],[t20519]) ).
cnf(t120,plain,
c_Message_Oanalz(sFlat0) = sFlat1,
inference(orient,[status(thm)],[t114]) ).
cnf(f4,axiom,
c_Message_Oanalz(c_union(c_Message_Osynth(V_G),V_H,tc_Message_Omsg)) = c_union(c_Message_Oanalz(c_union(V_G,V_H,tc_Message_Omsg)),c_Message_Osynth(V_G),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Message_Oanalz__synth__Un_0) ).
fof(f4_nnf,plain,
! [V_G,V_H] : c_Message_Oanalz(c_union(c_Message_Osynth(V_G),V_H,tc_Message_Omsg)) = c_union(c_Message_Oanalz(c_union(V_G,V_H,tc_Message_Omsg)),c_Message_Osynth(V_G),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [V_G,V_H] : c_Message_Oanalz(c_union(c_Message_Osynth(V_G),V_H,tc_Message_Omsg)) = c_union(c_Message_Oanalz(c_union(V_G,V_H,tc_Message_Omsg)),c_Message_Osynth(V_G),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
c_Message_Oanalz(c_union(c_Message_Osynth(X0),X1,tc_Message_Omsg)) = c_union(c_Message_Oanalz(c_union(X0,X1,tc_Message_Omsg)),c_Message_Osynth(X0),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t9,plain,
c_union(c_Message_Oanalz(c_union(X1,X2,tc_Message_Omsg)),c_Message_Osynth(X1),tc_Message_Omsg) = c_Message_Oanalz(c_union(c_Message_Osynth(X1),X2,tc_Message_Omsg)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t50,plain,
c_union(c_Message_Oanalz(c_union(X1,X2,tc_Message_Omsg)),c_Message_Osynth(X1),tc_Message_Omsg) = c_Message_Oanalz(c_union(c_Message_Osynth(X1),X2,tc_Message_Omsg)),
inference(orient,[status(thm)],[t9]) ).
cnf(t1674,plain,
c_union(c_Message_Oanalz(c_union(X1,X2,tc_Message_Omsg)),c_Message_Osynth(X1),tc_Message_Omsg) = c_Message_Oanalz(c_union(c_Message_Osynth(X1),X2,tc_Message_Omsg)),
inference(rw,[status(thm)],[t50]) ).
cnf(f15,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/sandbox/benchmark/theBenchmark.p',cls_Set_Osubset__antisym_0) ).
fof(f15_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)],[f15]) ).
fof(f15_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)],[f15_nnf]) ).
cnf(c15,plain,
( X1 = X0
| ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(t14,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)],[c15]) ).
cnf(t27,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)],[t14]) ).
cnf(f12,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/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__subset__iff_2) ).
fof(f12_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)],[f12]) ).
fof(f12_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)],[f12_nnf]) ).
cnf(c12,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)],[f12_sk]) ).
cnf(t16,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)],[c12]) ).
cnf(t28,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)],[t16]) ).
cnf(f7,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/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__Diff__cancel_0) ).
fof(f7_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)],[f7]) ).
fof(f7_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)],[f7_nnf]) ).
cnf(c7,plain,
c_union(X0,c_minus(X1,X0,tc_set(X2)),X2) = c_union(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t5,plain,
c_union(X1,c_minus(X2,X1,tc_set(X3)),X3) = c_union(X1,X2,X3),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t39,plain,
c_union(X1,c_minus(X2,X1,tc_set(X3)),X3) = c_union(X1,X2,X3),
inference(orient,[status(thm)],[t5]) ).
cnf(t41,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)],[t28,t39]) ).
cnf(t533,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)],[t41]) ).
cnf(f10,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/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__subset__iff_0) ).
fof(f10_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)],[f10]) ).
fof(f10_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)],[f10_nnf]) ).
cnf(c10,plain,
( c_lessequals(X0,X3,tc_set(X2))
| ~ c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2)) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t12,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)],[c10]) ).
cnf(t31,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)],[t12]) ).
cnf(f5,axiom,
( c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Orderings_Oorder__class_Oaxioms__1_0) ).
fof(f5_nnf,plain,
! [T_a,V_x] :
( c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [T_a,V_x] :
( c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( c_lessequals(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t3,plain,
ifeq(class_Orderings_Oorder(X1),true,c_lessequals(X2,X2,X1),true) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t33,plain,
ifeq(class_Orderings_Oorder(X1),true,c_lessequals(X2,X2,X1),true) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(f16,axiom,
class_Orderings_Oorder(tc_set(T_1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_set_2) ).
fof(f16_nnf,plain,
! [T_1] : class_Orderings_Oorder(tc_set(T_1)),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [T_1] : class_Orderings_Oorder(tc_set(T_1)),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
class_Orderings_Oorder(tc_set(X0)),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t0,plain,
class_Orderings_Oorder(tc_set(X1)) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t35,plain,
class_Orderings_Oorder(tc_set(X1)) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t36,plain,
true = ifeq(true,true,c_lessequals(X1,X1,tc_set(X2)),true),
inference(cp,[status(thm)],[t33,t35]) ).
cnf(t1,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t26,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t20523,plain,
true = c_lessequals(X1,X1,tc_set(X2)),
inference(step,[status(thm)],[t36,t26]) ).
cnf(t123,plain,
c_lessequals(X1,X1,tc_set(X2)) = true,
inference(orient,[status(thm)],[t20523]) ).
cnf(t126,plain,
true = ifeq(true,true,c_lessequals(X1,c_union(X1,X2,X3),tc_set(X3)),true),
inference(cp,[status(thm)],[t31,t123]) ).
cnf(t20533,plain,
true = c_lessequals(X1,c_union(X1,X2,X3),tc_set(X3)),
inference(step,[status(thm)],[t126,t26]) ).
cnf(t183,plain,
c_lessequals(X1,c_union(X1,X2,X3),tc_set(X3)) = true,
inference(orient,[status(thm)],[t20533]) ).
cnf(f6,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/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__Diff__cancel2_0) ).
fof(f6_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)],[f6]) ).
fof(f6_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)],[f6_nnf]) ).
cnf(c6,plain,
c_union(c_minus(X0,X1,tc_set(X2)),X1,X2) = c_union(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t6,plain,
c_union(c_minus(X1,X2,tc_set(X3)),X2,X3) = c_union(X1,X2,X3),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t42,plain,
c_union(c_minus(X1,X2,tc_set(X3)),X2,X3) = c_union(X1,X2,X3),
inference(orient,[status(thm)],[t6]) ).
cnf(t188,plain,
true = c_lessequals(c_minus(X1,X2,tc_set(X3)),c_union(X1,X2,X3),tc_set(X3)),
inference(cp,[status(thm)],[t183,t42]) ).
cnf(t1533,plain,
c_lessequals(c_minus(X1,X2,tc_set(X3)),c_union(X1,X2,X3),tc_set(X3)) = true,
inference(orient,[status(thm)],[t188]) ).
cnf(t1557,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)],[t533,t1533]) ).
cnf(t20637,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)],[t1557,t26]) ).
cnf(f11,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/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__subset__iff_1) ).
fof(f11_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)],[f11]) ).
fof(f11_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)],[f11_nnf]) ).
cnf(c11,plain,
( c_lessequals(X1,X3,tc_set(X2))
| ~ c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2)) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t13,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)],[c11]) ).
cnf(t30,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)],[t13]) ).
cnf(t128,plain,
true = ifeq(true,true,c_lessequals(X1,c_union(X2,X1,X3),tc_set(X3)),true),
inference(cp,[status(thm)],[t30,t123]) ).
cnf(t20536,plain,
true = c_lessequals(X1,c_union(X2,X1,X3),tc_set(X3)),
inference(step,[status(thm)],[t128,t26]) ).
cnf(t208,plain,
c_lessequals(X1,c_union(X2,X1,X3),tc_set(X3)) = true,
inference(orient,[status(thm)],[t20536]) ).
cnf(t20638,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)],[t20637,t208]) ).
cnf(t20639,plain,
true = c_lessequals(c_union(X1,X2,X3),c_union(X2,X1,X3),tc_set(X3)),
inference(step,[status(thm)],[t20638,t26]) ).
cnf(t1564,plain,
c_lessequals(c_union(X1,X2,X3),c_union(X2,X1,X3),tc_set(X3)) = true,
inference(orient,[status(thm)],[t20639]) ).
cnf(t1595,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)],[t27,t1564]) ).
cnf(t20644,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)],[t1595,t26]) ).
cnf(t20645,plain,
c_union(X1,X2,X3) = ifeq(true,true,c_union(X2,X1,X3),c_union(X1,X2,X3)),
inference(step,[status(thm)],[t20644,t1564]) ).
cnf(t20646,plain,
c_union(X1,X2,X3) = c_union(X2,X1,X3),
inference(step,[status(thm)],[t20645,t26]) ).
cnf(t1608,plain,
c_union(X1,X2,X3) = c_union(X2,X1,X3),
inference(orient,[status(thm)],[t20646]) ).
cnf(t20750,plain,
c_union(c_Message_Osynth(X1),c_Message_Oanalz(c_union(X1,X2,tc_Message_Omsg)),tc_Message_Omsg) = c_Message_Oanalz(c_union(c_Message_Osynth(X1),X2,tc_Message_Omsg)),
inference(step,[status(thm)],[t1674,t1608]) ).
cnf(t2889,plain,
c_union(c_Message_Osynth(X1),c_Message_Oanalz(c_union(X1,X2,tc_Message_Omsg)),tc_Message_Omsg) = c_Message_Oanalz(c_union(c_Message_Osynth(X1),X2,tc_Message_Omsg)),
inference(orient,[status(thm)],[t20750]) ).
cnf(f2,axiom,
c_Message_Oanalz(c_union(c_Message_Oanalz(V_G),V_H,tc_Message_Omsg)) = c_Message_Oanalz(c_union(V_G,V_H,tc_Message_Omsg)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Message_Oanalz__analz__Un_0) ).
fof(f2_nnf,plain,
! [V_G,V_H] : c_Message_Oanalz(c_union(c_Message_Oanalz(V_G),V_H,tc_Message_Omsg)) = c_Message_Oanalz(c_union(V_G,V_H,tc_Message_Omsg)),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [V_G,V_H] : c_Message_Oanalz(c_union(c_Message_Oanalz(V_G),V_H,tc_Message_Omsg)) = c_Message_Oanalz(c_union(V_G,V_H,tc_Message_Omsg)),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
c_Message_Oanalz(c_union(c_Message_Oanalz(X0),X1,tc_Message_Omsg)) = c_Message_Oanalz(c_union(X0,X1,tc_Message_Omsg)),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t4,plain,
c_Message_Oanalz(c_union(c_Message_Oanalz(X1),X2,tc_Message_Omsg)) = c_Message_Oanalz(c_union(X1,X2,tc_Message_Omsg)),
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t96,plain,
c_Message_Oanalz(c_union(c_Message_Oanalz(X1),X2,tc_Message_Omsg)) = c_Message_Oanalz(c_union(X1,X2,tc_Message_Omsg)),
inference(orient,[status(thm)],[t4]) ).
cnf(t2936,plain,
c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(X1)),X2,tc_Message_Omsg)) = c_union(c_Message_Osynth(c_Message_Oanalz(X1)),c_Message_Oanalz(c_union(X1,X2,tc_Message_Omsg)),tc_Message_Omsg),
inference(cp,[status(thm)],[t2889,t96]) ).
cnf(t6488,plain,
c_union(c_Message_Osynth(c_Message_Oanalz(X1)),c_Message_Oanalz(c_union(X1,X2,tc_Message_Omsg)),tc_Message_Omsg) = c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(X1)),X2,tc_Message_Omsg)),
inference(orient,[status(thm)],[t2936]) ).
cnf(t19,axiom,
sFlat2 = c_Message_Oanalz(v_G),
introduced(definition) ).
cnf(t104,plain,
c_Message_Oanalz(v_G) = sFlat2,
inference(orient,[status(thm)],[t19]) ).
cnf(t20,axiom,
sFlat3 = c_Message_Osynth(c_Message_Oanalz(v_G)),
introduced(definition) ).
cnf(t20520,plain,
sFlat3 = c_Message_Osynth(sFlat2),
inference(step,[status(thm)],[t20,t104]) ).
cnf(t115,plain,
c_Message_Osynth(sFlat2) = sFlat3,
inference(orient,[status(thm)],[t20520]) ).
cnf(f8,axiom,
c_union(c_insert(V_a,V_B,T_a),V_C,T_a) = c_insert(V_a,c_union(V_B,V_C,T_a),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__insert__left_0) ).
fof(f8_nnf,plain,
! [V_a,V_B,T_a,V_C] : c_union(c_insert(V_a,V_B,T_a),V_C,T_a) = c_insert(V_a,c_union(V_B,V_C,T_a),T_a),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [V_a,V_B,T_a,V_C] : c_union(c_insert(V_a,V_B,T_a),V_C,T_a) = c_insert(V_a,c_union(V_B,V_C,T_a),T_a),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
c_union(c_insert(X0,X1,X2),X3,X2) = c_insert(X0,c_union(X1,X3,X2),X2),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t8,plain,
c_union(c_insert(X1,X2,X3),X4,X3) = c_insert(X1,c_union(X2,X4,X3),X3),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(f9,axiom,
c_union(V_A,c_insert(V_a,V_B,T_a),T_a) = c_insert(V_a,c_union(V_A,V_B,T_a),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__insert__right_0) ).
fof(f9_nnf,plain,
! [V_A,V_a,V_B,T_a] : c_union(V_A,c_insert(V_a,V_B,T_a),T_a) = c_insert(V_a,c_union(V_A,V_B,T_a),T_a),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [V_A,V_a,V_B,T_a] : c_union(V_A,c_insert(V_a,V_B,T_a),T_a) = c_insert(V_a,c_union(V_A,V_B,T_a),T_a),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
c_union(X0,c_insert(X1,X2,X3),X3) = c_insert(X1,c_union(X0,X2,X3),X3),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t7,plain,
c_union(X1,c_insert(X2,X3,X4),X4) = c_insert(X2,c_union(X1,X3,X4),X4),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t45,plain,
c_insert(X1,c_union(X2,X3,X4),X4) = c_union(X2,c_insert(X1,X3,X4),X4),
inference(orient,[status(thm)],[t7]) ).
cnf(t20507,plain,
c_union(c_insert(X1,X2,X3),X4,X3) = c_union(X2,c_insert(X1,X4,X3),X3),
inference(step,[status(thm)],[t8,t45]) ).
cnf(t64,plain,
c_union(c_insert(X1,X2,X3),X4,X3) = c_union(X2,c_insert(X1,X4,X3),X3),
inference(orient,[status(thm)],[t20507]) ).
cnf(t111,plain,
c_union(v_H,c_insert(v_X,X1,tc_Message_Omsg),tc_Message_Omsg) = c_union(sFlat0,X1,tc_Message_Omsg),
inference(cp,[status(thm)],[t64,t110]) ).
cnf(t300,plain,
c_union(v_H,c_insert(v_X,X1,tc_Message_Omsg),tc_Message_Omsg) = c_union(sFlat0,X1,tc_Message_Omsg),
inference(orient,[status(thm)],[t111]) ).
cnf(t24,axiom,
sFlat7 = tc_set(tc_Message_Omsg),
introduced(definition) ).
cnf(t78,plain,
tc_set(tc_Message_Omsg) = sFlat7,
inference(orient,[status(thm)],[t24]) ).
cnf(t88,plain,
X1 = ifeq(c_lessequals(X1,X2,sFlat7),true,ifeq(c_lessequals(X2,X1,tc_set(tc_Message_Omsg)),true,X2,X1),X1),
inference(cp,[status(thm)],[t27,t78]) ).
cnf(t21110,plain,
X1 = ifeq(c_lessequals(X1,X2,sFlat7),true,ifeq(c_lessequals(X2,X1,sFlat7),true,X2,X1),X1),
inference(step,[status(thm)],[t88,t78]) ).
cnf(t14879,plain,
ifeq(c_lessequals(X1,X2,sFlat7),true,ifeq(c_lessequals(X2,X1,sFlat7),true,X2,X1),X1) = X1,
inference(orient,[status(thm)],[t21110]) ).
cnf(f14,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/sandbox/benchmark/theBenchmark.p',cls_Set_Oinsert__subset_2) ).
fof(f14_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)],[f14]) ).
fof(f14_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)],[f14_nnf]) ).
cnf(c14,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)],[f14_sk]) ).
cnf(t15,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)],[c14]) ).
cnf(t34,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)],[t15]) ).
cnf(t130,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)],[t34,t123]) ).
cnf(t21243,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)],[t130,t26]) ).
cnf(t20434,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)],[t21243]) ).
cnf(f0,negated_conjecture,
c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f0_nnf,plain,
c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f0]) ).
cnf(c0,plain,
c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f0_nnf]) ).
cnf(t2,plain,
c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t37,plain,
c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t20513,plain,
c_in(v_X,c_Message_Osynth(sFlat2),tc_Message_Omsg) = true,
inference(step,[status(thm)],[t37,t104]) ).
cnf(t106,plain,
c_in(v_X,c_Message_Osynth(sFlat2),tc_Message_Omsg) = true,
inference(rw,[status(thm)],[t20513]) ).
cnf(t20524,plain,
c_in(v_X,sFlat3,tc_Message_Omsg) = true,
inference(step,[status(thm)],[t106,t115]) ).
cnf(t135,plain,
c_in(v_X,sFlat3,tc_Message_Omsg) = true,
inference(orient,[status(thm)],[t20524]) ).
cnf(t20435,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)],[t20434,t135]) ).
cnf(t21244,plain,
true = c_lessequals(c_insert(v_X,sFlat3,tc_Message_Omsg),sFlat3,tc_set(tc_Message_Omsg)),
inference(step,[status(thm)],[t20435,t26]) ).
cnf(t21245,plain,
true = c_lessequals(c_insert(v_X,sFlat3,tc_Message_Omsg),sFlat3,sFlat7),
inference(step,[status(thm)],[t21244,t78]) ).
cnf(t20441,plain,
c_lessequals(c_insert(v_X,sFlat3,tc_Message_Omsg),sFlat3,sFlat7) = true,
inference(orient,[status(thm)],[t21245]) ).
cnf(t20442,plain,
c_insert(v_X,sFlat3,tc_Message_Omsg) = ifeq(true,true,ifeq(c_lessequals(sFlat3,c_insert(v_X,sFlat3,tc_Message_Omsg),sFlat7),true,sFlat3,c_insert(v_X,sFlat3,tc_Message_Omsg)),c_insert(v_X,sFlat3,tc_Message_Omsg)),
inference(cp,[status(thm)],[t14879,t20441]) ).
cnf(t21246,plain,
c_insert(v_X,sFlat3,tc_Message_Omsg) = ifeq(c_lessequals(sFlat3,c_insert(v_X,sFlat3,tc_Message_Omsg),sFlat7),true,sFlat3,c_insert(v_X,sFlat3,tc_Message_Omsg)),
inference(step,[status(thm)],[t20442,t26]) ).
cnf(f13,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/sandbox/benchmark/theBenchmark.p',cls_Set_Oinsert__subset_1) ).
fof(f13_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)],[f13]) ).
fof(f13_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)],[f13_nnf]) ).
cnf(c13,plain,
( c_lessequals(X1,X3,tc_set(X2))
| ~ c_lessequals(c_insert(X0,X1,X2),X3,tc_set(X2)) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t11,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)],[c13]) ).
cnf(t32,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)],[t11]) ).
cnf(t124,plain,
true = ifeq(true,true,c_lessequals(X1,c_insert(X2,X1,X3),tc_set(X3)),true),
inference(cp,[status(thm)],[t32,t123]) ).
cnf(t20531,plain,
true = c_lessequals(X1,c_insert(X2,X1,X3),tc_set(X3)),
inference(step,[status(thm)],[t124,t26]) ).
cnf(t163,plain,
c_lessequals(X1,c_insert(X2,X1,X3),tc_set(X3)) = true,
inference(orient,[status(thm)],[t20531]) ).
cnf(t166,plain,
true = c_lessequals(X1,c_insert(X2,X1,tc_Message_Omsg),sFlat7),
inference(cp,[status(thm)],[t163,t78]) ).
cnf(t181,plain,
c_lessequals(X1,c_insert(X2,X1,tc_Message_Omsg),sFlat7) = true,
inference(orient,[status(thm)],[t166]) ).
cnf(t21247,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)],[t21246,t181]) ).
cnf(t21248,plain,
c_insert(v_X,sFlat3,tc_Message_Omsg) = sFlat3,
inference(step,[status(thm)],[t21247,t26]) ).
cnf(t20450,plain,
c_insert(v_X,sFlat3,tc_Message_Omsg) = sFlat3,
inference(orient,[status(thm)],[t21248]) ).
cnf(t20453,plain,
c_union(sFlat0,sFlat3,tc_Message_Omsg) = c_union(v_H,sFlat3,tc_Message_Omsg),
inference(cp,[status(thm)],[t300,t20450]) ).
cnf(t21249,plain,
c_union(sFlat0,sFlat3,tc_Message_Omsg) = c_union(sFlat3,v_H,tc_Message_Omsg),
inference(step,[status(thm)],[t20453,t1608]) ).
cnf(t20474,plain,
c_union(sFlat3,v_H,tc_Message_Omsg) = c_union(sFlat0,sFlat3,tc_Message_Omsg),
inference(orient,[status(thm)],[t21249]) ).
cnf(f3,axiom,
( c_lessequals(c_Message_Oanalz(V_G),c_Message_Oanalz(V_H),tc_set(tc_Message_Omsg))
| ~ c_lessequals(V_G,V_H,tc_set(tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Message_Oanalz__mono_0) ).
fof(f3_nnf,plain,
! [V_G,V_H] :
( c_lessequals(c_Message_Oanalz(V_G),c_Message_Oanalz(V_H),tc_set(tc_Message_Omsg))
| ~ c_lessequals(V_G,V_H,tc_set(tc_Message_Omsg)) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [V_G,V_H] :
( c_lessequals(c_Message_Oanalz(V_G),c_Message_Oanalz(V_H),tc_set(tc_Message_Omsg))
| ~ c_lessequals(V_G,V_H,tc_set(tc_Message_Omsg)) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( c_lessequals(c_Message_Oanalz(X0),c_Message_Oanalz(X1),tc_set(tc_Message_Omsg))
| ~ c_lessequals(X0,X1,tc_set(tc_Message_Omsg)) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t10,plain,
ifeq(c_lessequals(X1,X2,tc_set(tc_Message_Omsg)),true,c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(X2),tc_set(tc_Message_Omsg)),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t29,plain,
ifeq(c_lessequals(X1,X2,tc_set(tc_Message_Omsg)),true,c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(X2),tc_set(tc_Message_Omsg)),true) = true,
inference(orient,[status(thm)],[t10]) ).
cnf(t20509,plain,
ifeq(c_lessequals(X1,X2,sFlat7),true,c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(X2),tc_set(tc_Message_Omsg)),true) = true,
inference(step,[status(thm)],[t29,t78]) ).
cnf(t20510,plain,
ifeq(c_lessequals(X1,X2,sFlat7),true,c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(X2),sFlat7),true) = true,
inference(step,[status(thm)],[t20509,t78]) ).
cnf(t95,plain,
ifeq(c_lessequals(X1,X2,sFlat7),true,c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(X2),sFlat7),true) = true,
inference(rw,[status(thm)],[t20510]) ).
cnf(t10352,plain,
ifeq(c_lessequals(X1,X2,sFlat7),true,c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(X2),sFlat7),true) = true,
inference(orient,[status(thm)],[t95]) ).
cnf(t214,plain,
true = c_lessequals(X1,c_union(X2,X1,tc_Message_Omsg),sFlat7),
inference(cp,[status(thm)],[t208,t78]) ).
cnf(t230,plain,
c_lessequals(X1,c_union(X2,X1,tc_Message_Omsg),sFlat7) = true,
inference(orient,[status(thm)],[t214]) ).
cnf(t10359,plain,
true = ifeq(true,true,c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(c_union(X2,X1,tc_Message_Omsg)),sFlat7),true),
inference(cp,[status(thm)],[t10352,t230]) ).
cnf(t20979,plain,
true = c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(c_union(X2,X1,tc_Message_Omsg)),sFlat7),
inference(step,[status(thm)],[t10359,t26]) ).
cnf(t11041,plain,
c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(c_union(X2,X1,tc_Message_Omsg)),sFlat7) = true,
inference(orient,[status(thm)],[t20979]) ).
cnf(t11201,plain,
true = c_lessequals(sFlat1,c_Message_Oanalz(c_union(X1,sFlat0,tc_Message_Omsg)),sFlat7),
inference(cp,[status(thm)],[t11041,t120]) ).
cnf(t11438,plain,
c_lessequals(sFlat1,c_Message_Oanalz(c_union(X1,sFlat0,tc_Message_Omsg)),sFlat7) = true,
inference(orient,[status(thm)],[t11201]) ).
cnf(t11445,plain,
true = c_lessequals(sFlat1,c_Message_Oanalz(c_union(sFlat0,X1,tc_Message_Omsg)),sFlat7),
inference(cp,[status(thm)],[t11438,t1608]) ).
cnf(t11484,plain,
c_lessequals(sFlat1,c_Message_Oanalz(c_union(sFlat0,X1,tc_Message_Omsg)),sFlat7) = true,
inference(orient,[status(thm)],[t11445]) ).
cnf(f1,negated_conjecture,
~ c_lessequals(c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg),tc_set(tc_Message_Omsg)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1_nnf,plain,
~ c_lessequals(c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg),tc_set(tc_Message_Omsg)),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
~ c_lessequals(c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg),tc_set(tc_Message_Omsg)),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
~ c_lessequals(c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg),tc_set(tc_Message_Omsg)),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(goal_0,negated_conjecture,
c_lessequals(c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg),tc_set(tc_Message_Omsg)) != true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(g0_0,plain,
c_lessequals(c_Message_Oanalz(sFlat0),c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg),tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[goal_0,t110]) ).
cnf(g0_1,plain,
c_lessequals(sFlat1,c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg),tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[g0_0,t120]) ).
cnf(g0_2,plain,
c_lessequals(sFlat1,c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg)),tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[g0_1,t6488]) ).
cnf(g0_3,plain,
c_lessequals(sFlat1,c_Message_Oanalz(c_union(v_H,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg)),tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[g0_2,t1608]) ).
cnf(g0_4,plain,
c_lessequals(sFlat1,c_Message_Oanalz(c_union(v_H,c_Message_Osynth(sFlat2),tc_Message_Omsg)),tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[g0_3,t104]) ).
cnf(g0_5,plain,
c_lessequals(sFlat1,c_Message_Oanalz(c_union(v_H,sFlat3,tc_Message_Omsg)),tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[g0_4,t115]) ).
cnf(g0_6,plain,
c_lessequals(sFlat1,c_Message_Oanalz(c_union(sFlat3,v_H,tc_Message_Omsg)),tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[g0_5,t1608]) ).
cnf(g0_7,plain,
c_lessequals(sFlat1,c_Message_Oanalz(c_union(sFlat0,sFlat3,tc_Message_Omsg)),tc_set(tc_Message_Omsg)) != true,
inference(rw,[status(thm)],[g0_6,t20474]) ).
cnf(g0_8,plain,
c_lessequals(sFlat1,c_Message_Oanalz(c_union(sFlat0,sFlat3,tc_Message_Omsg)),sFlat7) != true,
inference(rw,[status(thm)],[g0_7,t78]) ).
cnf(g0_9,plain,
true != true,
inference(rw,[status(thm)],[g0_8,t11484]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV249-2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n013.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 18:52:38 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 44.20/6.28 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 44.20/6.28 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------