Harry is big. Harry is red. Harry is rough. If someone is red and quiet then they are round. Big people are quiet. If Harry is big then Harry is kind. If someone is rough then they are big. Quiet, kind people are white. If someone is round then they are quiet.
Harry is big.
("Harry" "is" "big" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is red and quiet then they are round.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If Harry is big then Harry is kind.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "kind" "+"))
If someone is rough then they are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Quiet, kind people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If someone is round then they are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Harry is big.
True
1
proof
[(triple1 OR ((triple3) -> rule4))]
("Harry" "is" "big" "+")
triple1
((triple3) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule4))]
("Harry" "is" "big" "-")
triple1
((triple3) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
True
2
proof
[(((triple1) -> rule3) OR ((((triple3) -> rule4)) -> rule3))]
("Harry" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not quiet.
False
2
inv-proof
[(((triple1) -> rule2) OR ((((triple3) -> rule4)) -> rule2))]
("Harry" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
True
4
proof
[(((triple2 ((triple1) -> rule2)) -> rule1) OR ((triple2 ((((triple3) -> rule4)) -> rule2)) -> rule1))]
("Harry" "is" "round" "+")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not round.
False
4
inv-proof
[(((triple2 ((triple1) -> rule2)) -> rule1) OR ((triple2 ((((triple3) -> rule4)) -> rule2)) -> rule1))]
("Harry" "is" "round" "-")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
@0: Harry is big.[(triple1 OR ((triple3) -> rule4))] Harry is red.[(triple2)] Harry is rough.[(triple3)] @1: Harry is kind.[(((triple1) -> rule3) OR ((((triple3) -> rule4)) -> rule3))] Harry is quiet.[(((triple1) -> rule2) OR ((((triple3) -> rule4)) -> rule2))] @2: Harry is round.[(((triple2 ((triple1) -> rule2)) -> rule1) OR ((triple2 ((((triple3) -> rule4)) -> rule2)) -> rule1))] Harry is white.[(((((triple1) -> rule2) ((triple1) -> rule3)) -> rule5) OR ((((triple1) -> rule2) ((((triple3) -> rule4)) -> rule3)) -> rule5) OR ((((((triple3) -> rule4)) -> rule2) ((triple1) -> rule3)) -> rule5) OR ((((((triple3) -> rule4)) -> rule2) ((((triple3) -> rule4)) -> rule3)) -> rule5))]
Harry is big.
("Harry" "is" "big" "+")
triple1
((triple3) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((triple1) -> (rule2 % int4)) ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
((((((triple3) -> (rule4 % int4))) -> (rule2 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((((triple3) -> (rule4 % int4))) -> (rule2 % int3)) ((((triple3) -> (rule4 % int4))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4