Anne is rough. Bob is round. Harry is white. If something is white and round then it is rough. All round things are blue. Nice, white things are rough. If something is nice and rough then it is red. If something is white and blue then it is round. All rough things are blue. If something is nice then it is rough. If Bob is round and Bob is red then Bob is quiet.
Anne is rough.
("Anne" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is white and round then it is rough.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
All round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Nice, white things are rough.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If something is nice and rough then it is red.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is white and blue then it is round.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
All rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If Bob is round and Bob is red then Bob is quiet.
((("Bob" "is" "round" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "quiet" "+"))
Bob is round.
True
1
proof
[(triple2)]
("Bob" "is" "round" "+")
triple2
Bob is not round.
False
1
inv-proof
[(triple2)]
("Bob" "is" "round" "-")
triple2
Bob is blue.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "blue" "-")
((triple2) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Harry is not blue.
Unknown
inv-rconc
[@4: Harry is blue.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule6 <- rule1 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is rough.
Unknown
rconc
[@4: Harry is rough.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule6 <- rule3 <- FAIL)]]
("Harry" "is" "rough" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Anne is rough.[(triple1)] Bob is round.[(triple2)] Harry is white.[(triple3)] @1: Anne is blue.[(((triple1) -> rule6))] Bob is blue.[(((triple2) -> rule2))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1