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