Anne is nice. Anne is round. Bob is big. Bob is rough. Bob is round. Bob is smart. Charlie is not furry. Erin is not furry. Erin is not nice. Erin is rough. Erin is round. Erin is smart. If Bob is nice and Bob is big then Bob is not round. If something is round and not rough then it is nice. If something is big then it is not nice. All rough, nice things are big. If Anne is smart then Anne is furry. If something is furry and not smart then it is not white.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If Bob is nice and Bob is big then Bob is not round.
((("Bob" "is" "nice" "+") ("Bob" "is" "big" "+")) -> ("Bob" "is" "round" "-"))
If something is round and not rough then it is nice.
((("something" "is" "round" "+") ("something" "is" "rough" "~")) -> ("something" "is" "nice" "+"))
If something is big then it is not nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "-"))
All rough, nice things are big.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If Anne is smart then Anne is furry.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "furry" "+"))
If something is furry and not smart then it is not white.
((("something" "is" "furry" "+") ("something" "is" "smart" "~")) -> ("something" "is" "white" "-"))
Bob is rough.
True
1
proof
[(triple4)]
("Bob" "is" "rough" "+")
triple4
Erin is not smart.
False
1
inv-proof
[(triple12)]
("Erin" "is" "smart" "-")
triple12
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "big" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is nice.[(triple1)] Anne is round.[(triple2)] Bob is big.[(triple3)] Bob is rough.[(triple4)] Bob is round.[(triple5)] Bob is smart.[(triple6)] Charlie is not furry.[(triple7)] Erin is not furry.[(triple8)] Erin is not nice.[(triple9)] Erin is rough.[(triple10)] Erin is round.[(triple11)] Erin is smart.[(triple12)] @1: Bob is not nice.[(((triple3) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Bob is big.
("Bob" "is" "big" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple7
Erin is not furry.
("Erin" "is" "furry" "-")
triple8
Erin is not nice.
("Erin" "is" "nice" "-")
triple9
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Bob is not nice.
("Bob" "is" "nice" "-")
((triple3) -> (rule3 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1