Bob is furry. Bob is not green. Bob is kind. Bob is rough. Bob is smart. Erin is furry. Erin is red. Erin is smart. Erin is young. Fiona is furry. Fiona is not rough. Harry is not young. If someone is smart then they are rough. If someone is red and not smart then they are rough. If Erin is green then Erin is not red. Young, rough people are furry. If someone is smart then they are furry. If someone is smart and not green then they are red. If Fiona is young and Fiona is green then Fiona is not red. If someone is smart and not furry then they are kind.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is not rough.
("Fiona" "is" "rough" "-")
Harry is not young.
("Harry" "is" "young" "-")
If someone is smart then they are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If someone is red and not smart then they are rough.
((("someone" "is" "red" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "rough" "+"))
If Erin is green then Erin is not red.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "red" "-"))
Young, rough people are furry.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart then they are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart and not green then they are red.
((("someone" "is" "smart" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "red" "+"))
If Fiona is young and Fiona is green then Fiona is not red.
((("Fiona" "is" "young" "+") ("Fiona" "is" "green" "+")) -> ("Fiona" "is" "red" "-"))
If someone is smart and not furry then they are kind.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "kind" "+"))
Erin is smart.
True
1
proof
[(triple8)]
("Erin" "is" "smart" "+")
triple8
Bob is not rough.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule1))]
("Bob" "is" "rough" "-")
triple4
((triple5) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "furry" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Bob is furry.[(triple1 OR ((triple5) -> rule5))] Bob is kind.[(triple3)] Bob is not green.[(triple2)] Bob is rough.[(triple4 OR ((triple5) -> rule1))] Bob is smart.[(triple5)] Erin is furry.[(triple6 OR ((triple8) -> rule5) OR ((triple9 ((triple8) -> rule1)) -> rule4))] Erin is red.[(triple7)] Erin is smart.[(triple8)] Erin is young.[(triple9)] Fiona is furry.[(triple10)] Fiona is not rough.[(triple11)] Harry is not young.[(triple12)] @1: Bob is red.[(((triple5 triple2) -> rule6))] Erin is rough.[(((triple8) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
((triple5) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is not green.
("Bob" "is" "green" "-")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple4
((triple5) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple6
((triple8) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple9 ((triple8) -> (rule1 % int2))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
triple8
Erin is young.
("Erin" "is" "young" "+")
triple9
Fiona is furry.
("Fiona" "is" "furry" "+")
triple10
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple11
Harry is not young.
("Harry" "is" "young" "-")
triple12
Bob is red.
("Bob" "is" "red" "+")
((triple5 triple2) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple8) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1