%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT020-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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 : Tue Sep 29 11:47:41 AM UTC 2026
% Result : Unsatisfiable 242.81s 38.19s
% Output : Refutation 266.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 99
% Number of leaves : 10
% Syntax : Number of formulae : 700 ( 700 unt; 0 def)
% Number of atoms : 700 ( 699 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 2142 (2142 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/LAT004-0.ax',idempotence_of_meet) ).
fof(f2,axiom,
! [X0] : join(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/LAT004-0.ax',idempotence_of_join) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT004-0.ax',commutativity_of_meet) ).
fof(f4,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT004-0.ax',commutativity_of_join) ).
fof(f5,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT004-0.ax',associativity_of_meet) ).
fof(f6,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT004-0.ax',associativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : join(meet(X0,join(X1,X2)),meet(X0,X1)) = meet(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT004-0.ax',quasi_lattice1) ).
fof(f8,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,join(X1,X2)),meet(X0,X1)),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
! [X2,X0,X1] : meet(join(X0,meet(X1,X2)),join(X0,X1)) = join(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT004-0.ax',quasi_lattice2) ).
fof(f10,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,meet(X1,X2)),join(X0,X1)),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X2,X0,X1] : join(meet(join(meet(X0,X1),X2),X1),meet(X2,X0)) = meet(join(meet(join(X0,X1),X2),X1),join(X2,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',self_dual_distributivity) ).
fof(f12,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f13,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(superposition,[],[f5,f1]) ).
fof(f15,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f5,f3]) ).
fof(f20,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,meet(X0,X1))),
inference(superposition,[],[f1,f5]) ).
fof(f22,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f3,f5]) ).
fof(f27,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,meet(X0,X1)),
inference(superposition,[],[f13,f3]) ).
fof(f42,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,meet(X1,X2))),
inference(superposition,[],[f27,f5]) ).
fof(f45,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(meet(X0,X1),X2)),
inference(superposition,[],[f5,f27]) ).
fof(f47,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X1,meet(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f45,f5]) ).
fof(f48,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(superposition,[],[f6,f2]) ).
fof(f50,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f6,f4]) ).
fof(f57,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f4,f6]) ).
fof(f62,plain,
! [X0,X1] : join(X0,X1) = join(X1,join(X0,X1)),
inference(superposition,[],[f48,f4]) ).
fof(f74,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(X2,join(X0,X1)),meet(X2,X1)),
inference(superposition,[],[f8,f4]) ).
fof(f78,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),meet(join(X0,X1),X0)),
inference(superposition,[],[f8,f1]) ).
fof(f82,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = join(meet(X0,join(X0,X1)),X0),
inference(superposition,[],[f8,f1]) ).
fof(f84,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X1,join(X0,X2)),meet(X0,X1)),
inference(superposition,[],[f8,f3]) ).
fof(f85,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = join(meet(X0,join(meet(X0,X1),X2)),meet(X0,X1)),
inference(superposition,[],[f8,f13]) ).
fof(f91,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),join(meet(X0,X1),X3)) = join(meet(X0,join(X1,X2)),X3),
inference(superposition,[],[f6,f8]) ).
fof(f93,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,X1),meet(X0,join(X1,X2))),
inference(superposition,[],[f4,f8]) ).
fof(f94,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),X3) = join(meet(X0,X1),join(X3,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f91,f57]) ).
fof(f97,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X0,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f85,f4]) ).
fof(f98,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X0,X1),meet(X1,join(X0,X2))),
inference(forward_demodulation,[],[f84,f4]) ).
fof(f100,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = join(X0,meet(X0,join(X0,X1))),
inference(forward_demodulation,[],[f82,f4]) ).
fof(f104,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,meet(join(X0,X1),X0))),
inference(forward_demodulation,[],[f78,f6]) ).
fof(f106,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(X2,X1),meet(X2,join(X0,X1))),
inference(forward_demodulation,[],[f74,f4]) ).
fof(f110,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,meet(X0,join(X0,X1)))),
inference(forward_demodulation,[],[f104,f3]) ).
fof(f116,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,join(X1,X2))),
inference(superposition,[],[f62,f6]) ).
fof(f121,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(join(X0,X1),X2)),
inference(superposition,[],[f6,f62]) ).
fof(f123,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X0,join(X1,X2))),
inference(forward_demodulation,[],[f121,f6]) ).
fof(f138,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f5,f15]) ).
fof(f141,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X1,X0)),
inference(superposition,[],[f3,f15]) ).
fof(f236,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(meet(X0,X1),meet(X2,X0)),
inference(superposition,[],[f22,f13]) ).
fof(f241,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X0,meet(X1,X2))) = meet(X2,meet(X3,meet(X1,X0))),
inference(superposition,[],[f22,f15]) ).
fof(f272,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X0,X1)),
inference(superposition,[],[f27,f22]) ).
fof(f275,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X2,X0),X1),
inference(superposition,[],[f3,f22]) ).
fof(f284,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,X0)),
inference(superposition,[],[f13,f22]) ).
fof(f332,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X0,meet(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f236,f5]) ).
fof(f501,plain,
! [X2,X3,X0,X1] : join(join(X0,join(X1,X2)),X3) = join(X2,join(join(X0,X1),X3)),
inference(superposition,[],[f50,f6]) ).
fof(f509,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(superposition,[],[f6,f50]) ).
fof(f512,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X1,X0)),
inference(superposition,[],[f4,f50]) ).
fof(f528,plain,
! [X2,X3,X0,X1] : join(join(X0,join(X1,X2)),X3) = join(X2,join(X0,join(X1,X3))),
inference(forward_demodulation,[],[f501,f6]) ).
fof(f536,plain,
! [X2,X3,X0,X1] : join(X0,join(join(X1,X2),X3)) = join(X2,join(X0,join(X1,X3))),
inference(forward_demodulation,[],[f528,f6]) ).
fof(f541,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,join(X2,X3))) = join(X2,join(X0,join(X1,X3))),
inference(forward_demodulation,[],[f536,f6]) ).
fof(f607,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = meet(join(X2,meet(X0,X1)),join(X2,X1)),
inference(superposition,[],[f10,f27]) ).
fof(f614,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),join(meet(X0,X1),X0)),
inference(superposition,[],[f10,f2]) ).
fof(f616,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(meet(X0,X1),X2),join(X2,X0)),
inference(superposition,[],[f10,f4]) ).
fof(f620,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = meet(join(X0,meet(X0,X1)),X0),
inference(superposition,[],[f10,f2]) ).
fof(f622,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X1,meet(X0,X2)),join(X0,X1)),
inference(superposition,[],[f10,f4]) ).
fof(f623,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,meet(join(X0,X1),X2)),join(X0,X1)),
inference(superposition,[],[f10,f48]) ).
fof(f627,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),meet(X2,X3)) = meet(join(join(X0,X1),meet(X2,X3)),join(X0,join(X1,X2))),
inference(superposition,[],[f10,f6]) ).
fof(f640,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X1,X2))) = meet(join(X0,X1),meet(X3,join(X0,meet(X1,X2)))),
inference(superposition,[],[f22,f10]) ).
fof(f641,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,X1),join(X0,meet(X1,X2))),
inference(superposition,[],[f27,f10]) ).
fof(f650,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),meet(X2,X3)) = meet(join(X0,join(X1,X2)),join(join(X0,X1),meet(X2,X3))),
inference(forward_demodulation,[],[f627,f3]) ).
fof(f654,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X0,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f623,f3]) ).
fof(f655,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f622,f3]) ).
fof(f657,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = meet(X0,join(X0,meet(X0,X1))),
inference(forward_demodulation,[],[f620,f3]) ).
fof(f661,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(X2,X0),join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f616,f3]) ).
fof(f663,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(meet(X0,X1),X0))),
inference(forward_demodulation,[],[f614,f5]) ).
fof(f668,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = meet(join(X2,X1),join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f607,f3]) ).
fof(f676,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,meet(X2,X3))) = meet(join(X0,join(X1,X2)),join(X0,join(X1,meet(X2,X3)))),
inference(forward_demodulation,[],[f650,f6]) ).
fof(f682,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X0,meet(X0,X1)))),
inference(forward_demodulation,[],[f663,f4]) ).
fof(f688,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(join(X0,X1),join(X2,X0)),
inference(superposition,[],[f57,f48]) ).
fof(f693,plain,
! [X2,X3,X0,X1] : join(X3,join(X0,join(X1,X2))) = join(X2,join(X3,join(X1,X0))),
inference(superposition,[],[f57,f50]) ).
fof(f694,plain,
! [X2,X3,X0,X1] : join(X3,join(X0,join(X1,X2))) = join(X2,join(X3,join(X0,X1))),
inference(superposition,[],[f57,f6]) ).
fof(f729,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X2,X0),X1),
inference(superposition,[],[f4,f57]) ).
fof(f739,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,X0)),
inference(superposition,[],[f48,f57]) ).
fof(f748,plain,
! [X2,X3,X0,X1] : join(X2,meet(join(X0,X1),X3)) = meet(join(X2,meet(join(X0,X1),X3)),join(X0,join(X1,X2))),
inference(superposition,[],[f10,f57]) ).
fof(f753,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,join(X2,X3))) = join(X3,join(X2,join(X0,X1))),
inference(superposition,[],[f50,f57]) ).
fof(f758,plain,
! [X2,X3,X0,X1] : join(X2,meet(join(X0,X1),X3)) = meet(join(X0,join(X1,X2)),join(X2,meet(join(X0,X1),X3))),
inference(forward_demodulation,[],[f748,f3]) ).
fof(f791,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X0,join(X1,join(X2,X0))),
inference(forward_demodulation,[],[f688,f6]) ).
fof(f1035,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X2,X1)),
inference(superposition,[],[f22,f138]) ).
fof(f1039,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X0,X2),X1),
inference(superposition,[],[f3,f138]) ).
fof(f1044,plain,
! [X2,X3,X0,X1] : meet(meet(X0,meet(X1,X2)),X3) = meet(meet(X0,X2),meet(X1,X3)),
inference(superposition,[],[f15,f138]) ).
fof(f1061,plain,
! [X2,X3,X0,X1] : meet(meet(X0,meet(X1,X2)),X3) = meet(X0,meet(X2,meet(X1,X3))),
inference(forward_demodulation,[],[f1044,f5]) ).
fof(f1106,plain,
! [X2,X3,X0,X1] : meet(X0,meet(meet(X1,X2),X3)) = meet(X0,meet(X2,meet(X1,X3))),
inference(forward_demodulation,[],[f1061,f5]) ).
fof(f1115,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,meet(X2,X3))) = meet(X0,meet(X2,meet(X1,X3))),
inference(forward_demodulation,[],[f1106,f5]) ).
fof(f1566,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(superposition,[],[f57,f509]) ).
fof(f1570,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X2),X1),
inference(superposition,[],[f4,f509]) ).
fof(f1575,plain,
! [X2,X3,X0,X1] : join(join(X0,join(X1,X2)),X3) = join(join(X0,X2),join(X1,X3)),
inference(superposition,[],[f50,f509]) ).
fof(f1592,plain,
! [X2,X3,X0,X1] : join(join(X0,join(X1,X2)),X3) = join(X0,join(X2,join(X1,X3))),
inference(forward_demodulation,[],[f1575,f6]) ).
fof(f1637,plain,
! [X2,X3,X0,X1] : join(X0,join(join(X1,X2),X3)) = join(X0,join(X2,join(X1,X3))),
inference(forward_demodulation,[],[f1592,f6]) ).
fof(f1646,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,join(X2,X3))) = join(X0,join(X2,join(X1,X3))),
inference(forward_demodulation,[],[f1637,f6]) ).
fof(f1841,plain,
! [X0,X1] : meet(join(meet(join(X0,X0),X1),X0),join(X1,X0)) = join(meet(join(X0,X1),X0),meet(X1,X0)),
inference(superposition,[],[f11,f1]) ).
fof(f1843,plain,
! [X2,X0,X1] : meet(join(meet(join(X1,X0),X2),X0),join(X2,X1)) = join(meet(join(meet(X0,X1),X2),X0),meet(X2,X1)),
inference(superposition,[],[f11,f3]) ).
fof(f1863,plain,
! [X2,X0,X1] : meet(join(meet(join(X1,X2),X0),X2),join(X0,X1)) = join(meet(join(X0,meet(X1,X2)),X2),meet(X0,X1)),
inference(superposition,[],[f11,f4]) ).
fof(f1883,plain,
! [X0,X1] : meet(join(meet(join(X0,X1),X0),X1),join(X0,X0)) = join(meet(join(meet(X0,X1),X0),X1),X0),
inference(superposition,[],[f11,f1]) ).
fof(f1885,plain,
! [X2,X0,X1] : meet(join(meet(join(X0,X2),X1),X2),join(X1,X0)) = join(meet(join(meet(X0,X2),X1),X2),meet(X0,X1)),
inference(superposition,[],[f11,f3]) ).
fof(f1905,plain,
! [X2,X0,X1] : meet(join(meet(join(X0,X1),X2),X1),join(X2,X0)) = join(meet(X2,X0),meet(join(meet(X0,X1),X2),X1)),
inference(superposition,[],[f4,f11]) ).
fof(f1936,plain,
! [X2,X0,X1] : meet(join(meet(join(X0,X1),X2),X1),join(X2,X0)) = join(meet(X2,X0),meet(X1,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f1905,f3]) ).
fof(f1956,plain,
! [X2,X0,X1] : meet(join(meet(join(X0,X2),X1),X2),join(X1,X0)) = join(meet(X0,X1),meet(join(meet(X0,X2),X1),X2)),
inference(forward_demodulation,[],[f1885,f4]) ).
fof(f1958,plain,
! [X0,X1] : meet(join(meet(join(X0,X1),X0),X1),join(X0,X0)) = join(X0,meet(join(meet(X0,X1),X0),X1)),
inference(forward_demodulation,[],[f1883,f4]) ).
fof(f1978,plain,
! [X2,X0,X1] : meet(join(meet(join(X1,X2),X0),X2),join(X0,X1)) = join(meet(X0,X1),meet(join(X0,meet(X1,X2)),X2)),
inference(forward_demodulation,[],[f1863,f4]) ).
fof(f1998,plain,
! [X2,X0,X1] : meet(join(meet(join(X1,X0),X2),X0),join(X2,X1)) = join(meet(X2,X1),meet(join(meet(X0,X1),X2),X0)),
inference(forward_demodulation,[],[f1843,f4]) ).
fof(f2000,plain,
! [X0,X1] : meet(join(meet(join(X0,X0),X1),X0),join(X1,X0)) = join(meet(X1,X0),meet(join(X0,X1),X0)),
inference(forward_demodulation,[],[f1841,f4]) ).
fof(f2016,plain,
! [X2,X0,X1] : meet(join(X2,X0),join(meet(join(X0,X1),X2),X1)) = join(meet(X2,X0),meet(X1,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f1936,f3]) ).
fof(f2036,plain,
! [X2,X0,X1] : meet(join(meet(join(X0,X2),X1),X2),join(X1,X0)) = join(meet(X0,X1),meet(X2,join(meet(X0,X2),X1))),
inference(forward_demodulation,[],[f1956,f3]) ).
fof(f2038,plain,
! [X0,X1] : meet(join(meet(join(X0,X1),X0),X1),join(X0,X0)) = join(X0,meet(X1,join(meet(X0,X1),X0))),
inference(forward_demodulation,[],[f1958,f3]) ).
fof(f2058,plain,
! [X2,X0,X1] : meet(join(meet(join(X1,X2),X0),X2),join(X0,X1)) = join(meet(X0,X1),meet(X2,join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f1978,f3]) ).
fof(f2078,plain,
! [X2,X0,X1] : meet(join(meet(join(X1,X0),X2),X0),join(X2,X1)) = join(meet(X2,X1),meet(X0,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f1998,f3]) ).
fof(f2080,plain,
! [X0,X1] : meet(join(meet(join(X0,X0),X1),X0),join(X1,X0)) = join(meet(X1,X0),meet(X0,join(X0,X1))),
inference(forward_demodulation,[],[f2000,f3]) ).
fof(f2095,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X1,join(meet(X0,X1),X2))) = meet(join(X2,X0),join(X1,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f2016,f4]) ).
fof(f2115,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(meet(X0,X2),X1))) = meet(join(X1,X0),join(meet(join(X0,X2),X1),X2)),
inference(forward_demodulation,[],[f2036,f3]) ).
fof(f2117,plain,
! [X0,X1] : meet(join(meet(join(X0,X1),X0),X1),join(X0,X0)) = join(X0,meet(X1,join(X0,meet(X0,X1)))),
inference(forward_demodulation,[],[f2038,f4]) ).
fof(f2137,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(meet(join(X1,X2),X0),X2)) = join(meet(X0,X1),meet(X2,join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f2058,f3]) ).
fof(f2157,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(meet(join(X1,X0),X2),X0)) = join(meet(X2,X1),meet(X0,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f2078,f3]) ).
fof(f2159,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,join(X0,X1))) = meet(join(X1,X0),join(meet(join(X0,X0),X1),X0)),
inference(forward_demodulation,[],[f2080,f3]) ).
fof(f2185,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(meet(X0,X2),X1))) = meet(join(X1,X0),join(X2,meet(join(X0,X2),X1))),
inference(forward_demodulation,[],[f2115,f4]) ).
fof(f2187,plain,
! [X0,X1] : join(X0,meet(X1,join(X0,meet(X0,X1)))) = meet(join(X0,X0),join(meet(join(X0,X1),X0),X1)),
inference(forward_demodulation,[],[f2117,f3]) ).
fof(f2202,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X0,meet(X1,X2)))) = meet(join(X0,X1),join(X2,meet(join(X1,X2),X0))),
inference(forward_demodulation,[],[f2137,f4]) ).
fof(f2222,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(X0,join(meet(X0,X1),X2))) = meet(join(X2,X1),join(X0,meet(join(X1,X0),X2))),
inference(forward_demodulation,[],[f2157,f4]) ).
fof(f2224,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,join(X0,X1))) = meet(join(X1,X0),join(X0,meet(join(X0,X0),X1))),
inference(forward_demodulation,[],[f2159,f4]) ).
fof(f2241,plain,
! [X0,X1] : join(X0,meet(X1,join(X0,meet(X0,X1)))) = meet(join(X0,X0),join(X1,meet(join(X0,X1),X0))),
inference(forward_demodulation,[],[f2187,f4]) ).
fof(f2268,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,join(X0,X1))) = meet(join(X1,X0),join(X0,meet(X0,X1))),
inference(forward_demodulation,[],[f2224,f2]) ).
fof(f2278,plain,
! [X0,X1] : join(X0,meet(X1,join(X0,meet(X0,X1)))) = meet(join(X0,X0),join(X1,meet(X0,join(X0,X1)))),
inference(forward_demodulation,[],[f2241,f3]) ).
fof(f2298,plain,
! [X0,X1] : join(X0,meet(X1,join(X0,meet(X0,X1)))) = meet(X0,join(X1,meet(X0,join(X0,X1)))),
inference(forward_demodulation,[],[f2278,f2]) ).
fof(f2340,plain,
! [X2,X3,X0,X1] : join(join(X0,join(X1,X2)),X3) = join(join(X0,X2),join(X3,X1)),
inference(superposition,[],[f729,f509]) ).
fof(f2371,plain,
! [X2,X3,X0,X1] : join(join(X2,X0),meet(X1,X3)) = meet(join(join(X2,X0),meet(X1,X3)),join(X0,join(X1,X2))),
inference(superposition,[],[f10,f729]) ).
fof(f2419,plain,
! [X2,X3,X0,X1] : join(join(X2,X0),meet(X1,X3)) = meet(join(X0,join(X1,X2)),join(join(X2,X0),meet(X1,X3))),
inference(forward_demodulation,[],[f2371,f3]) ).
fof(f2441,plain,
! [X2,X3,X0,X1] : join(join(X0,join(X1,X2)),X3) = join(X0,join(X2,join(X3,X1))),
inference(forward_demodulation,[],[f2340,f6]) ).
fof(f2464,plain,
! [X2,X3,X0,X1] : join(X2,join(X0,meet(X1,X3))) = meet(join(X0,join(X1,X2)),join(X2,join(X0,meet(X1,X3)))),
inference(forward_demodulation,[],[f2419,f6]) ).
fof(f2482,plain,
! [X2,X3,X0,X1] : join(X0,join(join(X1,X2),X3)) = join(X0,join(X2,join(X3,X1))),
inference(forward_demodulation,[],[f2441,f6]) ).
fof(f2505,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,join(X2,X3))) = join(X0,join(X2,join(X3,X1))),
inference(forward_demodulation,[],[f2482,f6]) ).
fof(f2618,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X2,X1),X0),
inference(superposition,[],[f3,f1035]) ).
fof(f3070,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X2,X1),X0),
inference(superposition,[],[f4,f1566]) ).
fof(f4167,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = join(X1,meet(X1,join(X0,X1))),
inference(superposition,[],[f100,f62]) ).
fof(f4201,plain,
! [X2,X0,X1] : join(X0,join(meet(X0,join(X0,X1)),X2)) = join(X2,meet(X0,join(X0,X1))),
inference(superposition,[],[f57,f100]) ).
fof(f4211,plain,
! [X2,X0,X1] : join(meet(X0,join(X0,X1)),X2) = join(X0,join(X2,meet(X0,join(X0,X1)))),
inference(superposition,[],[f1570,f100]) ).
fof(f4285,plain,
! [X0,X1] : join(X0,X1) = join(X1,join(X0,meet(X1,join(X0,X1)))),
inference(superposition,[],[f110,f4]) ).
fof(f4332,plain,
! [X0,X1] : join(X0,X1) = join(X1,join(X0,meet(X0,join(X0,X1)))),
inference(superposition,[],[f509,f110]) ).
fof(f4346,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(join(X1,meet(X0,join(X0,X1))),join(X0,X2)),
inference(superposition,[],[f512,f110]) ).
fof(f4348,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(join(X1,meet(X0,join(X0,X1))),join(X2,X0)),
inference(superposition,[],[f729,f110]) ).
fof(f4365,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(meet(X0,join(X0,X1)),join(X2,X0))),
inference(forward_demodulation,[],[f4348,f6]) ).
fof(f4367,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X1,join(meet(X0,join(X0,X1)),join(X0,X2))),
inference(forward_demodulation,[],[f4346,f6]) ).
fof(f4376,plain,
! [X0,X1] : join(X0,X1) = join(X1,meet(X0,join(X0,X1))),
inference(forward_demodulation,[],[f4332,f100]) ).
fof(f4425,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,join(meet(X0,join(X0,X1)),X2))),
inference(forward_demodulation,[],[f4365,f2505]) ).
fof(f4427,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X1,join(X0,join(meet(X0,join(X0,X1)),X2))),
inference(forward_demodulation,[],[f4367,f1646]) ).
fof(f4457,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X2,meet(X0,join(X0,X1)))),
inference(forward_demodulation,[],[f4425,f4201]) ).
fof(f4459,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X1,join(X2,meet(X0,join(X0,X1)))),
inference(forward_demodulation,[],[f4427,f4201]) ).
fof(f4480,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X2,meet(X0,join(X0,X1)))),
inference(forward_demodulation,[],[f4457,f6]) ).
fof(f4534,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X0,meet(X1,join(meet(X0,X1),X2)))),
inference(superposition,[],[f4376,f5]) ).
fof(f4542,plain,
! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X1,X0)),
inference(superposition,[],[f10,f4376]) ).
fof(f4866,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f1035,f4542]) ).
fof(f4869,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(X2,meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f2618,f4542]) ).
fof(f4870,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(X2,join(X1,X0)),
inference(forward_demodulation,[],[f4869,f4542]) ).
fof(f4872,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,join(X0,X1)),
inference(forward_demodulation,[],[f4866,f4542]) ).
fof(f5299,plain,
! [X2,X3,X0,X1] : meet(join(X0,X1),join(X2,X3)) = meet(join(X1,X0),join(X3,X2)),
inference(superposition,[],[f4870,f4870]) ).
fof(f5326,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X0,join(X1,X2))) = meet(X3,meet(X0,join(X2,X1))),
inference(superposition,[],[f1035,f4870]) ).
fof(f5343,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(join(X1,X0),X2),
inference(superposition,[],[f3,f4870]) ).
fof(f5370,plain,
! [X2,X3,X0,X1] : meet(join(X0,X1),meet(X2,X3)) = meet(X3,meet(X2,join(X1,X0))),
inference(superposition,[],[f15,f4870]) ).
fof(f5371,plain,
! [X2,X3,X0,X1] : meet(join(X0,X1),meet(X2,X3)) = meet(X2,meet(X3,join(X1,X0))),
inference(superposition,[],[f5,f4870]) ).
fof(f5561,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(X3,join(X0,join(X2,X1))),
inference(superposition,[],[f4872,f3070]) ).
fof(f5565,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(X3,join(X2,join(X0,X1))),
inference(superposition,[],[f4872,f6]) ).
fof(f5664,plain,
! [X2,X3,X0,X1] : meet(join(X0,X1),join(X2,X3)) = meet(join(X3,X2),join(X1,X0)),
inference(superposition,[],[f4870,f4872]) ).
fof(f6299,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = meet(X1,join(X1,meet(X0,X1))),
inference(superposition,[],[f657,f27]) ).
fof(f6324,plain,
! [X2,X0,X1] : join(join(X2,X1),meet(X0,join(X1,X2))) = meet(join(X2,X1),join(join(X2,X1),meet(X0,join(X1,X2)))),
inference(superposition,[],[f657,f4870]) ).
fof(f6352,plain,
! [X2,X0,X1] : meet(X0,meet(join(X0,meet(X0,X1)),X2)) = meet(X2,join(X0,meet(X0,X1))),
inference(superposition,[],[f22,f657]) ).
fof(f6362,plain,
! [X2,X0,X1] : meet(join(X0,meet(X0,X1)),X2) = meet(X0,meet(X2,join(X0,meet(X0,X1)))),
inference(superposition,[],[f1039,f657]) ).
fof(f6402,plain,
! [X2,X0,X1] : join(X2,join(X1,meet(X0,join(X1,X2)))) = meet(join(X2,X1),join(X2,join(X1,meet(X0,join(X1,X2))))),
inference(forward_demodulation,[],[f6324,f6]) ).
fof(f6671,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,meet(X0,join(X1,meet(X0,X1)))),
inference(superposition,[],[f682,f3]) ).
fof(f6675,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,meet(meet(X0,X1),join(X1,meet(X0,X1)))),
inference(superposition,[],[f682,f27]) ).
fof(f6733,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,meet(X0,join(X0,meet(X0,X1)))),
inference(superposition,[],[f138,f682]) ).
fof(f6748,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(meet(X1,join(X0,meet(X0,X1))),meet(X0,X2)),
inference(superposition,[],[f141,f682]) ).
fof(f6774,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X1,meet(join(X0,meet(X0,X1)),meet(X0,X2))),
inference(forward_demodulation,[],[f6748,f5]) ).
fof(f6785,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(X0,meet(X0,X1))),
inference(forward_demodulation,[],[f6733,f657]) ).
fof(f6833,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,meet(X0,meet(X1,join(X1,meet(X0,X1))))),
inference(forward_demodulation,[],[f6675,f5]) ).
fof(f6845,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X1,meet(X0,meet(join(X0,meet(X0,X1)),X2))),
inference(forward_demodulation,[],[f6774,f1115]) ).
fof(f6876,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X1,meet(X0,X1)))),
inference(forward_demodulation,[],[f6833,f47]) ).
fof(f6885,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X1,meet(X2,join(X0,meet(X0,X1)))),
inference(forward_demodulation,[],[f6845,f6352]) ).
fof(f6907,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,meet(X0,X1))),
inference(forward_demodulation,[],[f6876,f6299]) ).
fof(f6994,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X1,X0)),
inference(superposition,[],[f8,f6785]) ).
fof(f7195,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X0,meet(join(X1,meet(X0,X1)),X2)),
inference(superposition,[],[f22,f6907]) ).
fof(f7199,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X0,meet(X2,join(X1,meet(X0,X1)))),
inference(superposition,[],[f138,f6907]) ).
fof(f7393,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = join(meet(X0,join(X2,X1)),meet(X0,join(X1,X2))),
inference(superposition,[],[f6994,f4870]) ).
fof(f7418,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,join(meet(X1,X0),meet(X0,X1))),
inference(superposition,[],[f1566,f6994]) ).
fof(f7421,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,join(meet(X1,X0),meet(X0,X1))),
inference(superposition,[],[f3070,f6994]) ).
fof(f7450,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f7421,f6994]) ).
fof(f7452,plain,
! [X2,X0,X1] : join(X2,meet(X1,X0)) = join(X2,meet(X0,X1)),
inference(forward_demodulation,[],[f7418,f6994]) ).
fof(f7937,plain,
! [X2,X3,X0,X1] : join(X3,meet(join(X0,X1),X2)) = join(meet(join(X1,X0),X2),X3),
inference(superposition,[],[f7450,f4870]) ).
fof(f7951,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,join(X1,X2))) = join(meet(X0,join(X2,X1)),X3),
inference(superposition,[],[f7450,f4870]) ).
fof(f7969,plain,
! [X2,X0,X1] : meet(join(meet(join(X2,X1),X0),X1),join(X0,X2)) = join(meet(join(X0,meet(X1,X2)),X1),meet(X0,X2)),
inference(superposition,[],[f11,f7450]) ).
fof(f7992,plain,
! [X2,X3,X0,X1] : join(X3,join(X0,meet(X1,X2))) = join(X3,join(X0,meet(X2,X1))),
inference(superposition,[],[f1566,f7450]) ).
fof(f8003,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X1,X2))) = meet(join(X0,meet(X2,X1)),X3),
inference(superposition,[],[f4870,f7450]) ).
fof(f8005,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X1,X2))) = meet(X3,join(X0,meet(X2,X1))),
inference(superposition,[],[f4872,f7450]) ).
fof(f8028,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X1,X0),X2),
inference(superposition,[],[f4,f7450]) ).
fof(f8069,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),join(X2,X3)) = join(X3,join(X2,meet(X1,X0))),
inference(superposition,[],[f50,f7450]) ).
fof(f8070,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),join(X2,X3)) = join(X2,join(X3,meet(X1,X0))),
inference(superposition,[],[f6,f7450]) ).
fof(f8112,plain,
! [X2,X0,X1] : meet(join(meet(join(X2,X1),X0),X1),join(X0,X2)) = join(meet(X0,X2),meet(X1,join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f7969,f7450]) ).
fof(f8177,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X1,join(X0,meet(X1,X2)))) = meet(join(X1,meet(join(X2,X1),X0)),join(X2,X0)),
inference(forward_demodulation,[],[f8112,f5299]) ).
fof(f8201,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X1,join(X0,meet(X1,X2)))) = meet(join(X2,X0),join(X1,meet(X0,join(X2,X1)))),
inference(forward_demodulation,[],[f8177,f8003]) ).
fof(f8252,plain,
! [X2,X3,X0,X1] : join(X3,meet(join(X0,X1),X2)) = join(X3,meet(join(X1,X0),X2)),
inference(superposition,[],[f7452,f4870]) ).
fof(f8257,plain,
! [X2,X3,X0,X1] : join(X3,meet(X2,meet(X0,X1))) = join(X3,meet(X0,meet(X1,X2))),
inference(superposition,[],[f7452,f5]) ).
fof(f8262,plain,
! [X2,X3,X0,X1] : join(X3,meet(X2,join(X1,X0))) = join(X3,meet(join(X0,X1),X2)),
inference(superposition,[],[f7452,f5343]) ).
fof(f8263,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,join(X1,X2))) = join(X3,meet(X0,join(X2,X1))),
inference(superposition,[],[f7452,f4870]) ).
fof(f8335,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,join(X1,X2)),meet(X1,X0)),
inference(superposition,[],[f8,f7452]) ).
fof(f8339,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X2,X3)) = join(meet(X3,X2),meet(X1,X0)),
inference(superposition,[],[f7450,f7452]) ).
fof(f8343,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,meet(X0,X1))),
inference(superposition,[],[f6907,f7452]) ).
fof(f8344,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(X0,meet(X1,X0))),
inference(superposition,[],[f6785,f7452]) ).
fof(f8414,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X1,X0),meet(X0,join(X2,X1))),
inference(forward_demodulation,[],[f8335,f7951]) ).
fof(f8600,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(meet(X0,join(X1,X2)),join(meet(X0,X1),X0)),
inference(superposition,[],[f10,f93]) ).
fof(f8655,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(meet(X0,X1),X0))),
inference(forward_demodulation,[],[f8600,f5]) ).
fof(f8703,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(X0,meet(X0,X1)))),
inference(forward_demodulation,[],[f8655,f5326]) ).
fof(f8726,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X0,meet(X0,X1)),join(X1,X2)),
inference(forward_demodulation,[],[f8703,f6362]) ).
fof(f8829,plain,
! [X2,X3,X0,X1] : join(meet(X2,join(X1,X0)),X3) = join(meet(join(X0,X1),X2),X3),
inference(superposition,[],[f8028,f5343]) ).
fof(f9153,plain,
! [X0,X1] : meet(join(X0,meet(X0,X1)),X0) = meet(join(X0,meet(X0,X1)),join(X0,join(X0,meet(X0,X1)))),
inference(superposition,[],[f8343,f657]) ).
fof(f9285,plain,
! [X0,X1] : meet(join(X0,meet(X0,X1)),X0) = meet(join(X0,meet(X0,X1)),join(X0,meet(X0,X1))),
inference(forward_demodulation,[],[f9153,f48]) ).
fof(f9339,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = meet(join(X0,meet(X0,X1)),X0),
inference(forward_demodulation,[],[f9285,f1]) ).
fof(f9377,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = meet(X0,join(X0,meet(X1,X0))),
inference(forward_demodulation,[],[f9339,f8003]) ).
fof(f9780,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(X1,X2),X3)) = meet(join(X2,X1),meet(X3,meet(X0,join(X1,X2)))),
inference(superposition,[],[f5343,f332]) ).
fof(f10163,plain,
! [X2,X3,X0,X1] : join(X3,join(X0,join(X1,X2))) = join(X1,join(X3,join(X2,join(X0,X1)))),
inference(superposition,[],[f509,f791]) ).
fof(f11659,plain,
! [X2,X0,X1] : meet(meet(X0,X1),join(X0,X2)) = join(meet(X0,X1),meet(meet(X0,X1),join(X0,X2))),
inference(superposition,[],[f98,f13]) ).
fof(f11747,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = join(meet(X0,X2),meet(join(X0,X1),X2)),
inference(superposition,[],[f98,f3]) ).
fof(f11875,plain,
! [X2,X0,X1] : meet(X0,meet(X1,join(X0,X2))) = join(meet(X0,X1),meet(X0,meet(X1,join(X0,X2)))),
inference(forward_demodulation,[],[f11659,f5]) ).
fof(f19898,plain,
! [X0,X1] : join(meet(X0,join(X1,X0)),X0) = join(meet(X0,join(X1,X0)),meet(X0,join(X1,X0))),
inference(superposition,[],[f739,f4167]) ).
fof(f19943,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = join(meet(X0,join(X1,X0)),X0),
inference(forward_demodulation,[],[f19898,f2]) ).
fof(f20031,plain,
! [X0,X1] : join(X0,meet(X0,join(X0,X1))) = meet(X0,join(X1,X0)),
inference(forward_demodulation,[],[f19943,f7951]) ).
fof(f20309,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(join(X0,meet(X1,X2)),X1),join(X0,meet(X1,X2))),
inference(superposition,[],[f106,f10]) ).
fof(f20329,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(meet(X0,join(X1,X2)),join(meet(X0,X2),X0)),
inference(superposition,[],[f10,f106]) ).
fof(f20359,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),X3) = join(meet(X0,X2),join(X3,meet(X0,join(X1,X2)))),
inference(superposition,[],[f1570,f106]) ).
fof(f20406,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(meet(X0,X2),X0))),
inference(forward_demodulation,[],[f20329,f5]) ).
fof(f20415,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(join(X0,meet(X1,X2)),meet(join(meet(X1,X2),X0),X1)),
inference(forward_demodulation,[],[f20309,f7937]) ).
fof(f20471,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(X0,meet(X0,X2)))),
inference(forward_demodulation,[],[f20406,f5326]) ).
fof(f20478,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(meet(X1,X2),meet(join(meet(X1,X2),X0),X1))),
inference(forward_demodulation,[],[f20415,f6]) ).
fof(f20507,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X0,meet(X0,X2)),join(X1,X2)),
inference(forward_demodulation,[],[f20471,f6362]) ).
fof(f20512,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(meet(X1,X2),meet(X1,join(meet(X1,X2),X0)))),
inference(forward_demodulation,[],[f20478,f7992]) ).
fof(f20534,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X1,join(meet(X1,X2),X0))),
inference(forward_demodulation,[],[f20512,f97]) ).
fof(f20667,plain,
! [X2,X0,X1] : meet(join(X0,meet(X1,X0)),X2) = meet(X0,meet(X2,join(X0,meet(X1,X0)))),
inference(superposition,[],[f1039,f6299]) ).
fof(f24657,plain,
! [X0,X1] : join(meet(X0,join(X0,X1)),X0) = join(meet(X0,join(X0,X1)),meet(X0,join(X1,X0))),
inference(superposition,[],[f739,f20031]) ).
fof(f24715,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = join(meet(X0,join(X0,X1)),X0),
inference(forward_demodulation,[],[f24657,f7393]) ).
fof(f24834,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = join(X0,meet(X0,join(X1,X0))),
inference(forward_demodulation,[],[f24715,f7951]) ).
fof(f25124,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(X0,X2),join(meet(X0,X1),X2)),
inference(superposition,[],[f655,f4]) ).
fof(f25154,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(join(X1,X0),X0),join(X0,meet(X1,X2))),
inference(superposition,[],[f93,f655]) ).
fof(f25158,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X1,X0),join(meet(X1,X2),X0)),
inference(superposition,[],[f4872,f655]) ).
fof(f25247,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X0,join(X0,X1)),join(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f25154,f8829]) ).
fof(f25341,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(meet(X1,X2),meet(join(X0,X1),X0))),
inference(forward_demodulation,[],[f25247,f8070]) ).
fof(f25400,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(meet(X1,X2),meet(X0,join(X0,X1)))),
inference(forward_demodulation,[],[f25341,f7992]) ).
fof(f25426,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X0,join(X0,X1)),meet(X1,X2)),
inference(forward_demodulation,[],[f25400,f4211]) ).
fof(f26598,plain,
! [X2,X0,X1] : join(join(X2,X1),meet(join(X2,X1),X0)) = meet(join(X2,X1),join(join(X2,X1),meet(X0,join(X1,X2)))),
inference(superposition,[],[f9377,f4872]) ).
fof(f26600,plain,
! [X0,X1] : meet(join(X1,meet(X1,X0)),join(join(X1,meet(X1,X0)),meet(X0,X1))) = join(join(X1,meet(X1,X0)),meet(join(X1,meet(X1,X0)),X0)),
inference(superposition,[],[f9377,f8343]) ).
fof(f26805,plain,
! [X0,X1] : meet(join(X1,meet(X1,X0)),join(join(X1,meet(X1,X0)),meet(X0,X1))) = join(X1,join(meet(X1,X0),meet(join(X1,meet(X1,X0)),X0))),
inference(forward_demodulation,[],[f26600,f6]) ).
fof(f26807,plain,
! [X2,X0,X1] : join(join(X2,X1),meet(join(X2,X1),X0)) = meet(join(X2,X1),join(X2,join(X1,meet(X0,join(X1,X2))))),
inference(forward_demodulation,[],[f26598,f6]) ).
fof(f26902,plain,
! [X0,X1] : meet(join(X1,meet(X1,X0)),join(join(X1,meet(X1,X0)),meet(X0,X1))) = join(X1,join(meet(X1,X0),meet(X0,join(X1,meet(X1,X0))))),
inference(forward_demodulation,[],[f26805,f7992]) ).
fof(f26904,plain,
! [X2,X0,X1] : join(join(X2,X1),meet(join(X2,X1),X0)) = join(X2,join(X1,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f26807,f6402]) ).
fof(f26976,plain,
! [X0,X1] : meet(join(X1,meet(X1,X0)),join(join(X1,meet(X1,X0)),meet(X0,X1))) = join(X1,meet(X0,join(X1,meet(X1,X0)))),
inference(forward_demodulation,[],[f26902,f98]) ).
fof(f26978,plain,
! [X2,X0,X1] : join(X2,join(X1,meet(join(X2,X1),X0))) = join(X2,join(X1,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f26904,f6]) ).
fof(f27033,plain,
! [X0,X1] : meet(join(X1,meet(X1,X0)),join(join(X1,meet(X1,X0)),meet(X0,X1))) = meet(X1,join(X0,meet(X1,join(X1,X0)))),
inference(forward_demodulation,[],[f26976,f2298]) ).
fof(f27078,plain,
! [X0,X1] : meet(X1,join(X1,X0)) = meet(join(X1,meet(X1,X0)),join(join(X1,meet(X1,X0)),meet(X0,X1))),
inference(forward_demodulation,[],[f27033,f4376]) ).
fof(f27117,plain,
! [X0,X1] : meet(X1,join(X1,X0)) = meet(join(X1,meet(X1,X0)),join(meet(X0,X1),join(X1,meet(X1,X0)))),
inference(forward_demodulation,[],[f27078,f4872]) ).
fof(f27146,plain,
! [X0,X1] : meet(X1,join(X1,X0)) = meet(join(X1,meet(X1,X0)),join(X1,join(meet(X1,X0),meet(X0,X1)))),
inference(forward_demodulation,[],[f27117,f5565]) ).
fof(f27165,plain,
! [X0,X1] : meet(X1,join(X1,X0)) = meet(join(X1,meet(X1,X0)),join(X1,meet(X1,X0))),
inference(forward_demodulation,[],[f27146,f6994]) ).
fof(f27183,plain,
! [X0,X1] : join(X1,meet(X1,X0)) = meet(X1,join(X1,X0)),
inference(forward_demodulation,[],[f27165,f1]) ).
fof(f27224,plain,
! [X2,X0,X1] : join(X1,meet(X0,meet(X1,X2))) = meet(X1,join(X1,meet(X0,X2))),
inference(superposition,[],[f27183,f138]) ).
fof(f27250,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = meet(X1,join(X1,join(X0,meet(X1,X0)))),
inference(superposition,[],[f27183,f8344]) ).
fof(f27251,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = meet(X0,join(X0,join(X1,meet(X0,X1)))),
inference(superposition,[],[f27183,f6907]) ).
fof(f27257,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,meet(X1,X2))) = meet(meet(X0,X2),join(meet(X0,X2),X1)),
inference(superposition,[],[f27183,f1039]) ).
fof(f27259,plain,
! [X2,X0,X1] : meet(meet(X1,X0),join(meet(X1,X0),X2)) = join(meet(X1,X0),meet(X0,meet(X1,X2))),
inference(superposition,[],[f27183,f15]) ).
fof(f27267,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(join(X2,X1),X0)) = join(join(X2,X1),meet(X0,join(X1,X2))),
inference(superposition,[],[f27183,f4870]) ).
fof(f27289,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = join(X0,meet(X1,X0)),
inference(superposition,[],[f7452,f27183]) ).
fof(f27308,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,meet(X0,join(X0,X1))),
inference(superposition,[],[f6785,f27183]) ).
fof(f27344,plain,
! [X2,X0,X1] : join(meet(X0,join(X0,X1)),X2) = join(X0,join(X2,meet(X0,X1))),
inference(superposition,[],[f1570,f27183]) ).
fof(f27365,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(join(X0,X1),X2)) = join(X1,join(X0,meet(join(X0,X1),X2))),
inference(superposition,[],[f50,f27183]) ).
fof(f27366,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(join(X0,X1),X2)) = join(X0,join(X1,meet(join(X0,X1),X2))),
inference(superposition,[],[f6,f27183]) ).
fof(f27367,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,join(X1,X2))) = join(X0,join(X1,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f27366,f6]) ).
fof(f27368,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,join(X1,X2))) = join(X1,join(X0,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f27365,f6]) ).
fof(f27437,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(join(X2,X1),X0)) = join(X2,join(X1,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f27267,f6]) ).
fof(f27445,plain,
! [X2,X0,X1] : meet(X1,meet(X0,join(meet(X1,X0),X2))) = join(meet(X1,X0),meet(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f27259,f5]) ).
fof(f27447,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,meet(X1,X2))) = meet(X0,meet(X2,join(meet(X0,X2),X1))),
inference(forward_demodulation,[],[f27257,f5]) ).
fof(f27453,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = meet(X0,join(X0,meet(X1,join(X1,X0)))),
inference(forward_demodulation,[],[f27251,f27289]) ).
fof(f27454,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = meet(X1,join(X1,meet(X0,join(X0,X1)))),
inference(forward_demodulation,[],[f27250,f27289]) ).
fof(f27514,plain,
! [X2,X0,X1] : join(X2,join(X1,meet(X0,join(X1,X2)))) = meet(join(X2,X1),join(X2,join(X1,X0))),
inference(forward_demodulation,[],[f27437,f6]) ).
fof(f27523,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = meet(X0,join(X1,X0)),
inference(forward_demodulation,[],[f27453,f4376]) ).
fof(f27524,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = meet(X1,join(X0,X1)),
inference(forward_demodulation,[],[f27454,f4376]) ).
fof(f27737,plain,
! [X0,X1] : meet(meet(X1,X0),join(meet(X1,X0),X0)) = join(meet(X1,X0),meet(meet(X1,X0),meet(X0,join(X0,X1)))),
inference(superposition,[],[f24834,f27289]) ).
fof(f27741,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(join(X0,X1),X2)) = join(X0,join(X1,meet(X2,join(X0,X1)))),
inference(superposition,[],[f6,f27289]) ).
fof(f27742,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,join(X1,X2))) = join(X0,join(X1,meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f27741,f6]) ).
fof(f27746,plain,
! [X0,X1] : meet(meet(X1,X0),join(meet(X1,X0),X0)) = meet(meet(X1,X0),join(meet(X1,X0),meet(X0,join(X0,X1)))),
inference(forward_demodulation,[],[f27737,f27183]) ).
fof(f27845,plain,
! [X0,X1] : meet(meet(X1,X0),join(meet(X1,X0),X0)) = meet(X1,meet(X0,join(meet(X1,X0),meet(X0,join(X0,X1))))),
inference(forward_demodulation,[],[f27746,f5]) ).
fof(f27911,plain,
! [X0,X1] : meet(meet(X1,X0),join(meet(X1,X0),X0)) = meet(X1,meet(X0,meet(join(X1,X0),join(X0,meet(X0,X1))))),
inference(forward_demodulation,[],[f27845,f2268]) ).
fof(f27958,plain,
! [X0,X1] : meet(meet(X1,X0),join(meet(X1,X0),X0)) = meet(X1,meet(join(X0,meet(X0,X1)),join(X1,X0))),
inference(forward_demodulation,[],[f27911,f6362]) ).
fof(f27995,plain,
! [X0,X1] : meet(meet(X1,X0),join(meet(X1,X0),X0)) = meet(X1,meet(join(X1,X0),join(X0,meet(X0,X1)))),
inference(forward_demodulation,[],[f27958,f1035]) ).
fof(f28020,plain,
! [X0,X1] : meet(join(X1,X0),meet(X0,X1)) = meet(meet(X1,X0),join(meet(X1,X0),X0)),
inference(forward_demodulation,[],[f27995,f6885]) ).
fof(f28035,plain,
! [X0,X1] : meet(join(X1,X0),meet(X0,X1)) = meet(X1,meet(X0,join(meet(X1,X0),X0))),
inference(forward_demodulation,[],[f28020,f5]) ).
fof(f28046,plain,
! [X0,X1] : meet(join(X1,X0),meet(X0,X1)) = meet(X1,meet(X0,join(X0,meet(X1,X0)))),
inference(forward_demodulation,[],[f28035,f5326]) ).
fof(f28056,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = meet(join(X1,X0),meet(X0,X1)),
inference(forward_demodulation,[],[f28046,f7199]) ).
fof(f28063,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = meet(X0,meet(X1,join(X0,X1))),
inference(forward_demodulation,[],[f28056,f5371]) ).
fof(f28069,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,join(X0,X1))),
inference(forward_demodulation,[],[f28063,f27]) ).
fof(f29172,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,X0)),X2) = join(X0,join(X2,meet(X0,X1))),
inference(superposition,[],[f1570,f27523]) ).
fof(f29675,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(join(X2,X0),X2),join(meet(X0,X1),X2)),
inference(superposition,[],[f106,f661]) ).
fof(f29710,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(X2,X0),meet(join(meet(X0,X1),X2),join(join(X2,X0),join(meet(X0,X1),X2)))),
inference(superposition,[],[f682,f661]) ).
fof(f29753,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(meet(X0,X1),X2),join(X2,X0)),
inference(forward_demodulation,[],[f29710,f28069]) ).
fof(f29775,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X2,join(X0,X2)),join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f29675,f8829]) ).
fof(f29897,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(X0,X2),join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f29753,f5664]) ).
fof(f29910,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,join(join(meet(X0,X1),X2),meet(X2,X0))),
inference(forward_demodulation,[],[f29775,f29172]) ).
fof(f30011,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,join(meet(X2,X0),join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f29910,f1566]) ).
fof(f30097,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X2,X0),join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f30011,f116]) ).
fof(f30141,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,join(meet(X0,X1),meet(X0,X2))),
inference(forward_demodulation,[],[f30097,f8069]) ).
fof(f31698,plain,
! [X2,X3,X0,X1] : meet(join(X0,join(X1,X2)),join(join(X2,join(X0,X1)),meet(X1,X3))) = join(meet(X1,X3),join(X2,join(X0,X1))),
inference(superposition,[],[f29897,f791]) ).
fof(f31801,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,X2)),meet(X1,X0)) = meet(join(X0,meet(X1,X0)),meet(X0,join(X1,X2))),
inference(superposition,[],[f29897,f98]) ).
fof(f31823,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(join(meet(X0,X1),X2),meet(join(X0,X2),X2)),
inference(superposition,[],[f8,f29897]) ).
fof(f31935,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X0,X1),join(X2,meet(join(X0,X2),X2))),
inference(forward_demodulation,[],[f31823,f6]) ).
fof(f31946,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,X2)),meet(X1,X0)) = meet(X0,meet(join(X1,X2),join(meet(X1,X0),X0))),
inference(forward_demodulation,[],[f31801,f5371]) ).
fof(f31985,plain,
! [X2,X3,X0,X1] : meet(join(X0,join(X1,X2)),join(join(X2,join(X0,X1)),meet(X1,X3))) = join(X1,join(X0,join(meet(X1,X3),X2))),
inference(forward_demodulation,[],[f31698,f753]) ).
fof(f32063,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X0,X1),join(X2,meet(X2,join(X0,X2)))),
inference(forward_demodulation,[],[f31935,f7992]) ).
fof(f32072,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,X2)),meet(X1,X0)) = meet(X0,meet(join(X1,X2),join(X0,meet(X1,X0)))),
inference(forward_demodulation,[],[f31946,f5326]) ).
fof(f32101,plain,
! [X2,X3,X0,X1] : meet(join(X0,join(X1,X2)),join(X2,join(join(X0,X1),meet(X1,X3)))) = join(X1,join(X0,join(meet(X1,X3),X2))),
inference(forward_demodulation,[],[f31985,f6]) ).
fof(f32156,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X0,X1),meet(X2,join(X0,X2))),
inference(forward_demodulation,[],[f32063,f4167]) ).
fof(f32162,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,X2)),meet(X1,X0)) = meet(join(X0,meet(X1,X0)),join(X1,X2)),
inference(forward_demodulation,[],[f32072,f20667]) ).
fof(f32181,plain,
! [X2,X3,X0,X1] : meet(join(X0,join(X1,X2)),join(X2,join(X0,join(X1,meet(X1,X3))))) = join(X1,join(X0,join(meet(X1,X3),X2))),
inference(forward_demodulation,[],[f32101,f6]) ).
fof(f32229,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,X2)),meet(X1,X0)) = meet(meet(X0,join(X0,X1)),join(X1,X2)),
inference(forward_demodulation,[],[f32162,f27289]) ).
fof(f32241,plain,
! [X2,X3,X0,X1] : join(X1,join(X0,join(meet(X1,X3),X2))) = meet(join(X0,join(X1,X2)),join(X2,join(X0,meet(X1,join(X1,X3))))),
inference(forward_demodulation,[],[f32181,f27183]) ).
fof(f32273,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,X2)),meet(X1,X0)) = meet(X0,meet(join(X0,X1),join(X1,X2))),
inference(forward_demodulation,[],[f32229,f5]) ).
fof(f32283,plain,
! [X2,X3,X0,X1] : join(X1,join(X0,join(meet(X1,X3),X2))) = join(X2,join(X0,meet(X1,join(X1,X3)))),
inference(forward_demodulation,[],[f32241,f2464]) ).
fof(f32307,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,join(X2,X1))) = meet(X0,meet(join(X0,X1),join(X1,X2))),
inference(forward_demodulation,[],[f32273,f7951]) ).
fof(f32320,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X0,X1),join(X1,X2))),
inference(forward_demodulation,[],[f32307,f8414]) ).
fof(f32464,plain,
! [X2,X0,X1] : join(join(X1,X2),meet(X0,join(X1,X2))) = join(meet(X0,X2),join(X1,X2)),
inference(superposition,[],[f30141,f106]) ).
fof(f32513,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,join(meet(X0,X2),meet(X0,X1))),
inference(superposition,[],[f1566,f30141]) ).
fof(f32655,plain,
! [X2,X0,X1] : join(join(X1,X2),meet(X0,join(X1,X2))) = join(X2,join(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f32464,f8069]) ).
fof(f32754,plain,
! [X2,X0,X1] : join(X1,join(X2,meet(X0,join(X1,X2)))) = join(X2,join(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f32655,f6]) ).
fof(f39245,plain,
! [X2,X3,X0,X1,X4] : meet(X4,meet(meet(X0,X1),join(X2,X3))) = meet(join(X3,X2),meet(X1,meet(X0,X4))),
inference(superposition,[],[f241,f4870]) ).
fof(f39548,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,meet(X1,meet(X2,X3)))) = meet(X3,join(meet(X0,meet(X2,X1)),X3)),
inference(superposition,[],[f27523,f241]) ).
fof(f39794,plain,
! [X2,X3,X0,X1,X4] : meet(X4,meet(X0,meet(X1,join(X2,X3)))) = meet(join(X3,X2),meet(X1,meet(X0,X4))),
inference(forward_demodulation,[],[f39245,f5]) ).
fof(f49650,plain,
! [X2,X3,X0,X1] : join(X2,join(X3,meet(X0,join(X0,X1)))) = join(X0,join(X2,join(X3,meet(X0,join(X0,X1))))),
inference(superposition,[],[f541,f100]) ).
fof(f49939,plain,
! [X2,X3,X0,X1,X4] : join(X0,join(meet(X1,X2),join(X3,X4))) = join(meet(X2,X1),join(X3,join(X0,X4))),
inference(superposition,[],[f8028,f541]) ).
fof(f51112,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X1,meet(X0,join(X0,X1))))) = join(meet(X0,X2),meet(X2,meet(X0,join(X1,meet(X0,join(X0,X1)))))),
inference(superposition,[],[f98,f2298]) ).
fof(f51221,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X1,meet(X0,join(X0,X1))))) = meet(X0,meet(X2,join(meet(X0,X2),join(X1,meet(X0,join(X0,X1)))))),
inference(forward_demodulation,[],[f51112,f27445]) ).
fof(f51419,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X1,meet(X0,join(X0,X1))))) = meet(X0,meet(X2,join(X0,join(X1,join(meet(X0,X1),meet(X0,X2)))))),
inference(forward_demodulation,[],[f51221,f32283]) ).
fof(f51595,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X1,meet(X0,join(X0,X1))))) = meet(X0,meet(X2,join(X0,join(meet(X0,X2),X1)))),
inference(forward_demodulation,[],[f51419,f32513]) ).
fof(f51750,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X0,X1))) = meet(X0,meet(X2,join(X0,join(meet(X0,X2),X1)))),
inference(forward_demodulation,[],[f51595,f4376]) ).
fof(f53681,plain,
! [X2,X3,X0,X1] : join(X3,join(meet(X0,X1),X2)) = join(meet(X0,X2),join(X3,join(meet(X0,X1),X2))),
inference(superposition,[],[f693,f30141]) ).
fof(f53900,plain,
! [X2,X3,X0,X1,X4] : join(X0,join(meet(X1,X2),join(X3,X4))) = join(meet(X2,X1),join(X4,join(X3,X0))),
inference(superposition,[],[f8028,f693]) ).
fof(f54147,plain,
! [X2,X3,X0,X1,X4] : meet(X4,join(X0,join(X1,join(X2,X3)))) = meet(X4,join(join(X0,join(X2,X1)),X3)),
inference(superposition,[],[f4872,f693]) ).
fof(f54174,plain,
! [X2,X3,X0,X1,X4] : meet(X4,join(X0,join(X1,join(X2,X3)))) = meet(X4,join(X0,join(join(X2,X1),X3))),
inference(forward_demodulation,[],[f54147,f6]) ).
fof(f54524,plain,
! [X2,X3,X0,X1] : join(X3,join(meet(X0,X1),X2)) = join(X2,join(meet(X2,X0),join(meet(X0,X1),X3))),
inference(forward_demodulation,[],[f53681,f53900]) ).
fof(f54620,plain,
! [X2,X3,X0,X1,X4] : meet(X4,join(X0,join(X1,join(X2,X3)))) = meet(X4,join(X0,join(X2,join(X1,X3)))),
inference(forward_demodulation,[],[f54174,f6]) ).
fof(f55726,plain,
! [X2,X3,X0,X1,X4] : join(X0,join(X1,join(X2,meet(X3,X4)))) = join(join(X0,join(X1,X2)),meet(X4,X3)),
inference(superposition,[],[f7450,f694]) ).
fof(f55958,plain,
! [X2,X3,X0,X1,X4] : join(X0,join(X1,join(X2,meet(X3,X4)))) = join(X0,join(join(X1,X2),meet(X4,X3))),
inference(forward_demodulation,[],[f55726,f6]) ).
fof(f56373,plain,
! [X2,X3,X0,X1,X4] : join(X0,join(X1,join(X2,meet(X3,X4)))) = join(X0,join(X1,join(X2,meet(X4,X3)))),
inference(forward_demodulation,[],[f55958,f6]) ).
fof(f64100,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(meet(X0,join(X1,X0)),join(X1,X2)),
inference(superposition,[],[f8726,f27523]) ).
fof(f64166,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(join(X3,meet(X3,X1)),join(X0,join(X1,X2))),
inference(superposition,[],[f8726,f791]) ).
fof(f64221,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),join(X0,meet(X0,X1))),
inference(superposition,[],[f4870,f8726]) ).
fof(f64240,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X1,X2),join(X0,meet(X0,X1))),
inference(superposition,[],[f3,f8726]) ).
fof(f64304,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X1,X2),meet(join(X0,meet(X0,X1)),join(join(X1,X2),meet(X0,join(X1,X2))))),
inference(superposition,[],[f6671,f8726]) ).
fof(f64324,plain,
! [X2,X0,X1] : join(join(X1,X2),meet(X0,join(X1,X2))) = meet(join(X1,X2),join(join(X0,meet(X0,X1)),join(X1,X2))),
inference(superposition,[],[f27524,f8726]) ).
fof(f64331,plain,
! [X2,X0,X1] : join(join(X1,X2),meet(X0,join(X1,X2))) = meet(join(X1,X2),join(X1,join(X2,join(X0,meet(X0,X1))))),
inference(forward_demodulation,[],[f64324,f5565]) ).
fof(f64350,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(join(X1,X2),meet(X0,join(X1,X2))),join(X0,meet(X0,X1))),
inference(forward_demodulation,[],[f64304,f20667]) ).
fof(f64411,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X1,X2),meet(X0,join(X0,X1))),
inference(forward_demodulation,[],[f64240,f27183]) ).
fof(f64429,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),meet(X0,join(X0,X1))),
inference(forward_demodulation,[],[f64221,f27183]) ).
fof(f64479,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(meet(X3,join(X3,X1)),join(X0,join(X1,X2))),
inference(forward_demodulation,[],[f64166,f27183]) ).
fof(f64521,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X0),join(X1,X2))),
inference(forward_demodulation,[],[f64100,f5]) ).
fof(f64603,plain,
! [X2,X0,X1] : join(join(X1,X2),meet(X0,join(X1,X2))) = meet(join(X1,X2),join(X1,join(X2,meet(X0,join(X0,X1))))),
inference(forward_demodulation,[],[f64331,f27183]) ).
fof(f64616,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(join(X1,X2),meet(X0,join(X1,X2))),meet(X0,join(X0,X1))),
inference(forward_demodulation,[],[f64350,f27183]) ).
fof(f64723,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(X3,meet(join(X3,X1),join(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f64479,f5]) ).
fof(f64837,plain,
! [X2,X0,X1] : meet(join(X1,X2),join(X2,join(X0,X1))) = join(join(X1,X2),meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f64603,f4459]) ).
fof(f64846,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X0,X1),join(meet(X0,join(X1,X2)),join(X1,X2)))),
inference(forward_demodulation,[],[f64616,f5371]) ).
fof(f64930,plain,
! [X2,X0,X1] : meet(join(X1,X2),join(X2,join(X0,X1))) = join(X1,join(X2,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f64837,f6]) ).
fof(f64938,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X0,X1),join(join(X1,X2),meet(X0,join(X1,X2))))),
inference(forward_demodulation,[],[f64846,f5326]) ).
fof(f64981,plain,
! [X2,X0,X1] : meet(join(X1,X2),join(X2,join(X0,X1))) = join(X2,join(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f64930,f32754]) ).
fof(f64987,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X0,X1),meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f64938,f7199]) ).
fof(f65011,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(X1,X0))),
inference(forward_demodulation,[],[f64987,f5371]) ).
fof(f65075,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(meet(X0,X1),X2)),X3) = join(meet(X0,X1),join(X3,meet(X0,join(meet(X0,X1),X2)))),
inference(superposition,[],[f94,f13]) ).
fof(f65963,plain,
! [X2,X0,X1] : meet(meet(X0,join(X0,X1)),X2) = join(meet(X0,X2),meet(meet(X0,join(X0,X1)),X2)),
inference(superposition,[],[f11747,f24834]) ).
fof(f66035,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X0,join(X0,X1)),join(X0,meet(X1,X2))),
inference(superposition,[],[f11747,f10]) ).
fof(f66039,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X0,join(X2,meet(X0,X1))),join(meet(X0,X1),X2)),
inference(superposition,[],[f11747,f29897]) ).
fof(f66290,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(join(meet(X0,X1),X2),meet(X0,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f66039,f7951]) ).
fof(f66293,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(join(X0,meet(X1,X2)),meet(X0,X1))),
inference(forward_demodulation,[],[f66035,f27344]) ).
fof(f66308,plain,
! [X2,X0,X1] : meet(X0,meet(join(X0,X1),X2)) = join(meet(X0,X2),meet(X0,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f65963,f5]) ).
fof(f66434,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X0,X1),join(X2,meet(X0,join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f66290,f6]) ).
fof(f66437,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(meet(X0,X1),join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f66293,f1566]) ).
fof(f66448,plain,
! [X2,X0,X1] : meet(X0,meet(join(X0,X1),X2)) = meet(X0,meet(X2,join(meet(X0,X2),join(X0,X1)))),
inference(forward_demodulation,[],[f66308,f27447]) ).
fof(f66550,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X0,join(meet(X0,X1),X2)),X2),
inference(forward_demodulation,[],[f66434,f65075]) ).
fof(f66552,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X0,X1),join(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f66437,f123]) ).
fof(f66557,plain,
! [X2,X0,X1] : meet(X0,meet(join(X0,X1),X2)) = meet(X0,meet(X2,join(X0,join(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f66448,f5565]) ).
fof(f66625,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X0,join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f66550,f7951]) ).
fof(f66626,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(meet(X1,X2),meet(X1,X0))),
inference(forward_demodulation,[],[f66552,f8070]) ).
fof(f66733,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(join(X0,meet(X0,X1)),join(X2,meet(X0,X1))),
inference(superposition,[],[f20507,f13]) ).
fof(f66810,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(meet(X0,join(X1,X0)),join(X2,X1)),
inference(superposition,[],[f20507,f27523]) ).
fof(f66952,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X1,X2),join(X0,meet(X0,X2))),
inference(superposition,[],[f3,f20507]) ).
fof(f66961,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X0,join(X1,X2))) = meet(join(X0,meet(X0,X2)),meet(join(X1,X2),X3)),
inference(superposition,[],[f22,f20507]) ).
fof(f67017,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X1,X2),meet(join(X0,meet(X0,X2)),join(join(X1,X2),meet(X0,join(X1,X2))))),
inference(superposition,[],[f6671,f20507]) ).
fof(f67031,plain,
! [X2,X0,X1] : meet(join(X1,X2),join(X0,meet(X0,X2))) = meet(join(X0,meet(X0,X2)),join(join(X1,X2),meet(X0,join(X1,X2)))),
inference(superposition,[],[f8344,f20507]) ).
fof(f67054,plain,
! [X2,X0,X1] : meet(join(X1,X2),join(X0,meet(X0,X2))) = meet(join(X0,meet(X0,X2)),join(X1,join(X2,meet(X0,join(X1,X2))))),
inference(forward_demodulation,[],[f67031,f6]) ).
fof(f67067,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(join(X1,X2),meet(X0,join(X1,X2))),join(X0,meet(X0,X2))),
inference(forward_demodulation,[],[f67017,f20667]) ).
fof(f67120,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X0,join(X1,X2))) = meet(meet(X0,join(X0,X2)),meet(join(X1,X2),X3)),
inference(forward_demodulation,[],[f66961,f27183]) ).
fof(f67129,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X1,X2),meet(X0,join(X0,X2))),
inference(forward_demodulation,[],[f66952,f27183]) ).
fof(f67257,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(X0,meet(join(X1,X0),join(X2,X1))),
inference(forward_demodulation,[],[f66810,f5]) ).
fof(f67334,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(meet(X0,join(X0,X1)),join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f66733,f27183]) ).
fof(f67347,plain,
! [X2,X0,X1] : meet(join(X1,X2),join(X0,meet(X0,X2))) = meet(join(X0,meet(X0,X2)),meet(join(X1,X2),join(X1,join(X2,X0)))),
inference(forward_demodulation,[],[f67054,f27742]) ).
fof(f67360,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(join(X1,X2),meet(X0,join(X1,X2))),meet(X0,join(X0,X2))),
inference(forward_demodulation,[],[f67067,f27183]) ).
fof(f67406,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X0,join(X1,X2))) = meet(X0,meet(join(X0,X2),meet(join(X1,X2),X3))),
inference(forward_demodulation,[],[f67120,f5]) ).
fof(f67587,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(X0,meet(join(X0,X1),join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f67334,f5]) ).
fof(f67599,plain,
! [X2,X0,X1] : meet(join(X1,X2),meet(X0,join(X0,X2))) = meet(meet(X0,join(X0,X2)),meet(join(X1,X2),join(X1,join(X2,X0)))),
inference(forward_demodulation,[],[f67347,f27183]) ).
fof(f67603,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X0,X2),join(meet(X0,join(X1,X2)),join(X1,X2)))),
inference(forward_demodulation,[],[f67360,f5371]) ).
fof(f67703,plain,
! [X2,X0,X1] : meet(join(X1,X2),meet(X0,join(X0,X2))) = meet(X0,meet(join(X0,X2),meet(join(X1,X2),join(X1,join(X2,X0))))),
inference(forward_demodulation,[],[f67599,f5]) ).
fof(f67706,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X0,X2),join(join(X1,X2),meet(X0,join(X1,X2))))),
inference(forward_demodulation,[],[f67603,f5326]) ).
fof(f67754,plain,
! [X2,X0,X1] : meet(join(X1,X2),meet(X0,join(X0,X2))) = meet(join(X1,join(X2,X0)),meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f67703,f67406]) ).
fof(f67757,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X0,X2),meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f67706,f7199]) ).
fof(f67789,plain,
! [X2,X0,X1] : meet(join(X1,X2),meet(X0,join(X0,X2))) = meet(X0,meet(join(X1,X2),join(join(X2,X0),X1))),
inference(forward_demodulation,[],[f67754,f5371]) ).
fof(f67791,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(X2,X0))),
inference(forward_demodulation,[],[f67757,f5371]) ).
fof(f67814,plain,
! [X2,X0,X1] : meet(X0,meet(join(X1,X2),join(X2,join(X0,X1)))) = meet(join(X1,X2),meet(X0,join(X0,X2))),
inference(forward_demodulation,[],[f67789,f6]) ).
fof(f67830,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(X0,meet(join(X1,X2),join(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f67814,f64429]) ).
fof(f67839,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(X0,join(X2,join(X1,meet(X2,X0)))),
inference(forward_demodulation,[],[f67830,f64981]) ).
fof(f67958,plain,
! [X2,X0,X1] : join(X2,meet(X1,X0)) = join(X2,meet(X1,join(meet(X0,X1),X2))),
inference(superposition,[],[f20534,f8028]) ).
fof(f67959,plain,
! [X2,X0,X1] : join(X0,meet(X2,X1)) = join(X0,meet(X2,join(X0,meet(X1,X2)))),
inference(superposition,[],[f20534,f7450]) ).
fof(f69050,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X1,meet(X0,join(X1,X2))),meet(X0,join(X1,X2))),
inference(superposition,[],[f25124,f98]) ).
fof(f69343,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(meet(X0,join(X1,X2)),join(X1,meet(join(X1,X2),X0))),
inference(forward_demodulation,[],[f69050,f8003]) ).
fof(f69509,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(X1,meet(join(X1,X2),X0)))),
inference(forward_demodulation,[],[f69343,f5]) ).
fof(f69634,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X1,meet(join(X1,X2),X0))),
inference(forward_demodulation,[],[f69509,f654]) ).
fof(f71060,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X1,X0),meet(X2,join(X0,X2))),
inference(superposition,[],[f8028,f32156]) ).
fof(f71914,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(X0,X1))),
inference(superposition,[],[f1035,f32320]) ).
fof(f81810,plain,
! [X2,X3,X0,X1] : meet(join(X2,X0),join(X1,X3)) = meet(join(X1,X3),meet(join(X2,X0),join(X0,join(X1,X2)))),
inference(superposition,[],[f64411,f729]) ).
fof(f81917,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X1,X2),meet(meet(X0,join(X0,X1)),meet(X0,join(X1,X2)))),
inference(superposition,[],[f20,f64411]) ).
fof(f82087,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X1,X2),meet(X0,meet(meet(X0,join(X0,X1)),join(X2,X1)))),
inference(forward_demodulation,[],[f81917,f39794]) ).
fof(f82162,plain,
! [X2,X3,X0,X1] : meet(join(X2,X0),join(X1,X3)) = meet(join(X1,X3),join(X0,join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f81810,f64981]) ).
fof(f82292,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(meet(X0,join(X0,X1)),meet(join(X2,X1),X0)),
inference(forward_demodulation,[],[f82087,f9780]) ).
fof(f82436,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X0,X1),meet(join(X2,X1),X0))),
inference(forward_demodulation,[],[f82292,f5]) ).
fof(f82514,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X0,X1),meet(join(X2,X1),X0)),
inference(forward_demodulation,[],[f82436,f42]) ).
fof(f82555,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X2,X1),join(X1,X0))),
inference(forward_demodulation,[],[f82514,f5370]) ).
fof(f85418,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(meet(X1,X0),meet(X1,X2))),
inference(superposition,[],[f1566,f66626]) ).
fof(f86123,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X0,X1)))) = meet(join(X2,meet(X0,join(X0,X1))),meet(X1,join(X0,X1))),
inference(superposition,[],[f67129,f4376]) ).
fof(f86214,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X1,X0))) = meet(join(X2,meet(X1,X0)),join(X0,meet(X1,X0))),
inference(superposition,[],[f67129,f6299]) ).
fof(f86512,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X1,X0))) = meet(join(X2,meet(X1,X0)),meet(X0,join(X0,X1))),
inference(forward_demodulation,[],[f86214,f27289]) ).
fof(f86568,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X0,X1)))) = meet(X1,meet(join(X0,X1),join(meet(X0,join(X0,X1)),X2))),
inference(forward_demodulation,[],[f86123,f5371]) ).
fof(f86664,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X1,X0))) = meet(X0,meet(join(X0,X1),join(meet(X1,X0),X2))),
inference(forward_demodulation,[],[f86512,f5371]) ).
fof(f86715,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X0,X1)))) = meet(X1,meet(join(X0,X1),join(X0,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f86568,f27344]) ).
fof(f86809,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X0,X1)))) = meet(X1,join(X0,join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f86715,f64521]) ).
fof(f86875,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,join(X2,meet(X0,join(X0,X1)))),
inference(forward_demodulation,[],[f86809,f67839]) ).
fof(f87184,plain,
! [X2,X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),X2)) = meet(meet(X0,X1),join(X0,X2)),
inference(superposition,[],[f67791,f29897]) ).
fof(f87282,plain,
! [X2,X0,X1] : meet(meet(join(X1,X2),join(X2,X0)),X0) = meet(meet(join(X1,X2),join(X2,X0)),meet(X0,join(X1,X2))),
inference(superposition,[],[f284,f67791]) ).
fof(f87410,plain,
! [X2,X0,X1] : meet(meet(join(X1,X2),join(X2,X0)),X0) = meet(join(X1,X2),meet(join(X2,X0),meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f87282,f5]) ).
fof(f87461,plain,
! [X2,X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),X2)) = meet(X0,meet(X1,join(X0,X2))),
inference(forward_demodulation,[],[f87184,f5]) ).
fof(f87612,plain,
! [X2,X0,X1] : meet(meet(join(X1,X2),join(X2,X0)),X0) = meet(join(X1,X2),meet(X0,meet(join(X2,X0),join(X2,X1)))),
inference(forward_demodulation,[],[f87410,f39794]) ).
fof(f87646,plain,
! [X2,X0,X1] : meet(X0,meet(X1,join(meet(X0,X1),X2))) = meet(X0,meet(X1,join(X0,X2))),
inference(forward_demodulation,[],[f87461,f5]) ).
fof(f87752,plain,
! [X2,X0,X1] : meet(meet(join(X1,X2),join(X2,X0)),X0) = meet(join(X2,X0),meet(join(X2,X1),X0)),
inference(forward_demodulation,[],[f87612,f9780]) ).
fof(f87805,plain,
! [X2,X0,X1] : meet(meet(join(X1,X2),join(X2,X0)),X0) = meet(X0,meet(join(X2,X1),join(X0,X2))),
inference(forward_demodulation,[],[f87752,f5370]) ).
fof(f87841,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(meet(join(X1,X2),join(X2,X0)),X0),
inference(forward_demodulation,[],[f87805,f71914]) ).
fof(f87867,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(join(X1,X2),meet(join(X2,X0),X0)),
inference(forward_demodulation,[],[f87841,f5]) ).
fof(f87889,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(join(X1,X2),meet(X0,join(X2,X0))),
inference(forward_demodulation,[],[f87867,f1035]) ).
fof(f91771,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(join(X0,X1),meet(X1,X2)),join(X0,meet(X1,X2))),
inference(superposition,[],[f106,f641]) ).
fof(f91948,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(join(X0,meet(X1,X2)),meet(join(X1,X0),meet(X1,X2))),
inference(forward_demodulation,[],[f91771,f7937]) ).
fof(f92085,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(meet(X1,X2),meet(join(X1,X0),meet(X1,X2)))),
inference(forward_demodulation,[],[f91948,f6]) ).
fof(f92163,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(meet(X1,X2),meet(X1,meet(X2,join(X1,X0))))),
inference(forward_demodulation,[],[f92085,f8257]) ).
fof(f92214,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X1,meet(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f92163,f11875]) ).
fof(f92549,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X2,X3)) = meet(join(meet(X3,X2),X1),join(meet(X0,X1),meet(X2,X3))),
inference(superposition,[],[f668,f7450]) ).
fof(f122961,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,join(X0,X1))),join(X0,join(X1,X2))) = join(join(X2,meet(X0,join(X0,X1))),meet(join(X2,meet(X0,join(X0,X1))),join(X0,join(X1,X2)))),
inference(superposition,[],[f4167,f4480]) ).
fof(f122992,plain,
! [X2,X3,X0,X1] : meet(join(X2,meet(X0,join(X0,X1))),join(X1,X3)) = meet(join(X2,meet(X0,join(X0,X1))),meet(join(X1,X3),join(X0,join(X1,X2)))),
inference(superposition,[],[f65011,f4480]) ).
fof(f123009,plain,
! [X2,X3,X0,X1] : meet(join(X2,meet(X0,join(X0,X1))),join(X1,X3)) = meet(join(X0,join(X1,X2)),meet(join(X1,X3),join(meet(X0,join(X0,X1)),X2))),
inference(forward_demodulation,[],[f122992,f5370]) ).
fof(f123036,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,join(X0,X1))),join(X0,join(X1,X2))) = join(X2,join(meet(X0,join(X0,X1)),meet(join(X2,meet(X0,join(X0,X1))),join(X0,join(X1,X2))))),
inference(forward_demodulation,[],[f122961,f6]) ).
fof(f123306,plain,
! [X2,X3,X0,X1] : meet(join(X2,meet(X0,join(X0,X1))),join(X1,X3)) = meet(join(X0,join(X1,X2)),meet(join(X1,X3),join(X0,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f123009,f27344]) ).
fof(f123331,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,join(X0,X1))),join(X0,join(X1,X2))) = join(X2,join(meet(X0,join(X0,X1)),meet(join(X0,join(X1,X2)),join(meet(X0,join(X0,X1)),X2)))),
inference(forward_demodulation,[],[f123036,f26978]) ).
fof(f123548,plain,
! [X2,X3,X0,X1] : meet(join(X2,meet(X0,join(X0,X1))),join(X1,X3)) = meet(join(X0,join(X1,X2)),meet(join(X2,X0),join(X1,X3))),
inference(forward_demodulation,[],[f123306,f82162]) ).
fof(f123562,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,join(X0,X1))),join(X0,join(X1,X2))) = meet(join(X2,meet(X0,join(X0,X1))),join(X2,join(meet(X0,join(X0,X1)),join(X0,join(X1,X2))))),
inference(forward_demodulation,[],[f123331,f27514]) ).
fof(f123730,plain,
! [X2,X3,X0,X1] : meet(join(X2,meet(X0,join(X0,X1))),join(X1,X3)) = meet(join(X2,X0),meet(join(X1,X3),join(join(X1,X2),X0))),
inference(forward_demodulation,[],[f123548,f5371]) ).
fof(f123740,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,join(X0,X1))),join(X0,join(X1,X2))) = meet(join(X2,meet(X0,join(X0,X1))),join(X2,join(X0,join(meet(X0,join(X0,X1)),join(X1,X2))))),
inference(forward_demodulation,[],[f123562,f54620]) ).
fof(f123870,plain,
! [X2,X3,X0,X1] : meet(join(X2,X0),meet(join(X1,X3),join(X1,join(X2,X0)))) = meet(join(X2,meet(X0,join(X0,X1))),join(X1,X3)),
inference(forward_demodulation,[],[f123730,f6]) ).
fof(f123877,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,join(X0,X1))),join(X0,join(X1,X2))) = meet(join(X2,meet(X0,join(X0,X1))),join(X0,join(X1,join(X2,meet(X0,join(X0,X1)))))),
inference(forward_demodulation,[],[f123740,f10163]) ).
fof(f123943,plain,
! [X2,X3,X0,X1] : meet(join(X2,X0),join(X1,X3)) = meet(join(X2,meet(X0,join(X0,X1))),join(X1,X3)),
inference(forward_demodulation,[],[f123870,f65011]) ).
fof(f123949,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,join(X0,X1))),join(X1,join(X2,meet(X0,join(X0,X1))))) = meet(join(X2,meet(X0,join(X0,X1))),join(X0,join(X1,X2))),
inference(forward_demodulation,[],[f123877,f49650]) ).
fof(f123992,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,join(X0,X1))),join(X1,join(X2,meet(X0,join(X0,X1))))) = meet(join(X0,join(X1,X2)),join(X2,meet(join(X0,X1),X0))),
inference(forward_demodulation,[],[f123949,f8003]) ).
fof(f124020,plain,
! [X2,X0,X1] : join(X2,meet(join(X0,X1),X0)) = meet(join(X2,meet(X0,join(X0,X1))),join(X1,join(X2,meet(X0,join(X0,X1))))),
inference(forward_demodulation,[],[f123992,f758]) ).
fof(f124037,plain,
! [X2,X0,X1] : join(X2,meet(join(X0,X1),X0)) = meet(join(X2,X0),join(X1,join(X2,meet(X0,join(X0,X1))))),
inference(forward_demodulation,[],[f124020,f123943]) ).
fof(f124050,plain,
! [X2,X0,X1] : join(X2,meet(join(X0,X1),X0)) = meet(join(X2,X0),join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f124037,f4459]) ).
fof(f124058,plain,
! [X2,X0,X1] : join(X2,meet(X0,join(X1,X0))) = meet(join(X2,X0),join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f124050,f8262]) ).
fof(f127336,plain,
! [X2,X3,X0,X1] : meet(join(X1,meet(X2,X3)),join(X0,join(X1,X2))) = meet(join(X1,meet(X2,X3)),join(X0,join(X1,meet(X2,X3)))),
inference(superposition,[],[f65011,f676]) ).
fof(f136071,plain,
! [X2,X0,X1] : meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2)) = join(join(meet(X0,X2),meet(X0,X1)),meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2))),
inference(superposition,[],[f4167,f32513]) ).
fof(f136072,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(join(meet(X0,X2),meet(X0,X1)),join(X2,meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2)))),
inference(superposition,[],[f4285,f32513]) ).
fof(f136091,plain,
! [X2,X0,X1] : join(join(meet(X0,X2),meet(X0,X1)),meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2))) = meet(join(meet(X0,X2),meet(X0,X1)),join(join(meet(X0,X2),meet(X0,X1)),X2)),
inference(superposition,[],[f24834,f32513]) ).
fof(f136134,plain,
! [X2,X0,X1] : meet(join(meet(X0,X2),meet(X0,X1)),join(X2,join(meet(X0,X2),meet(X0,X1)))) = join(join(meet(X0,X2),meet(X0,X1)),meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f136091,f4872]) ).
fof(f136151,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X0,X2),join(meet(X0,X1),join(X2,meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2))))),
inference(forward_demodulation,[],[f136072,f6]) ).
fof(f136152,plain,
! [X2,X0,X1] : meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2)) = join(meet(X0,X2),join(meet(X0,X1),meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f136071,f6]) ).
fof(f136350,plain,
! [X2,X0,X1] : meet(join(meet(X0,X2),meet(X0,X1)),join(X2,join(meet(X0,X2),meet(X0,X1)))) = join(meet(X0,X2),join(meet(X0,X1),meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f136134,f6]) ).
fof(f136367,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,join(meet(X2,X0),join(meet(X0,X1),meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2))))),
inference(forward_demodulation,[],[f136151,f49939]) ).
fof(f136368,plain,
! [X2,X0,X1] : meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2)) = meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X2),join(meet(X0,X1),join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f136152,f27367]) ).
fof(f136497,plain,
! [X2,X0,X1] : meet(join(meet(X0,X2),meet(X0,X1)),join(X2,join(meet(X0,X2),meet(X0,X1)))) = meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X2),join(meet(X0,X1),join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f136350,f27367]) ).
fof(f136505,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,join(meet(X2,X0),join(meet(X0,X1),meet(join(meet(X0,X1),X2),join(meet(X0,X2),meet(X0,X1)))))),
inference(forward_demodulation,[],[f136367,f56373]) ).
fof(f136506,plain,
! [X2,X0,X1] : meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2)) = join(meet(X0,X2),meet(meet(X0,X1),join(join(meet(X0,X1),X2),meet(X0,X1)))),
inference(forward_demodulation,[],[f136368,f124058]) ).
fof(f136578,plain,
! [X2,X0,X1] : meet(join(meet(X0,X2),meet(X0,X1)),join(X2,join(meet(X0,X2),meet(X0,X1)))) = join(meet(X0,X2),meet(meet(X0,X1),join(join(meet(X0,X1),X2),meet(X0,X1)))),
inference(forward_demodulation,[],[f136497,f124058]) ).
fof(f136583,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(join(meet(X0,X1),X2),join(meet(X0,X2),meet(X0,X1))),join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f136505,f54524]) ).
fof(f136584,plain,
! [X2,X0,X1] : meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2)) = join(meet(X0,X2),meet(meet(X0,X1),join(meet(X0,X1),join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f136506,f8263]) ).
fof(f136624,plain,
! [X2,X0,X1] : meet(join(meet(X0,X2),meet(X0,X1)),join(X2,join(meet(X0,X2),meet(X0,X1)))) = join(meet(X0,X2),meet(meet(X0,X1),join(meet(X0,X1),join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f136578,f8263]) ).
fof(f136627,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(join(meet(X0,X1),X2),meet(join(X2,meet(X0,X1)),join(meet(X0,X2),meet(X0,X1)))),
inference(forward_demodulation,[],[f136583,f7937]) ).
fof(f136628,plain,
! [X2,X0,X1] : meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2)) = join(meet(X0,X2),meet(X0,meet(X1,join(meet(X0,X1),join(meet(X0,X1),X2))))),
inference(forward_demodulation,[],[f136584,f5]) ).
fof(f136657,plain,
! [X2,X0,X1] : meet(join(meet(X0,X2),meet(X0,X1)),join(X2,join(meet(X0,X2),meet(X0,X1)))) = join(meet(X0,X2),meet(X0,meet(X1,join(meet(X0,X1),join(meet(X0,X1),X2))))),
inference(forward_demodulation,[],[f136624,f5]) ).
fof(f136659,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X0,X1),join(X2,meet(join(X2,meet(X0,X1)),join(meet(X0,X2),meet(X0,X1))))),
inference(forward_demodulation,[],[f136627,f6]) ).
fof(f136660,plain,
! [X2,X0,X1] : meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2)) = join(meet(X0,X2),meet(X0,meet(X1,join(X0,join(meet(X0,X1),X2))))),
inference(forward_demodulation,[],[f136628,f87646]) ).
fof(f136679,plain,
! [X2,X0,X1] : meet(join(meet(X0,X2),meet(X0,X1)),join(X2,join(meet(X0,X2),meet(X0,X1)))) = join(meet(X0,X2),meet(X0,meet(X1,join(X0,join(meet(X0,X1),X2))))),
inference(forward_demodulation,[],[f136657,f87646]) ).
fof(f136681,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(X2,meet(X0,X1)),join(X2,join(meet(X0,X1),join(meet(X0,X2),meet(X0,X1))))),
inference(forward_demodulation,[],[f136659,f27368]) ).
fof(f136682,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X1,meet(X0,join(X0,X2)))) = meet(join(meet(X0,X2),meet(X0,X1)),join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f136660,f51750]) ).
fof(f136692,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X1,meet(X0,join(X0,X2)))) = meet(join(meet(X0,X2),meet(X0,X1)),join(X2,join(meet(X0,X2),meet(X0,X1)))),
inference(forward_demodulation,[],[f136679,f51750]) ).
fof(f136694,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(meet(X0,X1),join(join(meet(X0,X2),meet(X0,X1)),meet(X0,X1)))),
inference(forward_demodulation,[],[f136681,f124058]) ).
fof(f136695,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X1,meet(X0,join(X0,X2)))) = meet(join(meet(X0,X1),X2),join(meet(X0,X2),meet(X1,X0))),
inference(forward_demodulation,[],[f136682,f8003]) ).
fof(f136701,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X1,meet(X0,join(X0,X2)))) = meet(join(meet(X0,X2),meet(X0,X1)),join(X2,join(meet(X0,X2),X0))),
inference(forward_demodulation,[],[f136692,f127336]) ).
fof(f136702,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(meet(X0,X1),join(meet(X0,X1),join(meet(X0,X2),meet(X0,X1))))),
inference(forward_demodulation,[],[f136694,f8263]) ).
fof(f136703,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X1,X0)) = join(meet(X0,X2),meet(X1,meet(X0,join(X0,X2)))),
inference(forward_demodulation,[],[f136695,f92549]) ).
fof(f136709,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X1,meet(X0,join(X0,X2)))) = meet(join(meet(X0,X2),meet(X0,X1)),join(X2,join(X0,meet(X0,X2)))),
inference(forward_demodulation,[],[f136701,f5561]) ).
fof(f136710,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X0,meet(X1,join(meet(X0,X1),join(meet(X0,X2),meet(X0,X1)))))),
inference(forward_demodulation,[],[f136702,f5]) ).
fof(f136712,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X1,meet(X0,join(X0,X2)))) = meet(join(meet(X0,X2),meet(X0,X1)),join(X2,meet(X0,join(X0,X2)))),
inference(forward_demodulation,[],[f136709,f27183]) ).
fof(f136713,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X0,meet(X1,join(X0,join(meet(X0,X2),meet(X0,X1)))))),
inference(forward_demodulation,[],[f136710,f87646]) ).
fof(f136714,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X1,meet(X0,join(X0,X2)))) = meet(join(meet(X0,X2),meet(X0,X1)),join(X0,X2)),
inference(forward_demodulation,[],[f136712,f4376]) ).
fof(f136715,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X0,meet(join(X0,meet(X0,X2)),X1))),
inference(forward_demodulation,[],[f136713,f66557]) ).
fof(f136716,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X1,meet(X0,join(X0,X2)))) = meet(join(X0,X2),join(meet(X0,X2),meet(X1,X0))),
inference(forward_demodulation,[],[f136714,f8003]) ).
fof(f136717,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X1,join(X0,meet(X0,X2)))),
inference(forward_demodulation,[],[f136715,f6352]) ).
fof(f136718,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X1,X0)) = meet(join(X0,X2),join(meet(X0,X2),meet(X1,X0))),
inference(forward_demodulation,[],[f136716,f136703]) ).
fof(f136719,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X1,meet(X0,join(X0,X2)))),
inference(forward_demodulation,[],[f136717,f27183]) ).
fof(f152228,plain,
! [X2,X0,X1] : meet(X2,join(meet(X1,X0),X0)) = meet(X2,meet(meet(X0,join(X0,X1)),join(meet(X1,X0),X2))),
inference(superposition,[],[f82555,f27289]) ).
fof(f153052,plain,
! [X2,X0,X1] : meet(X2,join(meet(X1,X0),X0)) = meet(X2,meet(X0,meet(join(X0,X1),join(meet(X1,X0),X2)))),
inference(forward_demodulation,[],[f152228,f5]) ).
fof(f153347,plain,
! [X2,X0,X1] : meet(X2,join(meet(X1,X0),X0)) = meet(X2,meet(X0,join(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f153052,f86664]) ).
fof(f153571,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X1,X0))) = meet(X2,meet(X0,join(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f153347,f4872]) ).
fof(f153731,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X0,X1))) = meet(X2,meet(X0,join(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f153571,f27289]) ).
fof(f154385,plain,
! [X2,X0,X1] : join(join(meet(X1,X0),meet(X1,X2)),meet(join(meet(X1,X0),meet(X1,X2)),join(X0,meet(X1,X2)))) = meet(join(meet(X1,X0),meet(X1,X2)),join(join(meet(X1,X0),meet(X1,X2)),X0)),
inference(superposition,[],[f24834,f85418]) ).
fof(f154437,plain,
! [X2,X0,X1] : meet(join(meet(X1,X0),meet(X1,X2)),join(X0,join(meet(X1,X0),meet(X1,X2)))) = join(join(meet(X1,X0),meet(X1,X2)),meet(join(meet(X1,X0),meet(X1,X2)),join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f154385,f4872]) ).
fof(f154662,plain,
! [X2,X0,X1] : meet(join(meet(X1,X0),meet(X1,X2)),join(X0,join(meet(X1,X0),meet(X1,X2)))) = join(meet(X1,X0),join(meet(X1,X2),meet(join(meet(X1,X0),meet(X1,X2)),join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f154437,f6]) ).
fof(f154815,plain,
! [X2,X0,X1] : meet(join(meet(X1,X0),meet(X1,X2)),join(X0,join(meet(X1,X0),meet(X1,X2)))) = meet(join(meet(X1,X0),meet(X1,X2)),join(meet(X1,X0),join(meet(X1,X2),join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f154662,f27367]) ).
fof(f154906,plain,
! [X2,X0,X1] : meet(join(meet(X1,X0),meet(X1,X2)),join(X0,join(meet(X1,X0),meet(X1,X2)))) = join(meet(X1,X0),meet(meet(X1,X2),join(join(X0,meet(X1,X2)),meet(X1,X2)))),
inference(forward_demodulation,[],[f154815,f124058]) ).
fof(f154966,plain,
! [X2,X0,X1] : meet(join(meet(X1,X0),meet(X1,X2)),join(X0,join(meet(X1,X0),meet(X1,X2)))) = join(meet(X1,X0),meet(meet(X1,X2),join(meet(X1,X2),join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f154906,f8263]) ).
fof(f154999,plain,
! [X2,X0,X1] : meet(join(meet(X1,X0),meet(X1,X2)),join(X0,join(meet(X1,X0),meet(X1,X2)))) = join(meet(X1,X0),meet(X1,meet(X2,join(meet(X1,X2),join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f154966,f5]) ).
fof(f155019,plain,
! [X2,X0,X1] : meet(join(meet(X1,X0),meet(X1,X2)),join(X0,join(meet(X1,X0),meet(X1,X2)))) = join(meet(X1,X0),meet(X1,meet(X2,join(X1,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f154999,f87646]) ).
fof(f155031,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,meet(join(X1,X0),X2))) = meet(join(meet(X1,X0),meet(X1,X2)),join(X0,join(meet(X1,X0),meet(X1,X2)))),
inference(forward_demodulation,[],[f155019,f66557]) ).
fof(f155039,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,meet(join(X1,X0),X2))) = meet(join(meet(X1,X0),meet(X1,X2)),join(X0,join(meet(X1,X0),X1))),
inference(forward_demodulation,[],[f155031,f127336]) ).
fof(f155043,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,meet(join(X1,X0),X2))) = meet(join(meet(X1,X0),meet(X1,X2)),join(X0,join(X1,meet(X1,X0)))),
inference(forward_demodulation,[],[f155039,f5561]) ).
fof(f155045,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,meet(join(X1,X0),X2))) = meet(join(meet(X1,X0),meet(X1,X2)),join(X0,meet(X1,join(X1,X0)))),
inference(forward_demodulation,[],[f155043,f27183]) ).
fof(f155046,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,meet(join(X1,X0),X2))) = meet(join(meet(X1,X0),meet(X1,X2)),join(X1,X0)),
inference(forward_demodulation,[],[f155045,f4376]) ).
fof(f155047,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,meet(join(X1,X0),X2))) = meet(join(X1,X0),join(meet(X1,X0),meet(X2,X1))),
inference(forward_demodulation,[],[f155046,f8003]) ).
fof(f155048,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X2,X1)) = join(meet(X1,X0),meet(X1,meet(join(X1,X0),X2))),
inference(forward_demodulation,[],[f155047,f136718]) ).
fof(f156175,plain,
! [X2,X0,X1] : meet(join(meet(X0,X1),X0),join(X2,meet(join(X0,X2),meet(X0,X1)))) = join(meet(X0,X1),meet(X2,join(meet(X0,X2),meet(X0,X1)))),
inference(superposition,[],[f2185,f13]) ).
fof(f156340,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(meet(X0,join(X1,meet(X0,X1))),meet(join(X1,meet(X0,join(X1,meet(X0,X1)))),X2))) = join(meet(X1,X2),meet(meet(X0,join(X1,meet(X0,X1))),join(meet(X0,X1),X2))),
inference(superposition,[],[f2185,f6671]) ).
fof(f156411,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(X0,meet(join(X1,X0),X2))) = join(meet(X1,X2),meet(X0,join(meet(X0,X1),X2))),
inference(superposition,[],[f2185,f8028]) ).
fof(f156522,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(join(X0,meet(X0,X2)),meet(join(X1,join(X0,meet(X0,X2))),X2))) = join(meet(X1,X2),meet(X0,join(meet(X1,join(X0,meet(X0,X2))),X2))),
inference(superposition,[],[f2185,f20507]) ).
fof(f156878,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(join(X0,meet(X0,X2)),meet(join(X1,join(X0,meet(X0,X2))),X2))) = join(meet(X1,X2),meet(X0,join(X2,meet(X1,join(X0,meet(X0,X2)))))),
inference(forward_demodulation,[],[f156522,f8263]) ).
fof(f157048,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(meet(X0,join(X1,meet(X0,X1))),meet(join(X1,meet(X0,join(X1,meet(X0,X1)))),X2))) = join(meet(X1,X2),meet(X0,meet(join(X1,meet(X0,X1)),join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f156340,f5]) ).
fof(f157175,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(join(meet(X0,X1),X0),join(X2,meet(join(X0,X2),meet(X0,X1)))),
inference(forward_demodulation,[],[f156175,f67958]) ).
fof(f157312,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(meet(X0,join(X0,X2)),meet(join(X1,meet(X0,join(X0,X2))),X2))) = join(meet(X1,X2),meet(X0,join(X2,meet(X1,meet(X0,join(X0,X2)))))),
inference(forward_demodulation,[],[f156878,f27183]) ).
fof(f157458,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(meet(X0,join(X1,meet(X0,X1))),meet(join(X1,meet(X0,join(X1,meet(X0,X1)))),X2))) = join(meet(X1,X2),meet(join(meet(X0,X1),X2),meet(X0,X1))),
inference(forward_demodulation,[],[f157048,f7195]) ).
fof(f157566,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(join(X0,meet(X0,X1)),join(meet(join(X0,X2),meet(X0,X1)),X2)),
inference(forward_demodulation,[],[f157175,f5299]) ).
fof(f157668,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(meet(X0,join(X0,X2)),meet(join(X1,meet(X0,join(X0,X2))),X2))) = join(meet(X1,X2),meet(X0,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f157312,f136719]) ).
fof(f157752,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(meet(X0,join(X1,meet(X0,X1))),meet(join(X1,meet(X0,join(X1,meet(X0,X1)))),X2))) = join(meet(X1,X2),meet(meet(X0,X1),join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f157458,f8262]) ).
fof(f157825,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(join(X0,meet(X0,X1)),join(X2,meet(join(X0,X2),meet(X0,X1)))),
inference(forward_demodulation,[],[f157566,f4872]) ).
fof(f157916,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(X0,meet(join(X1,X0),X2))) = meet(join(X2,X1),join(meet(X0,join(X0,X2)),meet(join(X1,meet(X0,join(X0,X2))),X2))),
inference(forward_demodulation,[],[f157668,f156411]) ).
fof(f157989,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(meet(X0,join(X1,meet(X0,X1))),meet(join(X1,meet(X0,join(X1,meet(X0,X1)))),X2))) = join(meet(X2,X1),meet(X0,X1)),
inference(forward_demodulation,[],[f157752,f71060]) ).
fof(f158056,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(join(X0,meet(X0,X1)),join(X2,meet(X0,meet(X1,join(X0,X2))))),
inference(forward_demodulation,[],[f157825,f8257]) ).
fof(f158138,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(X0,meet(join(X1,X0),X2))) = meet(join(X2,X1),join(meet(X0,join(X0,X2)),meet(X2,join(X1,meet(X0,join(X0,X2)))))),
inference(forward_demodulation,[],[f157916,f8005]) ).
fof(f158205,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(join(X2,X1),join(meet(X0,join(X1,meet(X0,X1))),meet(join(meet(X0,X1),X1),X2))),
inference(forward_demodulation,[],[f157989,f66625]) ).
fof(f158268,plain,
! [X2,X0,X1] : meet(join(X0,meet(X0,X1)),join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(X2,X0)),
inference(forward_demodulation,[],[f158056,f92214]) ).
fof(f158342,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(X0,meet(join(X1,X0),X2))) = meet(join(X2,X1),join(X0,meet(X2,join(X1,meet(X0,join(X0,X2)))))),
inference(forward_demodulation,[],[f158138,f25426]) ).
fof(f158400,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(join(X2,X1),join(meet(X0,join(X1,meet(X0,X1))),meet(join(X1,meet(X0,X1)),X2))),
inference(forward_demodulation,[],[f158205,f8252]) ).
fof(f158435,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(meet(X0,join(X0,X1)),join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f158268,f27183]) ).
fof(f158500,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(X0,meet(join(X1,X0),X2))) = meet(join(X2,X1),join(X0,meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f158342,f86875]) ).
fof(f158548,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(join(X2,X1),join(meet(X0,meet(X1,join(X1,X0))),meet(meet(X1,join(X1,X0)),X2))),
inference(forward_demodulation,[],[f158400,f27289]) ).
fof(f158577,plain,
! [X2,X0,X1] : meet(X0,meet(join(X0,X1),join(X2,meet(X0,X1)))) = join(meet(X0,X1),meet(X2,X0)),
inference(forward_demodulation,[],[f158435,f5]) ).
fof(f158679,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(join(X2,X1),join(meet(X0,meet(X1,join(X1,X0))),meet(X1,meet(join(X1,X0),X2)))),
inference(forward_demodulation,[],[f158548,f5]) ).
fof(f158702,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(X2,X0)),
inference(forward_demodulation,[],[f158577,f67587]) ).
fof(f158789,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(join(X2,X1),join(meet(X1,X0),meet(X1,meet(join(X1,X0),X2)))),
inference(forward_demodulation,[],[f158679,f27308]) ).
fof(f158865,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(join(X2,X1),join(meet(X1,X0),meet(X2,X1))),
inference(forward_demodulation,[],[f158789,f155048]) ).
fof(f158926,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(join(X2,X1),meet(X1,join(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f158865,f158702]) ).
fof(f158974,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = join(meet(X2,X1),meet(X0,X1)),
inference(forward_demodulation,[],[f158926,f640]) ).
fof(f159357,plain,
! [X2,X3,X0,X1] : join(meet(X1,X3),meet(X0,meet(X1,X2))) = meet(X1,join(meet(X2,X0),meet(X1,X3))),
inference(superposition,[],[f158702,f275]) ).
fof(f159472,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = join(meet(X1,X0),meet(X0,X2)),
inference(superposition,[],[f4,f158702]) ).
fof(f159499,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,join(X1,meet(X0,X2)))) = join(meet(X1,X0),join(meet(X0,X2),X3)),
inference(superposition,[],[f512,f158702]) ).
fof(f159507,plain,
! [X2,X3,X0,X1] : join(meet(meet(X1,X0),X3),meet(X0,X2)) = meet(meet(X0,join(X1,meet(X0,X2))),join(meet(meet(X1,X0),X3),meet(X0,X2))),
inference(superposition,[],[f661,f158702]) ).
fof(f159669,plain,
! [X2,X3,X0,X1] : join(meet(meet(X1,X0),X3),meet(X0,X2)) = meet(X0,meet(join(X1,meet(X0,X2)),join(meet(meet(X1,X0),X3),meet(X0,X2)))),
inference(forward_demodulation,[],[f159507,f5]) ).
fof(f159917,plain,
! [X2,X3,X0,X1] : join(meet(X1,meet(X0,X3)),meet(X0,X2)) = meet(X0,meet(join(X1,meet(X0,X2)),join(meet(X1,meet(X0,X3)),meet(X0,X2)))),
inference(forward_demodulation,[],[f159669,f5]) ).
fof(f160127,plain,
! [X2,X3,X0,X1] : join(meet(X1,meet(X0,X3)),meet(X0,X2)) = meet(X0,join(meet(X0,X2),meet(X1,meet(X0,X3)))),
inference(forward_demodulation,[],[f159917,f25158]) ).
fof(f160312,plain,
! [X2,X3,X0,X1] : join(meet(X1,meet(X0,X3)),meet(X0,X2)) = meet(X0,meet(X0,join(meet(X3,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f160127,f159357]) ).
fof(f160460,plain,
! [X2,X3,X0,X1] : join(meet(X1,meet(X0,X3)),meet(X0,X2)) = meet(X0,join(meet(X3,X1),meet(X0,X2))),
inference(forward_demodulation,[],[f160312,f13]) ).
fof(f160985,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),meet(X3,X0)) = meet(X0,join(join(X2,X1),meet(X0,X3))),
inference(superposition,[],[f158974,f4870]) ).
fof(f161074,plain,
! [X2,X3,X0,X1] : meet(X0,join(X3,meet(X0,meet(X2,X1)))) = join(meet(X3,X0),meet(X0,meet(X1,X2))),
inference(superposition,[],[f158974,f2618]) ).
fof(f161076,plain,
! [X2,X3,X0,X1] : meet(X1,join(X3,meet(X1,meet(X2,X0)))) = join(meet(X3,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f158974,f275]) ).
fof(f161082,plain,
! [X2,X3,X0,X1] : join(meet(X3,join(X1,X2)),meet(X0,join(X1,X2))) = meet(join(X1,X2),join(X3,meet(join(X1,X2),join(X0,meet(X0,X2))))),
inference(superposition,[],[f158974,f20507]) ).
fof(f161488,plain,
! [X2,X3,X0,X1] : meet(join(X1,X2),join(X3,meet(join(X1,X2),meet(X0,join(X0,X2))))) = join(meet(X3,join(X1,X2)),meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f161082,f27183]) ).
fof(f161492,plain,
! [X2,X3,X0,X1] : meet(X0,join(X3,meet(X0,meet(X1,X2)))) = meet(X0,join(X3,meet(X0,meet(X2,X1)))),
inference(forward_demodulation,[],[f161074,f159472]) ).
fof(f161576,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),meet(X3,X0)) = meet(X0,join(X2,join(X1,meet(X0,X3)))),
inference(forward_demodulation,[],[f160985,f6]) ).
fof(f161787,plain,
! [X2,X3,X0,X1] : meet(join(X1,X2),join(X3,meet(join(X1,X2),meet(X0,join(X0,X2))))) = meet(join(X1,X2),join(X3,meet(join(X1,X2),X0))),
inference(forward_demodulation,[],[f161488,f158974]) ).
fof(f161873,plain,
! [X2,X3,X0,X1] : meet(X0,join(X3,meet(X0,join(X1,X2)))) = meet(X0,join(X2,join(X1,meet(X0,X3)))),
inference(forward_demodulation,[],[f161576,f158702]) ).
fof(f162068,plain,
! [X2,X3,X0,X1] : meet(join(X1,X2),join(X3,meet(X0,join(X2,X1)))) = meet(join(X1,X2),join(X3,meet(join(X1,X2),X0))),
inference(forward_demodulation,[],[f161787,f64429]) ).
fof(f173135,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X1,meet(meet(X0,X1),X2)))) = meet(join(X1,meet(X0,X1)),join(X2,meet(join(meet(X0,X1),X2),X1))),
inference(superposition,[],[f2202,f27]) ).
fof(f174079,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X1,meet(meet(X0,X1),X2)))) = meet(join(X1,meet(X0,X1)),join(X2,meet(X1,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f173135,f158500]) ).
fof(f174454,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X1,meet(meet(X0,X1),X2)))) = meet(join(X1,meet(X0,X1)),join(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f174079,f67959]) ).
fof(f174727,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X1,meet(meet(X0,X1),X2)))) = meet(meet(X1,join(X1,X0)),join(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f174454,f27289]) ).
fof(f174975,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X1,meet(meet(X0,X1),X2)))) = meet(X1,meet(join(X1,X0),join(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f174727,f5]) ).
fof(f175193,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X1,meet(meet(X0,X1),X2)))) = meet(X1,join(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f174975,f67587]) ).
fof(f175388,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X1,meet(X0,meet(X1,X2))))) = meet(X1,join(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f175193,f5]) ).
fof(f175561,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = join(meet(X0,X1),meet(X2,meet(X1,join(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f175388,f27224]) ).
fof(f175707,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = meet(X1,join(X0,meet(X1,meet(join(X1,meet(X0,X2)),X2)))),
inference(forward_demodulation,[],[f175561,f161076]) ).
fof(f175816,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = meet(X1,join(X0,meet(X1,meet(X2,join(X1,meet(X0,X2)))))),
inference(forward_demodulation,[],[f175707,f161492]) ).
fof(f175904,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = meet(X1,join(X0,meet(X1,meet(X2,join(X2,X0))))),
inference(forward_demodulation,[],[f175816,f153731]) ).
fof(f175981,plain,
! [X2,X0,X1] : meet(X1,join(meet(X2,X1),X0)) = meet(X1,join(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f175904,f136719]) ).
fof(f176339,plain,
! [X2,X0,X1] : meet(X1,meet(join(X0,X1),join(X2,meet(join(X1,X2),X0)))) = meet(X1,join(X0,meet(X1,meet(X2,join(meet(X1,X2),X0))))),
inference(superposition,[],[f175981,f2095]) ).
fof(f176350,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(X1,meet(X0,X2))),
inference(superposition,[],[f175981,f8028]) ).
fof(f176470,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(X0,meet(join(X1,X0),X2))) = join(meet(X1,X2),meet(X0,join(X1,meet(X0,X2)))),
inference(superposition,[],[f2185,f175981]) ).
fof(f176820,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(X0,meet(join(X1,X0),X2))) = meet(join(X2,X1),join(X0,meet(X1,join(X2,X0)))),
inference(forward_demodulation,[],[f176470,f8201]) ).
fof(f176895,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,X2),X0)) = meet(X1,meet(join(X0,X1),join(X2,meet(join(X1,X2),X0)))),
inference(forward_demodulation,[],[f176339,f4534]) ).
fof(f177179,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,X2),X0)) = meet(X1,meet(join(X0,X1),join(X2,meet(X1,join(X0,X2))))),
inference(forward_demodulation,[],[f176895,f176820]) ).
fof(f177412,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = meet(X1,meet(join(X0,X1),join(X2,meet(X1,join(X0,X2))))),
inference(forward_demodulation,[],[f177179,f176350]) ).
fof(f178551,plain,
! [X2,X0,X1] : meet(meet(X0,join(X1,X0)),join(X2,X1)) = meet(meet(X0,join(X1,X0)),join(X2,meet(X0,join(X1,X2)))),
inference(superposition,[],[f69634,f87889]) ).
fof(f178934,plain,
! [X2,X0,X1] : meet(meet(X0,join(X1,X0)),join(X2,X1)) = meet(X0,meet(join(X1,X0),join(X2,meet(X0,join(X1,X2))))),
inference(forward_demodulation,[],[f178551,f5]) ).
fof(f179313,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(meet(X0,join(X1,X0)),join(X2,X1)),
inference(forward_demodulation,[],[f178934,f177412]) ).
fof(f179594,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(X0,meet(join(X1,X0),join(X2,X1))),
inference(forward_demodulation,[],[f179313,f5]) ).
fof(f179825,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(X0,join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f179594,f67257]) ).
fof(f180429,plain,
! [X2,X3,X0,X1] : meet(X0,join(X3,join(meet(X1,X0),X2))) = meet(X0,join(X3,meet(X0,join(X1,meet(X0,X2))))),
inference(superposition,[],[f179825,f175981]) ).
fof(f180432,plain,
! [X2,X3,X0,X1] : meet(meet(X2,X0),join(X3,X1)) = meet(meet(X2,X0),join(X3,meet(X0,meet(X1,X2)))),
inference(superposition,[],[f179825,f275]) ).
fof(f180442,plain,
! [X2,X3,X0,X1] : meet(join(X2,X1),join(X3,X0)) = meet(join(X2,X1),join(X3,meet(X0,join(X1,X2)))),
inference(superposition,[],[f179825,f4870]) ).
fof(f180452,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f179825,f7452]) ).
fof(f180472,plain,
! [X2,X3,X0,X1] : meet(X2,join(join(X0,X1),X3)) = meet(X2,join(X0,join(X1,meet(X2,X3)))),
inference(superposition,[],[f179825,f6]) ).
fof(f180483,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),X2)) = meet(X0,meet(X0,join(X1,meet(X0,X2)))),
inference(superposition,[],[f179825,f159472]) ).
fof(f180526,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = join(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f66625,f179825]) ).
fof(f180595,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X0,join(X1,X2))) = meet(X0,meet(X3,join(X1,meet(X0,X2)))),
inference(superposition,[],[f138,f179825]) ).
fof(f180597,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X0,join(X1,X2))) = meet(join(X1,meet(X0,X2)),meet(X0,X3)),
inference(superposition,[],[f141,f179825]) ).
fof(f180713,plain,
! [X2,X3,X0,X1] : meet(join(X1,meet(X0,X2)),join(X3,meet(join(X1,meet(X0,X2)),X0))) = join(meet(X3,join(X1,meet(X0,X2))),meet(X0,join(X1,X2))),
inference(superposition,[],[f158974,f179825]) ).
fof(f180757,plain,
! [X2,X3,X0,X1] : meet(join(X1,meet(X0,X2)),join(X3,meet(join(X1,meet(X0,X2)),X0))) = join(meet(X0,join(X1,X2)),meet(X3,join(meet(X0,X2),X1))),
inference(forward_demodulation,[],[f180713,f7951]) ).
fof(f180837,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X0,join(X1,X2))) = meet(X0,meet(X3,join(meet(X0,X2),X1))),
inference(forward_demodulation,[],[f180597,f5371]) ).
fof(f180912,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),X2)) = meet(X0,meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f180483,f180595]) ).
fof(f180923,plain,
! [X2,X3,X0,X1] : meet(X2,join(X0,join(X1,X3))) = meet(X2,join(X0,join(X1,meet(X2,X3)))),
inference(forward_demodulation,[],[f180472,f6]) ).
fof(f180948,plain,
! [X2,X3,X0,X1] : meet(meet(X2,X0),join(X3,X1)) = meet(X2,meet(X0,join(X3,meet(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f180432,f5]) ).
fof(f180951,plain,
! [X2,X3,X0,X1] : meet(X0,join(X3,join(meet(X1,X0),X2))) = meet(X0,join(X3,join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f180429,f179825]) ).
fof(f181006,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),meet(X3,join(meet(X0,X2),X1))) = meet(join(X1,meet(X0,X2)),join(X3,meet(X0,join(meet(X0,X2),X1)))),
inference(forward_demodulation,[],[f180757,f162068]) ).
fof(f181127,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(meet(X1,X0),X2)),
inference(forward_demodulation,[],[f180912,f13]) ).
fof(f181153,plain,
! [X2,X3,X0,X1] : meet(meet(X2,X0),join(X3,X1)) = meet(X2,meet(X0,join(X3,meet(X1,X2)))),
inference(forward_demodulation,[],[f180948,f179825]) ).
fof(f181156,plain,
! [X2,X3,X0,X1] : meet(X0,join(X3,join(X1,X2))) = meet(X0,join(X3,join(meet(X1,X0),X2))),
inference(forward_demodulation,[],[f180951,f180923]) ).
fof(f181180,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),meet(X3,join(meet(X0,X2),X1))) = meet(join(X1,meet(X0,X2)),join(X3,X0)),
inference(forward_demodulation,[],[f181006,f180442]) ).
fof(f181284,plain,
! [X2,X3,X0,X1] : meet(X2,meet(X0,join(X3,X1))) = meet(X2,meet(X0,join(X3,meet(X1,X2)))),
inference(forward_demodulation,[],[f181153,f5]) ).
fof(f181811,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X0,join(X1,X2))) = meet(X0,meet(join(X1,meet(X2,X0)),X3)),
inference(superposition,[],[f22,f180452]) ).
fof(f185431,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f180526,f4872]) ).
fof(f185432,plain,
! [X2,X0,X1] : join(X1,meet(join(X0,X1),X2)) = join(meet(X2,X0),X1),
inference(superposition,[],[f180526,f4870]) ).
fof(f185454,plain,
! [X2,X3,X0,X1] : join(X1,meet(X0,meet(join(X1,X2),X3))) = join(meet(meet(X3,X0),X2),X1),
inference(superposition,[],[f180526,f275]) ).
fof(f185518,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(meet(X2,X3),X1)),meet(X2,X3)) = join(meet(X0,join(meet(X2,X3),X1)),meet(X2,join(meet(X0,X1),meet(X2,X3)))),
inference(superposition,[],[f20534,f180526]) ).
fof(f185867,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(meet(X2,X3),X1)),meet(X2,X3)) = meet(join(meet(X2,X3),meet(X0,X1)),join(X2,X0)),
inference(forward_demodulation,[],[f185518,f181180]) ).
fof(f185923,plain,
! [X2,X3,X0,X1] : join(X1,meet(X0,meet(join(X1,X2),X3))) = join(meet(X3,meet(X0,X2)),X1),
inference(forward_demodulation,[],[f185454,f5]) ).
fof(f186137,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(meet(X2,X3),X1)),meet(X2,X3)) = meet(join(X2,X0),join(meet(X2,X3),meet(X1,X0))),
inference(forward_demodulation,[],[f185867,f8003]) ).
fof(f186321,plain,
! [X2,X3,X0,X1] : meet(join(X2,X0),join(meet(X2,X3),meet(X1,X0))) = join(meet(X2,X3),meet(X0,join(X1,meet(X2,X3)))),
inference(forward_demodulation,[],[f186137,f7951]) ).
fof(f186457,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X2,X3)) = meet(join(X2,X0),join(meet(X2,X3),meet(X1,X0))),
inference(forward_demodulation,[],[f186321,f185431]) ).
fof(f188749,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(X0,meet(join(X1,X0),X2))) = join(meet(X1,X2),meet(X0,join(X1,X2))),
inference(superposition,[],[f2185,f181127]) ).
fof(f188750,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(X0,meet(join(X1,X0),X2))) = join(meet(X2,X1),meet(X0,join(X1,X2))),
inference(superposition,[],[f2095,f181127]) ).
fof(f189117,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(X0,join(X1,X2))) = meet(join(X2,X1),join(meet(X2,X1),X0)),
inference(forward_demodulation,[],[f188750,f185432]) ).
fof(f189118,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X0,join(X1,X2))) = meet(join(X2,X1),join(meet(X2,X1),X0)),
inference(forward_demodulation,[],[f188749,f185432]) ).
fof(f190641,plain,
! [X2,X0,X1] : meet(join(X2,meet(X1,X0)),join(X1,meet(join(meet(X1,X0),X1),X2))) = join(meet(X2,meet(X1,X0)),meet(X1,join(meet(X0,X1),X2))),
inference(superposition,[],[f2222,f272]) ).
fof(f190698,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,join(X1,meet(X0,X1)))),join(X1,meet(join(meet(X0,join(X1,meet(X0,X1))),X1),X2))) = join(meet(X2,meet(X0,join(X1,meet(X0,X1)))),meet(X1,join(meet(X0,X1),X2))),
inference(superposition,[],[f2222,f6671]) ).
fof(f190935,plain,
! [X2,X0,X1] : join(meet(X2,join(meet(X2,X1),X0)),meet(X0,X1)) = join(meet(X2,join(meet(X2,X1),X0)),meet(X0,meet(join(X0,X1),join(X2,meet(join(X1,X2),X0))))),
inference(superposition,[],[f20534,f2222]) ).
fof(f191295,plain,
! [X2,X0,X1] : join(meet(X2,join(meet(X2,X1),X0)),meet(X0,X1)) = join(meet(X2,join(meet(X2,X1),X0)),meet(X0,meet(join(X0,X1),join(X2,join(X1,X2))))),
inference(forward_demodulation,[],[f190935,f181284]) ).
fof(f191518,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,join(X1,meet(X0,X1)))),join(X1,meet(join(meet(X0,join(X1,meet(X0,X1))),X1),X2))) = join(meet(join(meet(X0,X1),X2),X1),meet(meet(X0,join(X1,meet(X0,X1))),X2)),
inference(forward_demodulation,[],[f190698,f8339]) ).
fof(f191567,plain,
! [X2,X0,X1] : meet(join(X2,meet(X1,X0)),join(X1,meet(join(meet(X1,X0),X1),X2))) = meet(X1,join(meet(X0,X2),meet(X1,join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f190641,f160460]) ).
fof(f191854,plain,
! [X2,X0,X1] : join(meet(X2,join(meet(X2,X1),X0)),meet(X0,X1)) = join(meet(X2,join(meet(X2,X1),X0)),meet(X0,join(X2,join(X1,X2)))),
inference(forward_demodulation,[],[f191295,f64723]) ).
fof(f192074,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,join(X1,meet(X0,X1)))),join(X1,meet(join(meet(X0,join(X1,meet(X0,X1))),X1),X2))) = join(meet(X1,join(X2,meet(X0,X1))),meet(meet(X0,join(X1,meet(X0,X1))),X2)),
inference(forward_demodulation,[],[f191518,f8829]) ).
fof(f192120,plain,
! [X2,X0,X1] : meet(join(X2,meet(X1,X0)),join(X1,meet(join(meet(X1,X0),X1),X2))) = meet(X1,join(X2,join(meet(X0,X1),meet(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f191567,f161873]) ).
fof(f192393,plain,
! [X2,X0,X1] : join(meet(X2,join(meet(X2,X1),X0)),meet(X0,X1)) = join(meet(X2,join(meet(X2,X1),X0)),meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f191854,f62]) ).
fof(f192611,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,join(X1,meet(X0,X1)))),join(X1,meet(join(meet(X0,join(X1,meet(X0,X1))),X1),X2))) = join(meet(X1,join(X2,meet(X0,X1))),meet(X0,meet(join(X1,meet(X0,X1)),X2))),
inference(forward_demodulation,[],[f192074,f5]) ).
fof(f192657,plain,
! [X2,X0,X1] : meet(join(X2,meet(X1,X0)),join(X1,meet(join(meet(X1,X0),X1),X2))) = meet(X1,join(X2,join(meet(X0,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f192120,f180923]) ).
fof(f192925,plain,
! [X2,X0,X1] : join(meet(X2,join(meet(X2,X1),X0)),meet(X0,X1)) = join(meet(X0,join(X1,X2)),meet(X2,join(X0,meet(X2,X1)))),
inference(forward_demodulation,[],[f192393,f7951]) ).
fof(f193140,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(join(X2,meet(X0,join(X1,meet(X0,X1)))),join(X1,meet(join(meet(X0,join(X1,meet(X0,X1))),X1),X2))),
inference(forward_demodulation,[],[f192611,f7195]) ).
fof(f193186,plain,
! [X2,X0,X1] : meet(join(X2,meet(X1,X0)),join(X1,meet(join(meet(X1,X0),X1),X2))) = meet(X1,join(X2,join(X0,meet(X0,X2)))),
inference(forward_demodulation,[],[f192657,f181156]) ).
fof(f193432,plain,
! [X2,X0,X1] : join(meet(X2,join(meet(X2,X1),X0)),meet(X0,X1)) = join(meet(X0,X2),join(meet(X2,X1),meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f192925,f159499]) ).
fof(f193638,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(join(X2,meet(X0,join(X1,meet(X0,X1)))),join(X1,meet(meet(X0,join(X1,meet(X0,X1))),join(X2,X1)))),
inference(forward_demodulation,[],[f193140,f176820]) ).
fof(f193683,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X0,X2)))) = meet(join(X2,meet(X1,X0)),join(X1,meet(join(meet(X1,X0),X1),X2))),
inference(forward_demodulation,[],[f193186,f27183]) ).
fof(f193911,plain,
! [X2,X0,X1] : join(meet(X2,join(meet(X2,X1),X0)),meet(X0,X1)) = join(meet(X0,join(X1,X2)),meet(X2,X1)),
inference(forward_demodulation,[],[f193432,f20359]) ).
fof(f194088,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(join(X2,meet(X0,join(X1,meet(X0,X1)))),join(meet(meet(X0,join(X1,meet(X0,X1))),X2),X1)),
inference(forward_demodulation,[],[f193638,f185431]) ).
fof(f194119,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X0,X2)))) = meet(join(X2,meet(X1,X0)),join(X1,meet(meet(X1,X0),join(X2,X1)))),
inference(forward_demodulation,[],[f193683,f176820]) ).
fof(f194317,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(X0,join(X2,X1))) = join(meet(X2,join(meet(X2,X1),X0)),meet(X0,X1)),
inference(forward_demodulation,[],[f193911,f7951]) ).
fof(f194475,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(join(X2,meet(X0,join(X1,meet(X0,X1)))),join(X1,meet(meet(X0,join(X1,meet(X0,X1))),X2))),
inference(forward_demodulation,[],[f194088,f4872]) ).
fof(f194499,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X0,X2)))) = meet(join(X2,meet(X1,X0)),join(meet(meet(X1,X0),X2),X1)),
inference(forward_demodulation,[],[f194119,f185431]) ).
fof(f194653,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X0,meet(X2,X1)))) = join(meet(X2,X1),meet(X0,join(X2,X1))),
inference(forward_demodulation,[],[f194317,f7951]) ).
fof(f194795,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(join(X2,meet(X0,join(X1,meet(X0,X1)))),join(X1,meet(X0,meet(join(X1,meet(X0,X1)),X2)))),
inference(forward_demodulation,[],[f194475,f5]) ).
fof(f194814,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X0,X2)))) = meet(join(X2,meet(X1,X0)),join(X1,meet(meet(X1,X0),X2))),
inference(forward_demodulation,[],[f194499,f4872]) ).
fof(f194957,plain,
! [X2,X0,X1] : meet(join(X1,X2),join(meet(X1,X2),X0)) = join(meet(X0,X1),meet(X2,join(X0,meet(X2,X1)))),
inference(forward_demodulation,[],[f194653,f189118]) ).
fof(f195091,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(join(X2,meet(X0,join(X1,meet(X0,X1)))),join(meet(X2,meet(X0,meet(X0,X1))),X1)),
inference(forward_demodulation,[],[f194795,f185923]) ).
fof(f195110,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X0,X2)))) = meet(join(X2,meet(X1,X0)),join(X1,meet(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f194814,f5]) ).
fof(f195230,plain,
! [X2,X0,X1] : meet(join(X1,X2),join(meet(X1,X2),X0)) = join(meet(X0,X1),meet(X2,join(X0,X1))),
inference(forward_demodulation,[],[f194957,f179825]) ).
fof(f195356,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(join(X2,meet(X0,join(X1,meet(X0,X1)))),join(X1,meet(X2,meet(X0,meet(X0,X1))))),
inference(forward_demodulation,[],[f195091,f4872]) ).
fof(f195374,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X0,X2)))) = meet(join(X2,meet(X1,X0)),meet(X1,join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f195110,f27183]) ).
fof(f195579,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(join(X2,meet(X0,join(X1,meet(X0,X1)))),meet(X1,join(meet(X2,meet(X0,X0)),X1))),
inference(forward_demodulation,[],[f195356,f39548]) ).
fof(f195597,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X0,X2)))) = meet(X1,meet(join(X1,meet(X0,X2)),join(meet(X1,X0),X2))),
inference(forward_demodulation,[],[f195374,f5371]) ).
fof(f195769,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(meet(X1,join(meet(X2,meet(X0,X0)),X1)),join(X2,meet(join(X1,meet(X0,X1)),X0))),
inference(forward_demodulation,[],[f195579,f8003]) ).
fof(f195787,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X0,X2)))) = meet(join(X1,meet(X0,X2)),meet(X1,join(X2,X0))),
inference(forward_demodulation,[],[f195597,f180837]) ).
fof(f195938,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(X1,meet(join(meet(X2,meet(X0,X0)),X1),join(X2,meet(join(X1,meet(X0,X1)),X0)))),
inference(forward_demodulation,[],[f195769,f5]) ).
fof(f195955,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X0,X2)))) = meet(meet(X1,join(X2,X0)),join(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f195787,f8003]) ).
fof(f196077,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(X1,meet(join(meet(X2,meet(X0,X0)),X1),join(X2,meet(X0,join(X1,meet(X0,X1)))))),
inference(forward_demodulation,[],[f195938,f8005]) ).
fof(f196093,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X0,X2)))) = meet(X1,meet(join(X2,X0),join(X1,meet(X2,X0)))),
inference(forward_demodulation,[],[f195955,f5]) ).
fof(f196198,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(X1,meet(join(meet(X2,meet(X0,X0)),X1),join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f196077,f6907]) ).
fof(f196213,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,meet(join(X2,X0),join(X1,meet(X2,X0)))),
inference(forward_demodulation,[],[f196093,f4376]) ).
fof(f196311,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X2,meet(X0,X0)),X1))),
inference(forward_demodulation,[],[f196198,f1035]) ).
fof(f196404,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(join(meet(X2,meet(X0,X0)),X1),meet(X1,join(X2,X0))),
inference(forward_demodulation,[],[f196311,f181811]) ).
fof(f196480,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(X1,meet(join(X2,X0),join(X1,meet(X2,meet(X0,X0))))),
inference(forward_demodulation,[],[f196404,f5371]) ).
fof(f196541,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))) = meet(X1,meet(join(X2,X0),join(X1,meet(X2,X0)))),
inference(forward_demodulation,[],[f196480,f1]) ).
fof(f196598,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X1,join(X2,meet(X0,X1))),meet(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f196541,f196213]) ).
fof(f196650,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X2,meet(X0,X1)),meet(X1,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f196598,f7951]) ).
fof(f196695,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(join(X2,meet(X0,X1)),join(meet(X2,meet(X0,X1)),X1)),
inference(forward_demodulation,[],[f196650,f189117]) ).
fof(f196732,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X1,X2),meet(meet(X0,X1),join(X1,X2))),
inference(forward_demodulation,[],[f196695,f195230]) ).
fof(f196764,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(join(X2,X1),join(meet(X2,X1),meet(X0,X1))),
inference(forward_demodulation,[],[f196732,f189118]) ).
fof(f196791,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X1,X0),meet(X2,X1)),
inference(forward_demodulation,[],[f196764,f186457]) ).
fof(f197223,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,X2),meet(X0,X1)),
inference(superposition,[],[f7450,f196791]) ).
fof(f208847,plain,
meet(a,join(b,c)) != meet(a,join(c,b)),
inference(superposition,[],[f12,f197223]) ).
fof(f209281,plain,
$false,
inference(forward_subsumption_resolution,[],[f208847,f4872]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT020-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n020.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 13:57:49 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.31/2.30 % (3398527)Will run a generic schedule for satisfiability detection.
% 13.31/2.30 % (3398536)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2675654179:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.31/2.30 % (3398533)% WARNING: option uhcvi not known.
% 13.31/2.30 % (3398532)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=256798325_2999 on theBenchmark for (2999ds/0Mi)
% 13.31/2.30 % (3398533)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=861114052:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.31/2.30 % (3398534)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3698246126:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.31/2.30 % (3398535)dis+10_1_sil=32000:sp=arity:random_seed=3634593017:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.31/2.30 % (3398538)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1134135130:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.31/2.30 % (3398537)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4075520302:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.31/2.30 % TRYING [1]
% 13.31/2.30 % TRYING [2]
% 13.31/2.30 % TRYING [3]
% 13.31/2.30 % TRYING [4]
% 13.31/2.30 % (3398536)Instruction limit reached!
% 13.31/2.30 % (3398536)------------------------------
% 13.31/2.30 % (3398536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.31/2.30 % (3398536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.31/2.30 % (3398536)CaDiCaL version: 2.1.3
% 13.31/2.30 % (3398536)Termination reason: Instruction limit
% 13.31/2.30 % (3398536)Termination phase: Saturation
% 13.31/2.30 % (3398536)Time elapsed: 0.036 s
% 13.31/2.30 % (3398536)Peak memory usage: 12 MB
% 13.31/2.30 % (3398536)Instructions burned: 119 (million)
% 13.31/2.30 % (3398546)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1330323147:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.31/2.30 % TRYING [1]
% 13.31/2.30 % TRYING [2]
% 13.31/2.30 % TRYING [3]
% 13.31/2.30 % TRYING [4]
% 13.31/2.30 % (3398535)Instruction limit reached!
% 13.31/2.30 % (3398535)------------------------------
% 13.31/2.30 % (3398535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.31/2.30 % (3398535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.31/2.31 % (3398535)CaDiCaL version: 2.1.3
% 13.31/2.31 % (3398535)Termination reason: Instruction limit
% 13.31/2.31 % (3398535)Termination phase: Saturation
% 13.31/2.31 % (3398535)Time elapsed: 0.056 s
% 13.31/2.31 % (3398535)Peak memory usage: 12 MB
% 13.31/2.31 % (3398535)Instructions burned: 104 (million)
% 13.31/2.31 % TRYING [5]
% 13.31/2.31 % (3398537)Instruction limit reached!
% 13.31/2.31 % (3398537)------------------------------
% 13.31/2.31 % (3398537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.31/2.31 % (3398537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.31/2.31 % (3398537)CaDiCaL version: 2.1.3
% 13.31/2.31 % (3398537)Termination reason: Instruction limit
% 13.31/2.31 % (3398537)Termination phase: Saturation
% 13.31/2.31 % (3398537)Time elapsed: 0.075 s
% 13.31/2.31 % (3398537)Peak memory usage: 12 MB
% 13.31/2.31 % (3398537)Instructions burned: 135 (million)
% 13.31/2.31 % (3398548)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2934939423:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 13.31/2.31 % TRYING [5]
% 13.31/2.31 % (3398538)Instruction limit reached!
% 13.31/2.31 % (3398538)------------------------------
% 13.31/2.31 % (3398538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.31/2.31 % (3398538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.31/2.31 % (3398538)CaDiCaL version: 2.1.3
% 13.31/2.31 % (3398538)Termination reason: Instruction limit
% 13.31/2.31 % (3398538)Termination phase: Saturation
% 13.31/2.31 % (3398538)Time elapsed: 0.091 s
% 13.31/2.31 % (3398538)Peak memory usage: 12 MB
% 13.31/2.31 % (3398538)Instructions burned: 160 (million)
% 13.31/2.31 % (3398550)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2331924366:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.31/2.31 % (3398551)ott-21_1_sil=16000:fs=off:random_seed=4220596003:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.31/2.31 % (3398548)Instruction limit reached!
% 13.31/2.31 % (3398548)------------------------------
% 13.31/2.31 % (3398548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.68/6.34 % (3398548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.68/6.34 % (3398548)CaDiCaL version: 2.1.3
% 41.68/6.34 % (3398548)Termination reason: Instruction limit
% 41.68/6.34 % (3398548)Termination phase: Saturation
% 41.68/6.34 % (3398548)Time elapsed: 0.081 s
% 41.68/6.34 % (3398548)Peak memory usage: 12 MB
% 41.68/6.34 % (3398548)Instructions burned: 131 (million)
% 41.68/6.34 % (3398554)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3285501832:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 41.68/6.34 % (3398551)Instruction limit reached!
% 41.68/6.34 % (3398551)------------------------------
% 41.68/6.34 % (3398551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.68/6.34 % (3398551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.68/6.34 % (3398551)CaDiCaL version: 2.1.3
% 41.68/6.34 % (3398551)Termination reason: Instruction limit
% 41.68/6.34 % (3398551)Termination phase: Saturation
% 41.68/6.34 % (3398551)Time elapsed: 0.077 s
% 41.68/6.34 % (3398551)Peak memory usage: 11 MB
% 41.68/6.34 % (3398551)Instructions burned: 181 (million)
% 41.68/6.34 % (3398556)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3881162031:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 41.68/6.34 % TRYING [1]
% 41.68/6.34 % TRYING [2]
% 41.68/6.34 % TRYING [3]
% 41.68/6.34 % TRYING [6]
% 41.68/6.34 % TRYING [4]
% 41.68/6.34 % (3398546)Instruction limit reached!
% 41.68/6.34 % (3398546)------------------------------
% 41.68/6.34 % (3398546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.68/6.34 % (3398546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.68/6.34 % (3398546)CaDiCaL version: 2.1.3
% 41.68/6.34 % (3398546)Termination reason: Instruction limit
% 41.68/6.34 % (3398546)Termination phase: Finite model building constraint generation
% 41.68/6.34 % (3398546)Time elapsed: 0.199 s
% 41.68/6.34 % (3398546)Peak memory usage: 26 MB
% 41.68/6.34 % (3398546)Instructions burned: 721 (million)
% 41.68/6.34 % (3398558)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=177996861:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 41.68/6.34 % TRYING [6]
% 41.68/6.34 % TRYING [5]
% 41.68/6.34 % (3398554)Instruction limit reached!
% 41.68/6.34 % (3398554)------------------------------
% 41.68/6.34 % (3398554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.68/6.34 % (3398554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.68/6.34 % (3398554)CaDiCaL version: 2.1.3
% 41.68/6.34 % (3398554)Termination reason: Instruction limit
% 41.68/6.34 % (3398554)Termination phase: Saturation
% 41.68/6.34 % (3398554)Time elapsed: 0.240 s
% 41.68/6.34 % (3398554)Peak memory usage: 15 MB
% 41.68/6.34 % (3398554)Instructions burned: 478 (million)
% 41.68/6.34 % (3398550)Instruction limit reached!
% 41.68/6.34 % (3398550)------------------------------
% 41.68/6.34 % (3398550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.68/6.34 % (3398550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.68/6.34 % (3398550)CaDiCaL version: 2.1.3
% 41.68/6.34 % (3398550)Termination reason: Instruction limit
% 41.68/6.34 % (3398550)Termination phase: Saturation
% 41.68/6.34 % (3398550)Time elapsed: 0.329 s
% 41.68/6.34 % (3398550)Peak memory usage: 16 MB
% 41.68/6.34 % (3398550)Instructions burned: 685 (million)
% 41.68/6.34 % (3398560)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1038366257:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 41.68/6.34 % (3398561)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=246446988:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 41.68/6.34 % (3398556)Instruction limit reached!
% 41.68/6.34 % (3398556)------------------------------
% 41.68/6.34 % (3398556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.68/6.34 % (3398556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.68/6.34 % (3398556)CaDiCaL version: 2.1.3
% 41.68/6.34 % (3398556)Termination reason: Instruction limit
% 41.68/6.34 % (3398556)Termination phase: Finite model building constraint generation
% 41.68/6.34 % (3398556)Time elapsed: 0.340 s
% 41.68/6.34 % (3398556)Peak memory usage: 21 MB
% 41.68/6.34 % (3398556)Instructions burned: 865 (million)
% 41.68/6.34 % (3398564)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3214256881:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 41.68/6.34 % (3398558)Instruction limit reached!
% 90.60/13.21 % (3398558)------------------------------
% 90.60/13.21 % (3398558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.60/13.21 % (3398558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.60/13.21 % (3398558)CaDiCaL version: 2.1.3
% 90.60/13.21 % (3398558)Termination reason: Instruction limit
% 90.60/13.21 % (3398558)Termination phase: Saturation
% 90.60/13.21 % (3398558)Time elapsed: 0.383 s
% 90.60/13.21 % (3398558)Peak memory usage: 22 MB
% 90.60/13.21 % (3398558)Instructions burned: 1180 (million)
% 90.60/13.21 % (3398566)fmb+10_1_sil=64000:random_seed=2337126164:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 90.60/13.21 % TRYING [1]
% 90.60/13.21 % TRYING [2]
% 90.60/13.21 % TRYING [3]
% 90.60/13.21 % TRYING [4]
% 90.60/13.21 % TRYING [14]
% 90.60/13.21 % TRYING [5]
% 90.60/13.21 % (3398560)Instruction limit reached!
% 90.60/13.21 % (3398560)------------------------------
% 90.60/13.21 % (3398560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.60/13.21 % (3398560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.60/13.21 % (3398560)CaDiCaL version: 2.1.3
% 90.60/13.21 % (3398560)Termination reason: Instruction limit
% 90.60/13.21 % (3398560)Termination phase: Finite model building constraint generation
% 90.60/13.21 % (3398560)Time elapsed: 0.367 s
% 90.60/13.21 % (3398560)Peak memory usage: 91 MB
% 90.60/13.21 % (3398560)Instructions burned: 892 (million)
% 90.60/13.21 % (3398561)Instruction limit reached!
% 90.60/13.21 % (3398561)------------------------------
% 90.60/13.21 % (3398561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.60/13.21 % (3398561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.60/13.21 % (3398561)CaDiCaL version: 2.1.3
% 90.60/13.21 % (3398561)Termination reason: Instruction limit
% 90.60/13.21 % (3398561)Termination phase: Saturation
% 90.60/13.21 % (3398561)Time elapsed: 0.362 s
% 90.60/13.21 % (3398561)Peak memory usage: 16 MB
% 90.60/13.21 % (3398561)Instructions burned: 692 (million)
% 90.60/13.21 % (3398568)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3959930794:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 90.60/13.21 % TRYING [20]
% 90.60/13.21 % TRYING [6]
% 90.60/13.21 % (3398569)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3607261697:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 90.60/13.21 % TRYING [8]
% 90.60/13.21 % TRYING [7]
% 90.60/13.21 % (3398564)Instruction limit reached!
% 90.60/13.21 % (3398564)------------------------------
% 90.60/13.21 % (3398564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.60/13.21 % (3398564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.60/13.21 % (3398564)CaDiCaL version: 2.1.3
% 90.60/13.21 % (3398564)Termination reason: Instruction limit
% 90.60/13.21 % (3398564)Termination phase: Saturation
% 90.60/13.21 % (3398564)Time elapsed: 0.441 s
% 90.60/13.21 % (3398564)Peak memory usage: 18 MB
% 90.60/13.21 % (3398564)Instructions burned: 879 (million)
% 90.60/13.21 % (3398572)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2363767975:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 90.60/13.21 % (3398569)Instruction limit reached!
% 90.60/13.21 % (3398569)------------------------------
% 90.60/13.21 % (3398569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.60/13.21 % (3398569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.60/13.21 % (3398569)CaDiCaL version: 2.1.3
% 90.60/13.21 % (3398569)Termination reason: Instruction limit
% 90.60/13.21 % (3398569)Termination phase: Finite model building constraint generation
% 90.60/13.21 % (3398569)Time elapsed: 0.346 s
% 90.60/13.21 % (3398569)Peak memory usage: 76 MB
% 90.60/13.21 % (3398569)Instructions burned: 921 (million)
% 90.60/13.21 % (3398574)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=836291349:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 90.60/13.21 % TRYING [7]
% 90.60/13.21 % (3398574)Instruction limit reached!
% 90.60/13.21 % (3398574)------------------------------
% 90.60/13.21 % (3398574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.60/13.21 % (3398574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.60/13.21 % (3398574)CaDiCaL version: 2.1.3
% 90.60/13.21 % (3398574)Termination reason: Instruction limit
% 90.60/13.21 % (3398574)Termination phase: Saturation
% 90.60/13.21 % (3398574)Time elapsed: 0.615 s
% 90.60/13.21 % (3398574)Peak memory usage: 20 MB
% 90.60/13.21 % (3398574)Instructions burned: 1475 (million)
% 90.60/13.21 % (3398576)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=253492104:i=6324_2981 on theBenchmark for (2981ds/6324Mi)
% 236.01/33.70 % TRYING [77]
% 236.01/33.70 % TRYING [8]
% 236.01/33.70 % TRYING [8]
% 236.01/33.70 % (3398572)Instruction limit reached!
% 236.01/33.70 % (3398572)------------------------------
% 236.01/33.70 % (3398572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 236.01/33.70 % (3398572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.01/33.70 % (3398572)CaDiCaL version: 2.1.3
% 236.01/33.70 % (3398572)Termination reason: Instruction limit
% 236.01/33.70 % (3398572)Termination phase: Saturation
% 236.01/33.70 % (3398572)Time elapsed: 2.707 s
% 236.01/33.70 % (3398572)Peak memory usage: 54 MB
% 236.01/33.70 % (3398572)Instructions burned: 5131 (million)
% 236.01/33.70 % (3398578)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=901564792:fmbsr=2.30978:i=2174_2962 on theBenchmark for (2962ds/2174Mi)
% 236.01/33.70 % TRYING [16]
% 236.01/33.70 % (3398576)Instruction limit reached!
% 236.01/33.70 % (3398576)------------------------------
% 236.01/33.70 % (3398576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 236.01/33.70 % (3398576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.01/33.70 % (3398576)CaDiCaL version: 2.1.3
% 236.01/33.70 % (3398576)Termination reason: Instruction limit
% 236.01/33.70 % (3398576)Termination phase: Finite model building constraint generation
% 236.01/33.70 % (3398576)Time elapsed: 2.323 s
% 236.01/33.70 % (3398576)Peak memory usage: 429 MB
% 236.01/33.70 % (3398576)Instructions burned: 6325 (million)
% 236.01/33.70 % (3398580)ott-2_1_sil=16000:newcnf=on:random_seed=4117089053:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 236.01/33.70 % (3398568)Instruction limit reached!
% 236.01/33.70 % (3398568)------------------------------
% 236.01/33.70 % (3398568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 236.01/33.70 % (3398568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.01/33.70 % (3398568)CaDiCaL version: 2.1.3
% 236.01/33.70 % (3398568)Termination reason: Instruction limit
% 236.01/33.70 % (3398568)Termination phase: Finite model building constraint generation
% 236.01/33.70 % (3398568)Time elapsed: 3.473 s
% 236.01/33.70 % (3398568)Peak memory usage: 672 MB
% 236.01/33.70 % (3398568)Instructions burned: 9516 (million)
% 236.01/33.70 % (3398582)ott+10_1_sil=32000:tgt=ground:random_seed=4047982764:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 236.01/33.70 % (3398578)Instruction limit reached!
% 236.01/33.70 % (3398578)------------------------------
% 236.01/33.70 % (3398578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 236.01/33.70 % (3398578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.01/33.70 % (3398578)CaDiCaL version: 2.1.3
% 236.01/33.70 % (3398578)Termination reason: Instruction limit
% 236.01/33.70 % (3398578)Termination phase: Finite model building constraint generation
% 236.01/33.70 % (3398578)Time elapsed: 0.736 s
% 236.01/33.70 % (3398578)Peak memory usage: 134 MB
% 236.01/33.70 % (3398578)Instructions burned: 2177 (million)
% 236.01/33.70 % (3398584)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1003535194:i=54282_2954 on theBenchmark for (2954ds/54282Mi)
% 236.01/33.70 % TRYING [1]
% 236.01/33.70 % TRYING [2]
% 236.01/33.70 % TRYING [3]
% 236.01/33.70 % TRYING [4]
% 236.01/33.70 % TRYING [5]
% 236.01/33.70 % (3398580)Instruction limit reached!
% 236.01/33.70 % (3398580)------------------------------
% 236.01/33.70 % (3398580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 236.01/33.70 % (3398580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.01/33.70 % (3398580)CaDiCaL version: 2.1.3
% 236.01/33.70 % (3398580)Termination reason: Instruction limit
% 236.01/33.70 % (3398580)Termination phase: Saturation
% 236.01/33.70 % (3398580)Time elapsed: 0.516 s
% 236.01/33.70 % (3398580)Peak memory usage: 18 MB
% 236.01/33.70 % (3398580)Instructions burned: 870 (million)
% 236.01/33.70 % (3398586)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=708971226:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 236.01/33.70 % TRYING [6]
% 236.01/33.70 % TRYING [9]
% 236.01/33.70 % TRYING [7]
% 236.01/33.70 % (3398566)Instruction limit reached!
% 236.01/33.70 % (3398566)------------------------------
% 236.01/33.70 % (3398566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 236.01/33.70 % (3398566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.01/33.70 % (3398566)CaDiCaL version: 2.1.3
% 236.01/33.70 % (3398566)Termination reason: Instruction limit
% 236.01/33.70 % (3398566)Termination phase: Finite model building SAT solving
% 236.01/33.70 % (3398566)Time elapsed: 5.236 s
% 236.01/33.70 % (3398566)Peak memory usage: 175 MB
% 236.01/33.70 % (3398566)Instructions burned: 22064 (million)
% 242.81/38.19 % (3398588)dis+21_1_sil=32000:sas=cadical:random_seed=3224420211:i=3773:amm=off_2940 on theBenchmark for (2940ds/3773Mi)
% 242.81/38.19 % (3398586)Instruction limit reached!
% 242.81/38.19 % (3398586)------------------------------
% 242.81/38.19 % (3398586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 242.81/38.19 % (3398586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.81/38.19 % (3398586)CaDiCaL version: 2.1.3
% 242.81/38.19 % (3398586)Termination reason: Instruction limit
% 242.81/38.19 % (3398586)Termination phase: Saturation
% 242.81/38.19 % (3398586)Time elapsed: 1.802 s
% 242.81/38.19 % (3398586)Peak memory usage: 40 MB
% 242.81/38.19 % (3398586)Instructions burned: 3512 (million)
% 242.81/38.19 % (3398590)ott+11_1_sil=16000:gs=on:random_seed=2558341265:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2933 on theBenchmark for (2933ds/2251Mi)
% 242.81/38.19 % (3398588)Instruction limit reached!
% 242.81/38.19 % (3398588)------------------------------
% 242.81/38.19 % (3398588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 242.81/38.19 % (3398588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.81/38.19 % (3398588)CaDiCaL version: 2.1.3
% 242.81/38.19 % (3398588)Termination reason: Instruction limit
% 242.81/38.19 % (3398588)Termination phase: Saturation
% 242.81/38.19 % (3398588)Time elapsed: 1.043 s
% 242.81/38.19 % (3398588)Peak memory usage: 42 MB
% 242.81/38.19 % (3398588)Instructions burned: 3773 (million)
% 242.81/38.19 % (3398592)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2218806375:fmbsr=1.6:i=67534_2930 on theBenchmark for (2930ds/67534Mi)
% 242.81/38.19 % TRYING [7]
% 242.81/38.19 % TRYING [8]
% 242.81/38.19 % TRYING [9]
% 242.81/38.19 % (3398582)Instruction limit reached!
% 242.81/38.19 % (3398582)------------------------------
% 242.81/38.19 % (3398582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 242.81/38.19 % (3398582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.81/38.19 % (3398582)CaDiCaL version: 2.1.3
% 242.81/38.19 % (3398582)Termination reason: Instruction limit
% 242.81/38.19 % (3398582)Termination phase: Saturation
% 242.81/38.19 % (3398582)Time elapsed: 3.492 s
% 242.81/38.19 % (3398582)Peak memory usage: 56 MB
% 242.81/38.19 % (3398582)Instructions burned: 5115 (million)
% 242.81/38.19 % (3398594)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=916837050:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2920 on theBenchmark for (2920ds/4591Mi)
% 242.81/38.19 % (3398590)Instruction limit reached!
% 242.81/38.19 % (3398590)------------------------------
% 242.81/38.19 % (3398590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 242.81/38.19 % (3398590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.81/38.19 % (3398590)CaDiCaL version: 2.1.3
% 242.81/38.19 % (3398590)Termination reason: Instruction limit
% 242.81/38.19 % (3398590)Termination phase: Saturation
% 242.81/38.19 % (3398590)Time elapsed: 1.379 s
% 242.81/38.19 % (3398590)Peak memory usage: 27 MB
% 242.81/38.19 % (3398590)Instructions burned: 2252 (million)
% 242.81/38.19 % (3398596)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3476474079:i=29340_2919 on theBenchmark for (2919ds/29340Mi)
% 242.81/38.19 % TRYING [8]
% 242.81/38.19 % (3398594)Instruction limit reached!
% 242.81/38.19 % (3398594)------------------------------
% 242.81/38.19 % (3398594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 242.81/38.19 % (3398594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.81/38.19 % (3398594)CaDiCaL version: 2.1.3
% 242.81/38.19 % (3398594)Termination reason: Instruction limit
% 242.81/38.19 % (3398594)Termination phase: Saturation
% 242.81/38.19 % (3398594)Time elapsed: 2.077 s
% 242.81/38.19 % (3398594)Peak memory usage: 37 MB
% 242.81/38.19 % (3398594)Instructions burned: 4593 (million)
% 242.81/38.19 % (3398598)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3984147983:i=5211_2899 on theBenchmark for (2899ds/5211Mi)
% 242.81/38.19 % TRYING [9]
% 242.81/38.19 % TRYING [9]
% 242.81/38.19 % (3398598)Instruction limit reached!
% 242.81/38.19 % (3398598)------------------------------
% 242.81/38.19 % (3398598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 242.81/38.19 % (3398598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.81/38.19 % (3398598)CaDiCaL version: 2.1.3
% 242.81/38.19 % (3398598)Termination reason: Instruction limit
% 242.81/38.19 % (3398598)Termination phase: Saturation
% 242.81/38.19 % (3398598)Time elapsed: 2.721 s
% 242.81/38.19 % (3398598)Peak memory usage: 49 MB
% 242.81/38.19 % (3398598)Instructions burned: 5211 (million)
% 242.81/38.19 % (3398600)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1929923526:i=5497:nm=2_2872 on theBenchmark for (2872ds/5497Mi)
% 242.81/38.19 % TRYING [17]
% 242.81/38.19 % (3398600)Instruction limit reached!
% 242.81/38.19 % (3398600)------------------------------
% 242.81/38.19 % (3398600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 242.81/38.19 % (3398600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.81/38.19 % (3398600)CaDiCaL version: 2.1.3
% 242.81/38.19 % (3398600)Termination reason: Instruction limit
% 242.81/38.19 % (3398600)Termination phase: Finite model building constraint generation
% 242.81/38.19 % (3398600)Time elapsed: 1.971 s
% 242.81/38.19 % (3398600)Peak memory usage: 391 MB
% 242.81/38.19 % (3398600)Instructions burned: 5499 (million)
% 242.81/38.19 % (3398603)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=419587215:fmbsr=2:i=46332_2851 on theBenchmark for (2851ds/46332Mi)
% 242.81/38.19 % TRYING [15]
% 242.81/38.19 % TRYING [10]
% 242.81/38.19 % (3398596)Instruction limit reached!
% 242.81/38.19 % (3398596)------------------------------
% 242.81/38.19 % (3398596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 242.81/38.19 % (3398596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.81/38.19 % (3398596)CaDiCaL version: 2.1.3
% 242.81/38.19 % (3398596)Termination reason: Instruction limit
% 242.81/38.19 % (3398596)Termination phase: Saturation
% 242.81/38.19 % (3398596)Time elapsed: 14.555 s
% 242.81/38.19 % (3398596)Peak memory usage: 120 MB
% 242.81/38.19 % (3398596)Instructions burned: 29340 (million)
% 242.81/38.19 % (3398605)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1013243906:i=14071_2773 on theBenchmark for (2773ds/14071Mi)
% 242.81/38.19 % TRYING [12]
% 242.81/38.19 % (3398592)Instruction limit reached!
% 242.81/38.19 % (3398592)------------------------------
% 242.81/38.19 % (3398592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 242.81/38.19 % (3398592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.81/38.19 % (3398592)CaDiCaL version: 2.1.3
% 242.81/38.19 % (3398592)Termination reason: Instruction limit
% 242.81/38.19 % (3398592)Termination phase: Finite model building SAT solving
% 242.81/38.19 % (3398592)Time elapsed: 20.969 s
% 242.81/38.19 % (3398592)Peak memory usage: 314 MB
% 242.81/38.19 % (3398592)Instructions burned: 67535 (million)
% 242.81/38.19 % (3398607)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1629546434:i=22565:add=on:rawr=on_2720 on theBenchmark for (2720ds/22565Mi)
% 242.81/38.19 % (3398605)Instruction limit reached!
% 242.81/38.19 % (3398605)------------------------------
% 242.81/38.19 % (3398605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 242.81/38.19 % (3398605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.81/38.19 % (3398605)CaDiCaL version: 2.1.3
% 242.81/38.19 % (3398605)Termination reason: Instruction limit
% 242.81/38.19 % (3398605)Termination phase: Finite model building SAT solving
% 242.81/38.19 % (3398605)Time elapsed: 6.567 s
% 242.81/38.19 % (3398605)Peak memory usage: 820 MB
% 242.81/38.19 % (3398605)Instructions burned: 14072 (million)
% 242.81/38.19 % (3398742)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1856163385:i=8173:av=off_2706 on theBenchmark for (2706ds/8173Mi)
% 242.81/38.19 % (3398534)Instruction limit reached!
% 242.81/38.19 % (3398534)------------------------------
% 242.81/38.19 % (3398534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 242.81/38.19 % (3398534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.81/38.19 % (3398534)CaDiCaL version: 2.1.3
% 242.81/38.19 % (3398534)Termination reason: Instruction limit
% 242.81/38.19 % (3398534)Termination phase: Saturation
% 242.81/38.19 % (3398534)Time elapsed: 30.857 s
% 242.81/38.19 % (3398534)Peak memory usage: 209 MB
% 242.81/38.19 % (3398534)Instructions burned: 88027 (million)
% 242.81/38.19 % (3398763)dis+10_16:1_sil=16000:random_seed=908353232:i=9155:fsr=off_2690 on theBenchmark for (2690ds/9155Mi)
% 242.81/38.19 % (3398607)Instruction limit reached!
% 242.81/38.19 % (3398607)------------------------------
% 242.81/38.19 % (3398607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 242.81/38.19 % (3398607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.81/38.19 % (3398607)CaDiCaL version: 2.1.3
% 242.81/38.19 % (3398607)Termination reason: Instruction limit
% 242.81/38.19 % (3398607)Termination phase: Saturation
% 242.81/38.19 % (3398607)Time elapsed: 5.271 s
% 242.81/38.19 % (3398607)Peak memory usage: 105 MB
% 242.81/38.19 % (3398607)Instructions burned: 22569 (million)
% 242.81/38.19 % (3398765)ott-3_8_sil=64000:random_seed=3645196625:i=20139:bs=on_2667 on theBenchmark for (2667ds/20139Mi)
% 242.81/38.19 % (3398742)Instruction limit reached!
% 242.81/38.19 % (3398742)------------------------------
% 242.81/38.19 % (3398742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 242.81/38.19 % (3398742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.81/38.19 % (3398742)CaDiCaL version: 2.1.3
% 242.81/38.19 % (3398742)Termination reason: Instruction limit
% 242.81/38.19 % (3398742)Termination phase: Saturation
% 242.81/38.19 % (3398742)Time elapsed: 4.870 s
% 242.81/38.19 % (3398742)Peak memory usage: 56 MB
% 242.81/38.19 % (3398742)Instructions burned: 8175 (million)
% 242.81/38.19 % (3398767)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3129118505:fmbsr=2:i=32576_2657 on theBenchmark for (2657ds/32576Mi)
% 242.81/38.19 % TRYING [9]
% 242.81/38.19 % TRYING [10]
% 242.81/38.19 % (3398763)Instruction limit reached!
% 242.81/38.19 % (3398763)------------------------------
% 242.81/38.19 % (3398763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 242.81/38.19 % (3398763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.81/38.19 % (3398763)CaDiCaL version: 2.1.3
% 242.81/38.19 % (3398763)Termination reason: Instruction limit
% 242.81/38.19 % (3398763)Termination phase: Saturation
% 242.81/38.19 % (3398763)Time elapsed: 4.950 s
% 242.81/38.19 % (3398763)Peak memory usage: 83 MB
% 242.81/38.19 % (3398763)Instructions burned: 9155 (million)
% 242.81/38.19 % (3398769)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3419571878:i=11404_2641 on theBenchmark for (2641ds/11404Mi)
% 242.81/38.19 % (3398765) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3398527-3398765"...
% 242.81/38.19 % (3398765)...printing done.
% 242.81/38.19 % (3398765)Refutation found. Thanks to Tanya!
% 242.81/38.19 % SZS status Unsatisfiable for theBenchmark
% 242.81/38.19 % SZS output start Proof for theBenchmark
% See solution above
% 266.05/38.20 % (3398765)------------------------------
% 266.05/38.20 % (3398765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 266.05/38.20 % (3398765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 266.05/38.20 % (3398765)CaDiCaL version: 2.1.3
% 266.05/38.20 % (3398765)Termination reason: Refutation
% 266.05/38.20 % (3398765)Time elapsed: 4.097 s
% 266.05/38.20 % (3398765)Peak memory usage: 69 MB
% 266.05/38.20 % (3398765)Instructions burned: 12557 (million)
% 266.05/38.20 % (3398527)Success in time 37.76 s
% 266.05/38.20 % Vampire exiting
%------------------------------------------------------------------------------