use(diamond_pbeta).
use(comp_th).

comp_th(S,T).

dia_pbeta(s,t,x) -> [].

top_predicates_precedence([comp_th,dia_pbeta]).

option([var_overlaps(off),search_depth(0)]).
:-sarp(+[15]),saci([2]).



/*
Proof:
======

   1 : dia_pbeta(A,B,C)==(pbeta(A,B)and pbeta(A,C)=>?D.(pbeta(B,D)and pbeta(C,D))) [input]
   2 : comp_th(A,B)==(pbeta(A,B)=>pbeta(B,cd(A)))                       [input]
   3 : comp_th(A,B)                                                     [input]
   4 : dia_pbeta(s,t,x) ->                                              [input]
   5 : pbeta(A,B)=>pbeta(B,cd(A))                       [reduction of 3 by [2]]
   6 : pbeta(A,B) -> pbeta(B,cd(A))                          [expansion from 5]
   7 : pbeta(s,t)and pbeta(s,x)=>?A.(pbeta(t,A)and pbeta(x,A)) ->  [reduction of 4 by [1]]
   8 : pbeta(s,t)and pbeta(s,x)                              [expansion from 7]
   9 : ?A.(pbeta(t,A)and pbeta(x,A)) ->                      [expansion from 7]
  10 : pbeta(t,A),pbeta(x,A) ->                              [expansion from 9]
  11 : pbeta(s,t)                                            [expansion from 8]
  12 : pbeta(s,x)                                            [expansion from 8]
  13 : pbeta(t,cd(s))                          [negative chaining of 11 from 6]
  14 : pbeta(x,cd(s))                          [negative chaining of 12 from 6]
  15 : false                                     [reduction of 14 by [10,13,L]]

Length = 15, Depth = 6



Total time: 1530 milliseconds

Number of forward inferences: 2
Number of tableau inferences: 4
Number of kept clauses: 10
*/