Anne is red. Dave is white. Fiona is furry. Harry is white. Red things are furry. Big, red things are quiet. If something is rough and white then it is big. All blue things are white. If something is furry then it is white. Big things are blue.
Anne is red.
("Anne" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Harry is white.
("Harry" "is" "white" "+")
Red things are furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Big, red things are quiet.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If something is rough and white then it is big.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
All blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If something is furry then it is white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
Fiona is furry.
True
1
proof
[(triple3)]
("Fiona" "is" "furry" "+")
triple3
Harry is not white.
False
1
inv-proof
[(triple4)]
("Harry" "is" "white" "-")
triple4
Fiona is white.
True
2
proof
[(((triple3) -> rule5))]
("Fiona" "is" "white" "+")
((triple3) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not white.
False
2
inv-proof
[(((triple3) -> rule5))]
("Fiona" "is" "white" "-")
((triple3) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "white" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "furry" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "big" "+")
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "quiet" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is red.[(triple1)] Dave is white.[(triple2)] Fiona is furry.[(triple3)] Harry is white.[(triple4)] @1: Anne is furry.[(((triple1) -> rule1))] Fiona is white.[(((triple3) -> rule5))] @2: Anne is white.[(((((triple1) -> rule1)) -> rule5))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
triple4
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple3) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2