%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : RNG001-3 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:04:55 PM UTC 2026
% Result : Unsatisfiable 49.46s 25.67s
% Output : CNFRefutation 50.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 8
% Syntax : Number of clauses : 318 ( 187 unt; 0 nHn; 135 RR)
% Number of literals : 686 ( 0 equ; 393 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 921 ( 122 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(distributivity2,axiom,
( product(X1,X6,X7)
| ~ product(X1,X2,X3)
| ~ product(X1,X4,X5)
| ~ sum(X2,X4,X6)
| ~ sum(X3,X5,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distributivity2) ).
cnf(distributivity1,axiom,
( sum(X3,X5,X7)
| ~ product(X1,X2,X3)
| ~ product(X1,X4,X5)
| ~ sum(X2,X4,X6)
| ~ product(X1,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distributivity1) ).
cnf(associativity_of_addition1,axiom,
( sum(X1,X5,X6)
| ~ sum(X1,X2,X3)
| ~ sum(X2,X4,X5)
| ~ sum(X3,X4,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_addition1) ).
cnf(associativity_of_addition2,axiom,
( sum(X3,X4,X6)
| ~ sum(X1,X2,X3)
| ~ sum(X2,X4,X5)
| ~ sum(X1,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_addition2) ).
cnf(closure_of_multiplication,axiom,
product(X1,X2,multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closure_of_multiplication) ).
cnf(prove_a_times_additive_id_is_additive_id,negated_conjecture,
~ product(a,additive_identity,additive_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_a_times_additive_id_is_additive_id) ).
cnf(additive_inverse1,axiom,
sum(additive_inverse(X1),X1,additive_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_inverse1) ).
cnf(additive_identity1,axiom,
sum(additive_identity,X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_identity1) ).
cnf(i_0_8,axiom,
( product(X1,X6,X7)
| ~ product(X1,X2,X3)
| ~ product(X1,X4,X5)
| ~ sum(X2,X4,X6)
| ~ sum(X3,X5,X7) ),
distributivity2,
[final] ).
cnf(i_0_9,axiom,
( sum(X3,X5,X7)
| ~ product(X1,X2,X3)
| ~ product(X1,X4,X5)
| ~ sum(X2,X4,X6)
| ~ product(X1,X6,X7) ),
distributivity1,
[final] ).
cnf(i_0_10,axiom,
( sum(X1,X5,X6)
| ~ sum(X1,X2,X3)
| ~ sum(X2,X4,X5)
| ~ sum(X3,X4,X6) ),
associativity_of_addition1,
[final] ).
cnf(i_0_11,axiom,
( sum(X3,X4,X6)
| ~ sum(X1,X2,X3)
| ~ sum(X2,X4,X5)
| ~ sum(X1,X5,X6) ),
associativity_of_addition2,
[final] ).
cnf(i_0_12,axiom,
product(X1,X2,multiply(X1,X2)),
closure_of_multiplication,
[final] ).
cnf(i_0_13,negated_conjecture,
~ product(a,additive_identity,additive_identity),
prove_a_times_additive_id_is_additive_id,
[final] ).
cnf(i_0_14,axiom,
sum(additive_inverse(X1),X1,additive_identity),
additive_inverse1,
[final] ).
cnf(i_0_15,axiom,
sum(additive_identity,X1,X1),
additive_identity1,
[final] ).
cnf(i_0_16,plain,
sum(multiply(X1,additive_identity),multiply(X1,additive_identity),multiply(X1,additive_identity)),
inference(scs_inference,[],[i_0_15,i_0_12,i_0_9]) ).
cnf(i_0_17,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_18,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_19,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_20,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_21,plain,
( ~ product(X1,X2,X3)
| sum(X4,X5,X3)
| ~ product(X1,X6,X4)
| ~ product(X1,X7,X5)
| ~ sum(X6,X7,X2) ),
inference(rename_variables,[],[i_0_9]) ).
cnf(i_0_22,plain,
( ~ product(a,additive_inverse(X1),additive_identity)
| ~ product(a,X1,additive_identity) ),
inference(scs_inference,[],[i_0_13,i_0_15,i_0_20,i_0_12,i_0_14,i_0_9,i_0_8]) ).
cnf(i_0_23,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_24,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_25,plain,
sum(additive_inverse(multiply(X1,additive_identity)),multiply(X1,additive_identity),multiply(X1,additive_identity)),
inference(scs_inference,[],[i_0_14,i_0_16,i_0_15,i_0_10]) ).
cnf(i_0_26,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_27,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_28,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_29,plain,
sum(additive_identity,multiply(X1,additive_identity),additive_identity),
inference(scs_inference,[],[i_0_14,i_0_27,i_0_16,i_0_15,i_0_10,i_0_11]) ).
cnf(i_0_30,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_31,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_32,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_33,plain,
~ product(a,additive_inverse(X1),additive_inverse(multiply(a,X1))),
inference(scs_inference,[],[i_0_13,i_0_14,i_0_27,i_0_31,i_0_30,i_0_16,i_0_15,i_0_12,i_0_10,i_0_11,i_0_8]) ).
cnf(i_0_34,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_35,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_36,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_37,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_38,plain,
~ product(a,additive_identity,additive_inverse(multiply(a,additive_identity))),
inference(scs_inference,[],[i_0_13,i_0_14,i_0_15,i_0_12,i_0_8]) ).
cnf(i_0_39,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_40,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_41,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_42,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_43,plain,
( ~ product(a,additive_inverse(X1),additive_inverse(X1))
| ~ product(a,X1,X1) ),
inference(scs_inference,[],[i_0_13,i_0_14,i_0_8]) ).
cnf(i_0_44,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_45,plain,
sum(additive_inverse(additive_identity),additive_identity,multiply(X1,additive_identity)),
inference(scs_inference,[],[i_0_14,i_0_29,i_0_15,i_0_10]) ).
cnf(i_0_46,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_47,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_48,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_49,plain,
( product(X1,multiply(X2,additive_identity),multiply(X2,additive_identity))
| ~ product(X1,multiply(X2,additive_identity),multiply(X2,additive_identity)) ),
inference(scs_inference,[],[i_0_14,i_0_29,i_0_16,i_0_15,i_0_10,i_0_8]) ).
cnf(i_0_50,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_51,plain,
sum(multiply(X1,additive_identity),multiply(X2,additive_identity),multiply(X1,additive_identity)),
inference(scs_inference,[],[i_0_29,i_0_45,i_0_11]) ).
cnf(i_0_52,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_53,plain,
~ product(a,additive_inverse(additive_identity),additive_identity),
inference(scs_inference,[],[i_0_13,i_0_29,i_0_14,i_0_45,i_0_12,i_0_11,i_0_8]) ).
cnf(i_0_54,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_55,plain,
sum(additive_identity,multiply(X1,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_56,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_57,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_58,plain,
sum(additive_identity,multiply(X1,additive_identity),multiply(X2,additive_identity)),
inference(scs_inference,[],[i_0_29,i_0_15,i_0_51,i_0_10]) ).
cnf(i_0_59,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_60,plain,
sum(additive_identity,multiply(X1,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_61,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_63,plain,
( product(X1,multiply(X2,additive_identity),multiply(X2,additive_identity))
| ~ product(X1,additive_identity,additive_identity)
| ~ product(X1,multiply(X3,additive_identity),multiply(X3,additive_identity)) ),
inference(scs_inference,[],[i_0_58,i_0_8]) ).
cnf(i_0_65,plain,
( product(X1,multiply(X2,additive_identity),multiply(X2,additive_identity))
| ~ product(X1,additive_inverse(additive_identity),additive_inverse(additive_identity))
| ~ product(X1,additive_identity,additive_identity) ),
inference(scs_inference,[],[i_0_45,i_0_8]) ).
cnf(i_0_280,plain,
sum(additive_inverse(additive_identity),multiply(X1,additive_identity),multiply(X1,additive_identity)),
inference(scs_inference,[],[i_0_14,i_0_58,i_0_10]) ).
cnf(i_0_281,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_282,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_395,plain,
sum(multiply(X1,additive_identity),additive_identity,multiply(X1,additive_identity)),
inference(scs_inference,[],[i_0_15,i_0_45,i_0_11]) ).
cnf(i_0_396,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_397,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_510,plain,
sum(multiply(X1,additive_identity),additive_identity,additive_identity),
inference(scs_inference,[],[i_0_25,i_0_14,i_0_395,i_0_11]) ).
cnf(i_0_511,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_512,plain,
sum(additive_inverse(multiply(X1,additive_identity)),multiply(X1,additive_identity),multiply(X1,additive_identity)),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_513,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_514,plain,
sum(additive_inverse(multiply(X1,additive_identity)),additive_identity,additive_identity),
inference(scs_inference,[],[i_0_25,i_0_512,i_0_14,i_0_395,i_0_11,i_0_10]) ).
cnf(i_0_515,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_517,plain,
sum(multiply(X1,additive_identity),multiply(X2,additive_identity),additive_identity),
inference(scs_inference,[],[i_0_25,i_0_14,i_0_51,i_0_11]) ).
cnf(i_0_518,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_519,plain,
sum(additive_inverse(multiply(X1,additive_identity)),multiply(X1,additive_identity),multiply(X1,additive_identity)),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_520,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_521,plain,
( ~ product(a,multiply(X1,additive_identity),multiply(X1,additive_identity))
| ~ product(a,multiply(X2,additive_identity),multiply(X2,additive_identity)) ),
inference(scs_inference,[],[i_0_25,i_0_13,i_0_14,i_0_51,i_0_11,i_0_8]) ).
cnf(i_0_522,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_633,plain,
sum(additive_identity,additive_identity,multiply(X1,additive_identity)),
inference(scs_inference,[],[i_0_29,i_0_517,i_0_58,i_0_10]) ).
cnf(i_0_634,plain,
sum(additive_identity,multiply(X1,additive_identity),multiply(X2,additive_identity)),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_635,plain,
sum(additive_identity,multiply(X1,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_636,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_637,plain,
( product(X1,multiply(X2,additive_identity),multiply(X2,additive_identity))
| ~ product(X1,additive_identity,additive_identity) ),
inference(scs_inference,[],[i_0_29,i_0_517,i_0_58,i_0_10,i_0_8]) ).
cnf(i_0_638,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_751,plain,
sum(multiply(X1,additive_identity),additive_identity,multiply(X2,additive_identity)),
inference(scs_inference,[],[i_0_510,i_0_29,i_0_15,i_0_10]) ).
cnf(i_0_752,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_753,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_754,plain,
( ~ product(a,additive_inverse(X1),multiply(X2,additive_identity))
| ~ product(a,X1,additive_identity) ),
inference(scs_inference,[],[i_0_13,i_0_510,i_0_29,i_0_15,i_0_14,i_0_10,i_0_8]) ).
cnf(i_0_755,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_756,plain,
sum(multiply(X1,additive_identity),multiply(X2,additive_identity),multiply(X2,additive_identity)),
inference(scs_inference,[],[i_0_510,i_0_633,i_0_10]) ).
cnf(i_0_757,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_869,plain,
sum(additive_inverse(additive_identity),multiply(X1,additive_identity),additive_identity),
inference(scs_inference,[],[i_0_633,i_0_14,i_0_15,i_0_10]) ).
cnf(i_0_870,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_871,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_872,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_873,plain,
( product(X1,additive_identity,multiply(X2,additive_identity))
| ~ product(X1,additive_inverse(X3),additive_identity)
| ~ product(X1,X3,additive_identity) ),
inference(scs_inference,[],[i_0_633,i_0_14,i_0_871,i_0_15,i_0_10,i_0_8]) ).
cnf(i_0_985,plain,
sum(additive_inverse(additive_inverse(additive_identity)),multiply(X1,additive_identity),additive_identity),
inference(scs_inference,[],[i_0_45,i_0_14,i_0_15,i_0_10]) ).
cnf(i_0_986,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_987,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_988,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_1101,plain,
( product(X1,additive_identity,multiply(X2,additive_identity))
| ~ product(X1,additive_inverse(additive_identity),multiply(X2,additive_identity)) ),
inference(scs_inference,[],[i_0_51,i_0_14,i_0_12,i_0_8]) ).
cnf(i_0_1102,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_1103,plain,
sum(multiply(X1,additive_identity),multiply(X2,additive_identity),multiply(X1,additive_identity)),
inference(rename_variables,[],[i_0_51]) ).
cnf(i_0_1104,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_1105,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_1329,plain,
( product(X1,additive_identity,multiply(X2,additive_identity))
| ~ product(X1,additive_identity,additive_identity) ),
inference(scs_inference,[],[i_0_58,i_0_15,i_0_12,i_0_8]) ).
cnf(i_0_1330,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_1331,plain,
sum(additive_identity,multiply(X1,additive_identity),multiply(X2,additive_identity)),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_1332,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_1333,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_1334,plain,
( sum(multiply(X1,additive_identity),multiply(X1,additive_identity),multiply(X2,additive_identity))
| ~ product(X1,additive_identity,additive_identity) ),
inference(scs_inference,[],[i_0_58,i_0_15,i_0_1330,i_0_12,i_0_1332,i_0_8,i_0_9]) ).
cnf(i_0_1335,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_1336,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_1337,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_1338,plain,
( ~ product(X1,X2,X3)
| sum(X4,X5,X3)
| ~ product(X1,X6,X4)
| ~ product(X1,X7,X5)
| ~ sum(X6,X7,X2) ),
inference(rename_variables,[],[i_0_9]) ).
cnf(i_0_1339,plain,
( product(X1,additive_identity,multiply(X2,additive_identity))
| ~ product(X1,additive_inverse(additive_identity),additive_identity) ),
inference(scs_inference,[],[i_0_58,i_0_14,i_0_12,i_0_8]) ).
cnf(i_0_1340,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_1341,plain,
sum(additive_identity,multiply(X1,additive_identity),multiply(X2,additive_identity)),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_1342,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_1343,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_1344,plain,
( sum(multiply(X1,additive_identity),multiply(X1,additive_identity),multiply(X2,additive_identity))
| ~ product(X1,additive_inverse(additive_identity),additive_identity) ),
inference(scs_inference,[],[i_0_58,i_0_15,i_0_14,i_0_12,i_0_1342,i_0_8,i_0_9]) ).
cnf(i_0_1345,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_1346,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_1347,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_1348,plain,
( ~ product(X1,X2,X3)
| sum(X4,X5,X3)
| ~ product(X1,X6,X4)
| ~ product(X1,X7,X5)
| ~ sum(X6,X7,X2) ),
inference(rename_variables,[],[i_0_9]) ).
cnf(i_0_1683,plain,
sum(additive_inverse(multiply(X1,additive_identity)),X2,X2),
inference(scs_inference,[],[i_0_514,i_0_15,i_0_10]) ).
cnf(i_0_1684,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_1685,plain,
( ~ product(a,additive_inverse(X1),additive_inverse(multiply(X2,additive_identity)))
| ~ product(a,X1,additive_identity) ),
inference(scs_inference,[],[i_0_514,i_0_13,i_0_14,i_0_15,i_0_10,i_0_8]) ).
cnf(i_0_1686,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_1798,plain,
sum(additive_inverse(multiply(X1,additive_identity)),multiply(X2,additive_identity),additive_identity),
inference(scs_inference,[],[i_0_751,i_0_14,i_0_15,i_0_10]) ).
cnf(i_0_1799,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_1800,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_1801,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_1802,plain,
( product(X1,X2,multiply(X3,additive_identity))
| ~ product(X1,X2,additive_identity) ),
inference(scs_inference,[],[i_0_751,i_0_14,i_0_15,i_0_1799,i_0_12,i_0_10,i_0_8]) ).
cnf(i_0_1803,plain,
sum(multiply(X1,additive_identity),additive_identity,multiply(X2,additive_identity)),
inference(rename_variables,[],[i_0_751]) ).
cnf(i_0_1804,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_1805,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_2030,plain,
~ product(a,additive_identity,additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_869,i_0_13,i_0_15,i_0_12,i_0_8]) ).
cnf(i_0_2031,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_2032,plain,
sum(additive_inverse(additive_identity),multiply(X1,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_869]) ).
cnf(i_0_2033,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_2034,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_2035,plain,
~ product(a,additive_inverse(multiply(X1,additive_identity)),additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_869,i_0_13,i_0_1683,i_0_12,i_0_8]) ).
cnf(i_0_2036,plain,
sum(additive_inverse(multiply(X1,additive_identity)),X2,X2),
inference(rename_variables,[],[i_0_1683]) ).
cnf(i_0_2037,plain,
sum(additive_inverse(additive_identity),multiply(X1,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_869]) ).
cnf(i_0_2038,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_2039,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_2040,plain,
~ product(a,additive_inverse(additive_identity),additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_869,i_0_13,i_0_14,i_0_12,i_0_8]) ).
cnf(i_0_2041,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_2042,plain,
sum(additive_inverse(additive_identity),multiply(X1,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_869]) ).
cnf(i_0_2043,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_2044,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_2154,plain,
sum(additive_inverse(additive_inverse(additive_identity)),additive_identity,additive_identity),
inference(scs_inference,[],[i_0_985,i_0_15,i_0_510,i_0_10]) ).
cnf(i_0_2155,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_2156,plain,
sum(additive_inverse(additive_inverse(additive_identity)),multiply(X1,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_985]) ).
cnf(i_0_2157,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_2158,plain,
~ product(a,additive_identity,additive_inverse(additive_inverse(additive_identity))),
inference(scs_inference,[],[i_0_985,i_0_2156,i_0_13,i_0_15,i_0_2155,i_0_510,i_0_12,i_0_10,i_0_8]) ).
cnf(i_0_2159,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_2160,plain,
sum(additive_inverse(additive_inverse(additive_identity)),multiply(X1,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_985]) ).
cnf(i_0_2161,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_2162,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_2163,plain,
( sum(additive_identity,X1,additive_identity)
| ~ sum(multiply(X2,additive_identity),X1,additive_inverse(additive_identity)) ),
inference(scs_inference,[],[i_0_985,i_0_2156,i_0_2160,i_0_13,i_0_15,i_0_2155,i_0_510,i_0_14,i_0_12,i_0_10,i_0_8,i_0_11]) ).
cnf(i_0_2164,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_2165,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_2166,plain,
sum(additive_inverse(additive_inverse(additive_identity)),additive_identity,multiply(X1,additive_identity)),
inference(scs_inference,[],[i_0_985,i_0_510,i_0_633,i_0_10]) ).
cnf(i_0_2167,plain,
sum(additive_inverse(additive_inverse(additive_identity)),multiply(X1,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_985]) ).
cnf(i_0_2168,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_2169,plain,
~ product(a,additive_inverse(additive_identity),additive_inverse(additive_inverse(additive_identity))),
inference(scs_inference,[],[i_0_985,i_0_2167,i_0_13,i_0_510,i_0_633,i_0_14,i_0_12,i_0_10,i_0_8]) ).
cnf(i_0_2170,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_2171,plain,
sum(additive_inverse(additive_inverse(additive_identity)),multiply(X1,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_985]) ).
cnf(i_0_2172,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_2173,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_2396,plain,
sum(additive_inverse(multiply(X1,additive_identity)),additive_identity,multiply(X2,additive_identity)),
inference(scs_inference,[],[i_0_1798,i_0_510,i_0_633,i_0_10]) ).
cnf(i_0_2397,plain,
sum(additive_inverse(multiply(X1,additive_identity)),multiply(X2,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_1798]) ).
cnf(i_0_2398,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_2399,plain,
~ product(a,additive_identity,additive_inverse(multiply(X1,additive_identity))),
inference(scs_inference,[],[i_0_1798,i_0_2397,i_0_13,i_0_510,i_0_633,i_0_15,i_0_12,i_0_10,i_0_8]) ).
cnf(i_0_2400,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_2401,plain,
sum(additive_inverse(multiply(X1,additive_identity)),multiply(X2,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_1798]) ).
cnf(i_0_2402,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_2403,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_2739,plain,
sum(additive_identity,additive_inverse(additive_identity),additive_identity),
inference(scs_inference,[],[i_0_2154,i_0_14,i_0_15,i_0_11]) ).
cnf(i_0_2740,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_2741,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_2742,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_2743,plain,
sum(additive_inverse(additive_inverse(additive_identity)),multiply(X1,additive_identity),multiply(X1,additive_identity)),
inference(scs_inference,[],[i_0_2154,i_0_633,i_0_14,i_0_15,i_0_11,i_0_10]) ).
cnf(i_0_2744,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_2745,plain,
( ~ product(a,additive_inverse(X1),additive_inverse(additive_inverse(additive_identity)))
| ~ product(a,X1,additive_identity) ),
inference(scs_inference,[],[i_0_2154,i_0_13,i_0_633,i_0_14,i_0_2740,i_0_15,i_0_11,i_0_10,i_0_8]) ).
cnf(i_0_2746,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_2747,plain,
( sum(additive_identity,X1,additive_identity)
| ~ sum(additive_inverse(additive_identity),X1,additive_inverse(additive_identity)) ),
inference(scs_inference,[],[i_0_2739,i_0_11]) ).
cnf(i_0_2748,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_2749,plain,
( sum(additive_identity,X1,additive_identity)
| ~ sum(additive_inverse(additive_identity),additive_inverse(additive_identity),X1) ),
inference(scs_inference,[],[i_0_2739,i_0_11,i_0_10]) ).
cnf(i_0_2750,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_2813,plain,
sum(multiply(X1,additive_identity),additive_inverse(additive_identity),multiply(X1,additive_identity)),
inference(scs_inference,[],[i_0_633,i_0_2739,i_0_11]) ).
cnf(i_0_2814,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_2815,plain,
( sum(multiply(X1,additive_identity),X2,multiply(X1,additive_identity))
| ~ sum(additive_inverse(additive_identity),additive_inverse(additive_identity),X2) ),
inference(scs_inference,[],[i_0_633,i_0_2739,i_0_11,i_0_10]) ).
cnf(i_0_2816,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_2818,plain,
( sum(multiply(X1,additive_identity),X2,multiply(X1,additive_identity))
| ~ sum(additive_inverse(additive_identity),X2,additive_inverse(additive_identity)) ),
inference(scs_inference,[],[i_0_2813,i_0_11]) ).
cnf(i_0_2819,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_2849,plain,
sum(additive_inverse(additive_inverse(additive_identity)),additive_identity,additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_2154,i_0_2739,i_0_15,i_0_10]) ).
cnf(i_0_2850,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_2851,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_2852,plain,
sum(additive_inverse(additive_identity),additive_inverse(additive_identity),additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_2154,i_0_2739,i_0_15,i_0_10,i_0_11]) ).
cnf(i_0_2853,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_2873,plain,
sum(additive_identity,additive_inverse(additive_identity),multiply(X1,additive_identity)),
inference(scs_inference,[],[i_0_29,i_0_15,i_0_2813,i_0_11]) ).
cnf(i_0_2874,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_2875,plain,
sum(additive_identity,multiply(X1,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_2876,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_2877,plain,
sum(additive_identity,multiply(X1,additive_identity),additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_29,i_0_2875,i_0_15,i_0_2874,i_0_2813,i_0_11,i_0_10]) ).
cnf(i_0_2878,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_2879,plain,
sum(additive_identity,multiply(X1,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_2880,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_2881,plain,
~ product(a,additive_inverse(multiply(X1,additive_identity)),additive_identity),
inference(scs_inference,[],[i_0_13,i_0_29,i_0_2875,i_0_2879,i_0_15,i_0_2874,i_0_2813,i_0_1683,i_0_12,i_0_11,i_0_10,i_0_8]) ).
cnf(i_0_2882,plain,
sum(additive_inverse(multiply(X1,additive_identity)),X2,X2),
inference(rename_variables,[],[i_0_1683]) ).
cnf(i_0_2883,plain,
sum(additive_identity,multiply(X1,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_2884,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_2885,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_2886,plain,
sum(additive_inverse(additive_identity),multiply(X1,additive_identity),additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_29,i_0_2849,i_0_11]) ).
cnf(i_0_2887,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_2888,plain,
sum(additive_identity,additive_identity,additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_29,i_0_517,i_0_2849,i_0_2877,i_0_11,i_0_10]) ).
cnf(i_0_2889,plain,
sum(additive_identity,multiply(X1,additive_identity),additive_inverse(additive_identity)),
inference(rename_variables,[],[i_0_2877]) ).
cnf(i_0_2890,plain,
sum(additive_identity,multiply(X1,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_2891,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_2893,plain,
sum(additive_inverse(additive_identity),additive_identity,additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_517,i_0_2886,i_0_10]) ).
cnf(i_0_2894,plain,
sum(additive_inverse(additive_identity),multiply(X1,additive_identity),additive_inverse(additive_identity)),
inference(rename_variables,[],[i_0_2886]) ).
cnf(i_0_2895,plain,
sum(multiply(X1,additive_identity),multiply(X2,additive_identity),additive_identity),
inference(rename_variables,[],[i_0_517]) ).
cnf(i_0_2896,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_3007,plain,
sum(multiply(X1,additive_identity),additive_inverse(additive_identity),additive_identity),
inference(scs_inference,[],[i_0_2166,i_0_14,i_0_15,i_0_11]) ).
cnf(i_0_3008,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_3009,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_3010,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_3011,plain,
( product(X1,additive_identity,multiply(X2,additive_identity))
| ~ product(X1,additive_inverse(X3),additive_inverse(additive_inverse(additive_identity)))
| ~ product(X1,X3,additive_identity) ),
inference(scs_inference,[],[i_0_2166,i_0_14,i_0_3008,i_0_15,i_0_11,i_0_8]) ).
cnf(i_0_3235,plain,
sum(additive_inverse(additive_identity),additive_inverse(additive_identity),additive_identity),
inference(scs_inference,[],[i_0_2877,i_0_3007,i_0_15,i_0_11]) ).
cnf(i_0_3236,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_3237,plain,
sum(additive_identity,multiply(X1,additive_identity),additive_inverse(additive_identity)),
inference(rename_variables,[],[i_0_2877]) ).
cnf(i_0_3238,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_3239,plain,
sum(additive_inverse(multiply(X1,additive_identity)),additive_inverse(additive_identity),additive_identity),
inference(scs_inference,[],[i_0_2396,i_0_2877,i_0_3007,i_0_15,i_0_3236,i_0_11,i_0_10]) ).
cnf(i_0_3240,plain,
sum(multiply(X1,additive_identity),additive_inverse(additive_identity),additive_identity),
inference(rename_variables,[],[i_0_3007]) ).
cnf(i_0_3241,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_3242,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_3244,plain,
sum(multiply(X1,additive_identity),multiply(X2,additive_identity),additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_2396,i_0_2877,i_0_1683,i_0_11]) ).
cnf(i_0_3245,plain,
sum(additive_inverse(multiply(X1,additive_identity)),X2,X2),
inference(rename_variables,[],[i_0_1683]) ).
cnf(i_0_3246,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_3247,plain,
sum(additive_inverse(additive_identity),additive_inverse(additive_identity),multiply(X1,additive_identity)),
inference(scs_inference,[],[i_0_2396,i_0_2893,i_0_2877,i_0_1683,i_0_280,i_0_11,i_0_10]) ).
cnf(i_0_3248,plain,
sum(additive_inverse(additive_identity),multiply(X1,additive_identity),multiply(X1,additive_identity)),
inference(rename_variables,[],[i_0_280]) ).
cnf(i_0_3249,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_3250,plain,
( product(X1,multiply(X2,additive_identity),multiply(X2,additive_identity))
| ~ product(X1,additive_inverse(additive_identity),additive_inverse(additive_identity)) ),
inference(scs_inference,[],[i_0_2396,i_0_2893,i_0_2877,i_0_1683,i_0_280,i_0_11,i_0_10,i_0_8]) ).
cnf(i_0_3251,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_3376,plain,
sum(multiply(X1,additive_identity),X2,X2),
inference(scs_inference,[],[i_0_510,i_0_15,i_0_10]) ).
cnf(i_0_3377,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_3379,plain,
sum(additive_inverse(additive_inverse(additive_identity)),additive_inverse(additive_identity),additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_2743,i_0_3244,i_0_10]) ).
cnf(i_0_3380,plain,
sum(multiply(X1,additive_identity),multiply(X2,additive_identity),additive_inverse(additive_identity)),
inference(rename_variables,[],[i_0_3244]) ).
cnf(i_0_3381,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_3480,plain,
sum(multiply(X1,additive_identity),additive_identity,additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_2813,i_0_869,i_0_3244,i_0_10]) ).
cnf(i_0_3481,plain,
sum(multiply(X1,additive_identity),multiply(X2,additive_identity),additive_inverse(additive_identity)),
inference(rename_variables,[],[i_0_3244]) ).
cnf(i_0_3482,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_3483,plain,
( product(X1,X2,multiply(X1,additive_identity))
| ~ product(X1,X2,additive_inverse(additive_identity)) ),
inference(scs_inference,[],[i_0_2813,i_0_15,i_0_869,i_0_3244,i_0_12,i_0_10,i_0_8]) ).
cnf(i_0_3484,plain,
sum(multiply(X1,additive_identity),additive_inverse(additive_identity),multiply(X1,additive_identity)),
inference(rename_variables,[],[i_0_2813]) ).
cnf(i_0_3485,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_3486,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_3711,plain,
( ~ product(a,additive_inverse(X1),additive_inverse(additive_identity))
| ~ product(a,X1,additive_inverse(additive_identity)) ),
inference(scs_inference,[],[i_0_2852,i_0_2030,i_0_14,i_0_8]) ).
cnf(i_0_3712,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_3824,plain,
sum(multiply(X1,additive_identity),additive_inverse(additive_identity),multiply(X2,additive_identity)),
inference(scs_inference,[],[i_0_2873,i_0_15,i_0_3247,i_0_11]) ).
cnf(i_0_3825,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_3826,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_3828,plain,
( ~ product(a,multiply(X1,additive_identity),additive_identity)
| ~ product(a,additive_inverse(additive_identity),multiply(X2,additive_identity)) ),
inference(scs_inference,[],[i_0_2877,i_0_2040,i_0_3376,i_0_8]) ).
cnf(i_0_3829,plain,
sum(multiply(X1,additive_identity),X2,X2),
inference(rename_variables,[],[i_0_3376]) ).
cnf(i_0_3830,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_3941,plain,
sum(multiply(X1,additive_identity),multiply(X2,additive_identity),multiply(X3,additive_identity)),
inference(scs_inference,[],[i_0_3007,i_0_3247,i_0_2873,i_0_10]) ).
cnf(i_0_3942,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_3943,plain,
( ~ product(a,additive_inverse(X1),multiply(X2,additive_identity))
| ~ product(a,X1,additive_inverse(additive_identity)) ),
inference(scs_inference,[],[i_0_13,i_0_3007,i_0_14,i_0_3247,i_0_2873,i_0_10,i_0_8]) ).
cnf(i_0_3944,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_4168,plain,
( ~ product(a,additive_inverse(X1),additive_inverse(additive_identity))
| ~ product(a,X1,additive_identity) ),
inference(scs_inference,[],[i_0_2893,i_0_2030,i_0_14,i_0_8]) ).
cnf(i_0_4169,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_4393,plain,
sum(additive_inverse(multiply(X1,additive_identity)),additive_identity,additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_1683,i_0_3007,i_0_3376,i_0_10]) ).
cnf(i_0_4394,plain,
sum(multiply(X1,additive_identity),X2,X2),
inference(rename_variables,[],[i_0_3376]) ).
cnf(i_0_4395,plain,
sum(additive_inverse(multiply(X1,additive_identity)),X2,X2),
inference(rename_variables,[],[i_0_1683]) ).
cnf(i_0_4396,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_4509,plain,
sum(additive_inverse(multiply(X1,additive_identity)),multiply(X2,additive_identity),additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_3239,i_0_15,i_0_3247,i_0_10]) ).
cnf(i_0_4510,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_4511,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_4512,plain,
( ~ product(a,additive_inverse(X1),additive_inverse(multiply(X2,additive_identity)))
| ~ product(a,X1,additive_inverse(additive_identity)) ),
inference(scs_inference,[],[i_0_3239,i_0_13,i_0_15,i_0_3247,i_0_14,i_0_10,i_0_8]) ).
cnf(i_0_4513,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_4514,plain,
sum(additive_inverse(multiply(X1,additive_identity)),additive_inverse(additive_identity),multiply(X2,additive_identity)),
inference(scs_inference,[],[i_0_3239,i_0_633,i_0_2893,i_0_10]) ).
cnf(i_0_4515,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_4517,plain,
sum(additive_inverse(multiply(X1,additive_identity)),multiply(X2,additive_identity),multiply(X3,additive_identity)),
inference(scs_inference,[],[i_0_3239,i_0_3247,i_0_2873,i_0_10]) ).
cnf(i_0_4518,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_4629,plain,
~ product(a,additive_inverse(additive_identity),multiply(X1,additive_identity)),
inference(scs_inference,[],[i_0_3244,i_0_2030,i_0_14,i_0_12,i_0_8]) ).
cnf(i_0_4630,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_4631,plain,
sum(multiply(X1,additive_identity),multiply(X2,additive_identity),additive_inverse(additive_identity)),
inference(rename_variables,[],[i_0_3244]) ).
cnf(i_0_4632,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_4633,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_4745,plain,
sum(additive_inverse(additive_inverse(additive_identity)),multiply(X1,additive_identity),additive_inverse(additive_identity)),
inference(scs_inference,[],[i_0_3247,i_0_14,i_0_15,i_0_10]) ).
cnf(i_0_4746,plain,
sum(additive_identity,X1,X1),
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_4747,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_4748,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X4,X6,X1)
| ~ sum(X6,X2,X5) ),
inference(rename_variables,[],[i_0_10]) ).
cnf(i_0_4749,plain,
( product(X1,additive_identity,multiply(X2,additive_identity))
| ~ product(X1,additive_inverse(X3),additive_inverse(additive_identity))
| ~ product(X1,X3,additive_inverse(additive_identity)) ),
inference(scs_inference,[],[i_0_3247,i_0_14,i_0_4747,i_0_15,i_0_10,i_0_8]) ).
cnf(i_0_4973,plain,
( ~ product(a,additive_inverse(X1),additive_inverse(additive_inverse(additive_identity)))
| ~ product(a,X1,additive_inverse(additive_identity)) ),
inference(scs_inference,[],[i_0_3379,i_0_2030,i_0_14,i_0_8]) ).
cnf(i_0_4974,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_5310,plain,
( product(X1,additive_identity,multiply(X2,additive_identity))
| ~ product(X1,additive_inverse(additive_identity),multiply(X3,additive_identity)) ),
inference(scs_inference,[],[i_0_3941,i_0_14,i_0_12,i_0_8]) ).
cnf(i_0_5311,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_5312,plain,
sum(multiply(X1,additive_identity),multiply(X2,additive_identity),multiply(X3,additive_identity)),
inference(rename_variables,[],[i_0_3941]) ).
cnf(i_0_5313,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_5314,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_5315,plain,
( product(X1,multiply(X2,additive_identity),multiply(X2,additive_identity))
| ~ product(X1,multiply(X3,additive_identity),multiply(X3,additive_identity))
| ~ product(X1,multiply(X4,additive_identity),multiply(X4,additive_identity)) ),
inference(scs_inference,[],[i_0_3941,i_0_8]) ).
cnf(i_0_5426,plain,
sum(additive_inverse(additive_identity),X1,X1),
inference(scs_inference,[],[i_0_3480,i_0_3376,i_0_15,i_0_11]) ).
cnf(i_0_5427,plain,
sum(multiply(X1,additive_identity),X2,X2),
inference(rename_variables,[],[i_0_3376]) ).
cnf(i_0_5428,plain,
( ~ sum(X1,X2,X3)
| sum(X4,X5,X3)
| ~ sum(X1,X6,X4)
| ~ sum(X6,X5,X2) ),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_5430,plain,
( product(X1,additive_identity,multiply(X2,additive_identity))
| ~ product(X1,additive_inverse(X3),additive_inverse(multiply(X4,additive_identity)))
| ~ product(X1,X3,additive_inverse(additive_identity)) ),
inference(scs_inference,[],[i_0_4514,i_0_14,i_0_8]) ).
cnf(i_0_5541,plain,
( product(X1,additive_identity,multiply(X2,additive_identity))
| ~ product(X1,additive_inverse(additive_identity),additive_inverse(multiply(X3,additive_identity))) ),
inference(scs_inference,[],[i_0_4517,i_0_14,i_0_12,i_0_8]) ).
cnf(i_0_5542,plain,
sum(additive_inverse(X1),X1,additive_identity),
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_5543,plain,
sum(additive_inverse(multiply(X1,additive_identity)),multiply(X2,additive_identity),multiply(X3,additive_identity)),
inference(rename_variables,[],[i_0_4517]) ).
cnf(i_0_5544,plain,
product(X1,X2,multiply(X1,X2)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_5545,plain,
( ~ sum(X1,X2,X3)
| ~ sum(X4,X5,X6)
| product(X7,X3,X6)
| ~ product(X7,X1,X4)
| ~ product(X7,X2,X5) ),
inference(rename_variables,[],[i_0_8]) ).
cnf(i_0_5670,plain,
$false,
inference(scs_inference,[],[i_0_2888,i_0_2040,i_0_3244,i_0_12,i_0_8]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : RNG001-3 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n003.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 01:44:41 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 49.46/25.67 % Version : CSE_E---1.7
% 49.46/25.67 % Problem : theBenchmark.p
% 49.46/25.67 % SZS status Unsatisfiable for theBenchmark.p
% 49.46/25.67 % SZS output start CNFRefutation
% See solution above
% 50.02/25.93 % Total time : 25.325s
%------------------------------------------------------------------------------