Charlie is furry. Charlie is green. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is red. Harry is furry. Harry is nice. Harry is quiet. Harry is red. Green, kind people are nice. All quiet people are green. All green, quiet people are red. If someone is red then they are green. If someone is nice and furry then they are big. All big people are furry.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Green, kind people are nice.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
All green, quiet people are red.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If someone is red then they are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is nice and furry then they are big.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
All big people are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Charlie is red.
True
1
proof
[(triple6 OR ((triple2 triple5) -> rule3) OR ((((triple5) -> rule2) triple5) -> rule3))]
("Charlie" "is" "red" "+")
triple6
((triple2 triple5) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple5) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Harry is not red.
False
1
inv-proof
[(triple10 OR ((((triple9) -> rule2) triple9) -> rule3))]
("Harry" "is" "red" "-")
triple10
((((triple9) -> (rule2 % int2)) triple9) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Charlie is big.
True
3
proof
[(((triple4 triple1) -> rule5) OR ((((triple2 triple3) -> rule1) triple1) -> rule5) OR ((((((triple5) -> rule2) triple3) -> rule1) triple1) -> rule5) OR ((((((triple6) -> rule4) triple3) -> rule1) triple1) -> rule5))]
("Charlie" "is" "big" "+")
((triple4 triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple2 triple3) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((((triple5) -> (rule2 % int3)) triple3) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((((((triple6) -> (rule4 % int3)) triple3) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is not big.
False
3
inv-proof
[(((triple4 triple1) -> rule5) OR ((((triple2 triple3) -> rule1) triple1) -> rule5) OR ((((((triple5) -> rule2) triple3) -> rule1) triple1) -> rule5) OR ((((((triple6) -> rule4) triple3) -> rule1) triple1) -> rule5))]
("Charlie" "is" "big" "-")
((triple4 triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple2 triple3) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((((triple5) -> (rule2 % int3)) triple3) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((((((triple6) -> (rule4 % int3)) triple3) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
@0: Charlie is furry.[(triple1)] Charlie is green.[(triple2 OR ((triple5) -> rule2) OR ((triple6) -> rule4))] Charlie is kind.[(triple3)] Charlie is nice.[(triple4 OR ((triple2 triple3) -> rule1) OR ((((triple5) -> rule2) triple3) -> rule1) OR ((((triple6) -> rule4) triple3) -> rule1))] Charlie is quiet.[(triple5)] Charlie is red.[(triple6 OR ((triple2 triple5) -> rule3) OR ((((triple5) -> rule2) triple5) -> rule3))] Harry is furry.[(triple7)] Harry is nice.[(triple8)] Harry is quiet.[(triple9)] Harry is red.[(triple10 OR ((((triple9) -> rule2) triple9) -> rule3))] @1: Charlie is big.[(((triple4 triple1) -> rule5) OR ((((triple2 triple3) -> rule1) triple1) -> rule5) OR ((((((triple5) -> rule2) triple3) -> rule1) triple1) -> rule5) OR ((((((triple6) -> rule4) triple3) -> rule1) triple1) -> rule5))] Harry is big.[(((triple8 triple7) -> rule5))] Harry is green.[(((triple10) -> rule4) OR ((triple9) -> rule2))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((triple5) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple6) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
((triple2 triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple5) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple6) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
((triple2 triple5) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple5) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
((((triple9) -> (rule2 % int2)) triple9) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((triple4 triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple2 triple3) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((((triple5) -> (rule2 % int3)) triple3) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((((((triple6) -> (rule4 % int3)) triple3) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((triple8 triple7) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple10) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple9) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1