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