Anne is furry. Anne is green. Anne is kind. Anne is quiet. Anne is red. Anne is round. Anne is smart. Dave is furry. Dave is green. Dave is kind. Dave is red. Dave is smart. If Dave is green and Dave is smart then Dave is quiet. Red people are smart. All kind people are round. If someone is green then they are furry. Smart people are kind. Green, red people are smart.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If Dave is green and Dave is smart then Dave is quiet.
((("Dave" "is" "green" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "quiet" "+"))
Red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
All kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If someone is green then they are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Green, red people are smart.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Anne is red.
True
1
proof
[(triple5)]
("Anne" "is" "red" "+")
triple5
Dave is not red.
False
1
inv-proof
[(triple11)]
("Dave" "is" "red" "-")
triple11
@0: Anne is furry.[(triple1 OR ((triple2) -> rule4))] Anne is green.[(triple2)] Anne is kind.[(triple3 OR ((triple7) -> rule5) OR ((((triple5) -> rule2)) -> rule5) OR ((((triple2 triple5) -> rule6)) -> rule5))] Anne is quiet.[(triple4)] Anne is red.[(triple5)] Anne is round.[(triple6 OR ((triple3) -> rule3) OR ((((triple7) -> rule5)) -> rule3) OR ((((((triple5) -> rule2)) -> rule5)) -> rule3) OR ((((((triple2 triple5) -> rule6)) -> rule5)) -> rule3))] Anne is smart.[(triple7 OR ((triple5) -> rule2) OR ((triple2 triple5) -> rule6))] Dave is furry.[(triple8 OR ((triple9) -> rule4))] Dave is green.[(triple9)] Dave is kind.[(triple10 OR ((triple12) -> rule5) OR ((((triple11) -> rule2)) -> rule5) OR ((((triple9 triple11) -> rule6)) -> rule5))] Dave is red.[(triple11)] Dave is smart.[(triple12 OR ((triple11) -> rule2) OR ((triple9 triple11) -> rule6))] @1: Dave is quiet.[(((triple9 triple12) -> rule1) OR ((triple9 ((triple11) -> rule2)) -> rule1) OR ((triple9 ((triple9 triple11) -> rule6)) -> rule1))] Dave is round.[(((triple10) -> rule3) OR ((((triple12) -> rule5)) -> rule3) OR ((((((triple11) -> rule2)) -> rule5)) -> rule3) OR ((((((triple9 triple11) -> rule6)) -> rule5)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple2) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple7) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple2 triple5) -> (rule6 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple3) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((triple2 triple5) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
triple7
((triple5) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple2 triple5) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple8
((triple9) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is kind.
("Dave" "is" "kind" "+")
triple10
((triple12) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple11) -> (rule2 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple9 triple11) -> (rule6 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
triple12
((triple11) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple9 triple11) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple9 triple12) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple9 ((triple11) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple9 ((triple9 triple11) -> (rule6 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((triple10) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple12) -> (rule5 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((((triple11) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((((((triple9 triple11) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3