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