Anne is blue. Anne is nice. Anne is rough. Dave is blue. Dave is furry. Dave is nice. Dave is quiet. Dave is white. Fiona is quiet. Fiona is white. Blue people are furry. Blue, furry people are white. If Anne is furry and Anne is quiet then Anne is white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Blue, furry people are white.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If Anne is furry and Anne is quiet then Anne is white.
((("Anne" "is" "furry" "+") ("Anne" "is" "quiet" "+")) -> ("Anne" "is" "white" "+"))
Dave is white.
True
1
proof
[(triple8 OR ((triple4 triple5) -> rule2) OR ((triple4 ((triple4) -> rule1)) -> rule2))]
("Dave" "is" "white" "+")
triple8
((triple4 triple5) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not blue.
False
1
inv-proof
[(triple4)]
("Dave" "is" "blue" "-")
triple4
Anne is furry.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Anne is blue.[(triple1)] Anne is nice.[(triple2)] Anne is rough.[(triple3)] Dave is blue.[(triple4)] Dave is furry.[(triple5 OR ((triple4) -> rule1))] Dave is nice.[(triple6)] Dave is quiet.[(triple7)] Dave is white.[(triple8 OR ((triple4 triple5) -> rule2) OR ((triple4 ((triple4) -> rule1)) -> rule2))] Fiona is quiet.[(triple9)] Fiona is white.[(triple10)] @1: Anne is furry.[(((triple1) -> rule1))] @2: Anne is white.[(((triple1 ((triple1) -> rule1)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
((triple4) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
triple8
((triple4 triple5) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2