Anne is rough. Dave is red. Fiona is blue. Gary is big. Red people are furry. All red, blue people are big. Red, furry people are blue.
Anne is rough.
("Anne" "is" "rough" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Gary is big.
("Gary" "is" "big" "+")
Red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All red, blue people are big.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Red, furry people are blue.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Dave is furry.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "furry" "-")
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
True
4
proof
[(((triple2 ((triple2) -> rule1)) -> rule3))]
("Dave" "is" "blue" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not blue.
False
4
inv-proof
[(((triple2 ((triple2) -> rule1)) -> rule3))]
("Dave" "is" "blue" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "furry" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "blue" "+")
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "furry" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is rough.[(triple1)] Dave is red.[(triple2)] Fiona is blue.[(triple3)] Gary is big.[(triple4)] @1: Dave is furry.[(((triple2) -> rule1))] @2: Dave is blue.[(((triple2 ((triple2) -> rule1)) -> rule3))] @3: Dave is big.[(((triple2 ((triple2 ((triple2) -> rule1)) -> rule3)) -> rule2))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((triple2 ((triple2 ((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3