Anne is furry. Bob is blue. Bob is furry. Bob is nice. Bob is quiet. Bob is white. Dave is furry. Dave is nice. Dave is quiet. Dave is red. Dave is rough. Dave is white. If Anne is furry and Anne is white then Anne is nice. If Bob is red then Bob is blue. Quiet, white things are blue. All white, nice things are quiet. If Bob is blue and Bob is furry then Bob is nice. Furry, red things are rough. Red things are nice. All red, white things are nice.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
If Anne is furry and Anne is white then Anne is nice.
((("Anne" "is" "furry" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "nice" "+"))
If Bob is red then Bob is blue.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "blue" "+"))
Quiet, white things are blue.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
All white, nice things are quiet.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If Bob is blue and Bob is furry then Bob is nice.
((("Bob" "is" "blue" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "nice" "+"))
Furry, red things are rough.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
All red, white things are nice.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Bob is nice.
True
1
proof
[(triple4 OR ((triple2 triple3) -> rule5) OR ((((triple5 triple6) -> rule3) triple3) -> rule5))]
("Bob" "is" "nice" "+")
triple4
((triple2 triple3) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple5 triple6) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not nice.
False
1
inv-proof
[(triple4 OR ((triple2 triple3) -> rule5) OR ((((triple5 triple6) -> rule3) triple3) -> rule5))]
("Bob" "is" "nice" "-")
triple4
((triple2 triple3) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple5 triple6) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "rough" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is furry.[(triple1)] Bob is blue.[(triple2 OR ((triple5 triple6) -> rule3) OR ((((triple6 triple4) -> rule4) triple6) -> rule3))] Bob is furry.[(triple3)] Bob is nice.[(triple4 OR ((triple2 triple3) -> rule5) OR ((((triple5 triple6) -> rule3) triple3) -> rule5))] Bob is quiet.[(triple5 OR ((triple6 triple4) -> rule4) OR ((triple6 ((triple2 triple3) -> rule5)) -> rule4))] Bob is white.[(triple6)] Dave is furry.[(triple7)] Dave is nice.[(triple8 OR ((triple10) -> rule7) OR ((triple10 triple12) -> rule8))] Dave is quiet.[(triple9 OR ((triple12 triple8) -> rule4) OR ((triple12 ((triple10) -> rule7)) -> rule4) OR ((triple12 ((triple10 triple12) -> rule8)) -> rule4))] Dave is red.[(triple10)] Dave is rough.[(triple11 OR ((triple7 triple10) -> rule6))] Dave is white.[(triple12)] @1: Dave is blue.[(((triple9 triple12) -> rule3) OR ((((triple12 triple8) -> rule4) triple12) -> rule3) OR ((((triple12 ((triple10) -> rule7)) -> rule4) triple12) -> rule3) OR ((((triple12 ((triple10 triple12) -> rule8)) -> rule4) triple12) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple5 triple6) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple6 triple4) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((triple2 triple3) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple5 triple6) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple6 triple4) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple6 ((triple2 triple3) -> (rule5 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple6
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
triple8
((triple10) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple10 triple12) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
((triple12 triple8) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple12 ((triple10) -> (rule7 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((triple12 ((triple10 triple12) -> (rule8 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple10
Dave is rough.
("Dave" "is" "rough" "+")
triple11
((triple7 triple10) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple12
Dave is blue.
("Dave" "is" "blue" "+")
((triple9 triple12) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple12 triple8) -> (rule4 % int2)) triple12) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple12 ((triple10) -> (rule7 % int3))) -> (rule4 % int2)) triple12) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((triple12 ((triple10 triple12) -> (rule8 % int3))) -> (rule4 % int2)) triple12) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3