Bob is big. Bob is not blue. Bob is furry. Bob is green. Bob is red. Bob is not rough. Bob is white. Erin is big. Erin is blue. Erin is furry. Erin is green. Erin is red. Erin is rough. Erin is not white. All furry, rough people are red. Blue people are big. If Bob is white then Bob is big. If someone is rough then they are blue. All rough, green people are furry. If Erin is big and Erin is blue then Erin is red. If Erin is not furry and Erin is not white then Erin is red. If Erin is green and Erin is big then Erin is red.
Bob is big.
("Bob" "is" "big" "+")
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is white.
("Bob" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is not white.
("Erin" "is" "white" "-")
All furry, rough people are red.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
Blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If Bob is white then Bob is big.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "big" "+"))
If someone is rough then they are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
All rough, green people are furry.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If Erin is big and Erin is blue then Erin is red.
((("Erin" "is" "big" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "red" "+"))
If Erin is not furry and Erin is not white then Erin is red.
((("Erin" "is" "furry" "~") ("Erin" "is" "white" "~")) -> ("Erin" "is" "red" "+"))
If Erin is green and Erin is big then Erin is red.
((("Erin" "is" "green" "+") ("Erin" "is" "big" "+")) -> ("Erin" "is" "red" "+"))
Erin is green.
True
1
proof
[(triple11)]
("Erin" "is" "green" "+")
triple11
Erin is not big.
False
1
inv-proof
[(triple8 OR ((triple9) -> rule2) OR ((((triple13) -> rule4)) -> rule2))]
("Erin" "is" "big" "-")
triple8
((triple9) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple13) -> (rule4 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
@0: Bob is big.[(triple1 OR ((triple7) -> rule3))] Bob is furry.[(triple3)] Bob is green.[(triple4)] Bob is not blue.[(triple2)] Bob is not rough.[(triple6)] Bob is red.[(triple5)] Bob is white.[(triple7)] Erin is big.[(triple8 OR ((triple9) -> rule2) OR ((((triple13) -> rule4)) -> rule2))] Erin is blue.[(triple9 OR ((triple13) -> rule4))] Erin is furry.[(triple10 OR ((triple13 triple11) -> rule5))] Erin is green.[(triple11)] Erin is not white.[(triple14)] Erin is red.[(triple12 OR ((triple10 triple13) -> rule1) OR ((triple11 triple8) -> rule8) OR ((triple8 triple9) -> rule6) OR ((triple11 ((triple9) -> rule2)) -> rule8) OR ((triple8 ((triple13) -> rule4)) -> rule6) OR ((((triple9) -> rule2) triple9) -> rule6) OR ((((triple13 triple11) -> rule5) triple13) -> rule1) OR ((((triple9) -> rule2) ((triple13) -> rule4)) -> rule6) OR ((triple11 ((((triple13) -> rule4)) -> rule2)) -> rule8) OR ((((((triple13) -> rule4)) -> rule2) triple9) -> rule6) OR ((((((triple13) -> rule4)) -> rule2) ((triple13) -> rule4)) -> rule6))] Erin is rough.[(triple13)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple7) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is not blue.
("Bob" "is" "blue" "-")
triple2
Bob is not rough.
("Bob" "is" "rough" "-")
triple6
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
((triple9) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple13) -> (rule4 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
triple9
((triple13) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple10
((triple13 triple11) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple11
Erin is not white.
("Erin" "is" "white" "-")
triple14
Erin is red.
("Erin" "is" "red" "+")
triple12
((triple10 triple13) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple11 triple8) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple8 triple9) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple11 ((triple9) -> (rule2 % int2))) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((triple8 ((triple13) -> (rule4 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple9) -> (rule2 % int2)) triple9) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple13 triple11) -> (rule5 % int2)) triple13) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple9) -> (rule2 % int3)) ((triple13) -> (rule4 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
((triple11 ((((triple13) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple13) -> (rule4 % int3))) -> (rule2 % int2)) triple9) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple13) -> (rule4 % int3))) -> (rule2 % int2)) ((triple13) -> (rule4 % int3))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
triple13