Harry is big. Harry is quiet. Harry is round. If someone is kind then they are nice. All green, quiet people are nice. Nice people are kind. All blue people are nice. If Harry is quiet then Harry is green. Round people are green. If someone is round and blue then they are nice. Kind people are nice.
Harry is big.
("Harry" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is kind then they are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
All green, quiet people are nice.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If Harry is quiet then Harry is green.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "green" "+"))
Round people are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is round and blue then they are nice.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Harry is big.
True
1
proof
[(triple1)]
("Harry" "is" "big" "+")
triple1
Harry is not quiet.
False
1
inv-proof
[(triple2)]
("Harry" "is" "quiet" "-")
triple2
Harry is green.
True
2
proof
[(((triple2) -> rule5) OR ((triple3) -> rule6))]
("Harry" "is" "green" "+")
((triple2) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple3) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple2) -> rule5) OR ((triple3) -> rule6))]
("Harry" "is" "green" "-")
((triple2) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple3) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
True
4
proof
[(((((triple2) -> rule5) triple2) -> rule2) OR ((((triple3) -> rule6) triple2) -> rule2))]
("Harry" "is" "nice" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple3) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not nice.
False
4
inv-proof
[(((((triple2) -> rule5) triple2) -> rule2) OR ((((triple3) -> rule6) triple2) -> rule2))]
("Harry" "is" "nice" "-")
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple3) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is kind.
True
5
proof
[(((((((triple2) -> rule5) triple2) -> rule2)) -> rule3) OR ((((((triple3) -> rule6) triple2) -> rule2)) -> rule3))]
("Harry" "is" "kind" "+")
((((((triple2) -> (rule5 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple3) -> (rule6 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not kind.
False
5
inv-proof
[(((((((triple2) -> rule5) triple2) -> rule2)) -> rule3) OR ((((((triple3) -> rule6) triple2) -> rule2)) -> rule3))]
("Harry" "is" "kind" "-")
((((((triple2) -> (rule5 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple3) -> (rule6 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
@0: Harry is big.[(triple1)] Harry is quiet.[(triple2)] Harry is round.[(triple3)] @1: Harry is green.[(((triple2) -> rule5) OR ((triple3) -> rule6))] @2: Harry is nice.[(((((triple2) -> rule5) triple2) -> rule2) OR ((((triple3) -> rule6) triple2) -> rule2))] @3: Harry is kind.[(((((((triple2) -> rule5) triple2) -> rule2)) -> rule3) OR ((((((triple3) -> rule6) triple2) -> rule2)) -> rule3))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
((triple2) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple3) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple3) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple2) -> (rule5 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple3) -> (rule6 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3