Bob is furry. Bob is green. Bob is nice. Bob is red. Bob is not rough. Bob is smart. Bob is white. Fiona is not furry. Fiona is green. Fiona is nice. Fiona is red. Fiona is rough. Fiona is smart. Fiona is not white. If something is white and not red then it is nice. If something is red and white then it is furry. If Fiona is red and Fiona is rough then Fiona is green. If something is green and not white then it is rough. If something is smart and not furry then it is green. All rough, red things are green.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Fiona is not furry.
("Fiona" "is" "furry" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is not white.
("Fiona" "is" "white" "-")
If something is white and not red then it is nice.
((("something" "is" "white" "+") ("something" "is" "red" "~")) -> ("something" "is" "nice" "+"))
If something is red and white then it is furry.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If Fiona is red and Fiona is rough then Fiona is green.
((("Fiona" "is" "red" "+") ("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "green" "+"))
If something is green and not white then it is rough.
((("something" "is" "green" "+") ("something" "is" "white" "~")) -> ("something" "is" "rough" "+"))
If something is smart and not furry then it is green.
((("something" "is" "smart" "+") ("something" "is" "furry" "~")) -> ("something" "is" "green" "+"))
All rough, red things are green.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Fiona is red.
True
1
proof
[(triple11)]
("Fiona" "is" "red" "+")
triple11
Fiona is not smart.
False
1
inv-proof
[(triple13)]
("Fiona" "is" "smart" "-")
triple13
@0: Bob is furry.[(triple1 OR ((triple4 triple7) -> rule2))] Bob is green.[(triple2)] Bob is nice.[(triple3)] Bob is not rough.[(triple5)] Bob is red.[(triple4)] Bob is smart.[(triple6)] Bob is white.[(triple7)] Fiona is green.[(triple9 OR ((triple11 triple12) -> rule3) OR ((triple12 triple11) -> rule6) OR ((triple13 triple8) -> rule5))] Fiona is nice.[(triple10)] Fiona is not furry.[(triple8)] Fiona is not white.[(triple14)] Fiona is red.[(triple11)] Fiona is rough.[(triple12 OR ((triple9 triple14) -> rule4) OR ((((triple13 triple8) -> rule5) triple14) -> rule4))] Fiona is smart.[(triple13)]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
((triple4 triple7) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not rough.
("Bob" "is" "rough" "-")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
Fiona is green.
("Fiona" "is" "green" "+")
triple9
((triple11 triple12) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple12 triple11) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple13 triple8) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
Fiona is not furry.
("Fiona" "is" "furry" "-")
triple8
Fiona is not white.
("Fiona" "is" "white" "-")
triple14
Fiona is red.
("Fiona" "is" "red" "+")
triple11
Fiona is rough.
("Fiona" "is" "rough" "+")
triple12
((triple9 triple14) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((triple13 triple8) -> (rule5 % int2)) triple14) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple13