Anne is rough. Bob is white. Gary is blue. White things are nice. If something is white and rough then it is green. If something is nice and round then it is rough. All round things are rough. If something is nice then it is rough. If something is round and furry then it is not blue.
Anne is rough.
("Anne" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
White things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is white and rough then it is green.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is nice and round then it is rough.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
All round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something is round and furry then it is not blue.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "-"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Gary is not blue.
False
1
inv-proof
[(triple3)]
("Gary" "is" "blue" "-")
triple3
Bob is nice.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "nice" "-")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
True
3
proof
[(((((triple2) -> rule1)) -> rule5))]
("Bob" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not rough.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5))]
("Bob" "is" "rough" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "nice" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is rough.[(triple1)] Bob is white.[(triple2)] Gary is blue.[(triple3)] @1: Bob is nice.[(((triple2) -> rule1))] @2: Bob is rough.[(((((triple2) -> rule1)) -> rule5))] @3: Bob is green.[(((triple2 ((((triple2) -> rule1)) -> rule5)) -> rule2))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3