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