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