Bob is furry. Bob is red. Bob is rough. Charlie is round. Dave is blue. Dave is young. Gary is young. All rough, round things are green. If something is round then it is rough.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is young.
("Gary" "is" "young" "+")
All rough, round things are green.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is round then it is rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
Bob is red.
True
1
proof
[(triple2)]
("Bob" "is" "red" "+")
triple2
Bob is not red.
False
1
inv-proof
[(triple2)]
("Bob" "is" "red" "-")
triple2
Charlie is rough.
True
2
proof
[(((triple4) -> rule2))]
("Charlie" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple4) -> rule2))]
("Charlie" "is" "rough" "-")
((triple4) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
True
4
proof
[(((((triple4) -> rule2) triple4) -> rule1))]
("Charlie" "is" "green" "+")
((((triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not green.
False
4
inv-proof
[(((((triple4) -> rule2) triple4) -> rule1))]
("Charlie" "is" "green" "-")
((((triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "green" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Bob is furry.[(triple1)] Bob is red.[(triple2)] Bob is rough.[(triple3)] Charlie is round.[(triple4)] Dave is blue.[(triple5)] Dave is young.[(triple6)] Gary is young.[(triple7)] @1: Charlie is rough.[(((triple4) -> rule2))] @2: Charlie is green.[(((((triple4) -> rule2) triple4) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2