Anne is cold. Anne is red. Anne is young. Bob is quiet. Dave is quiet. Dave is round. Dave is young. Harry is not quiet. Harry is not red. Harry is rough. All red, cold people are white. All red people are white. Young people are white. If someone is rough and cold then they are not white. Cold people are young. If someone is red and white then they are young. If someone is young and cold then they are round. If someone is cold and not white then they are round.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is not red.
("Harry" "is" "red" "-")
Harry is rough.
("Harry" "is" "rough" "+")
All red, cold people are white.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
All red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If someone is rough and cold then they are not white.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "-"))
Cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone is red and white then they are young.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If someone is young and cold then they are round.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is cold and not white then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "round" "+"))
Harry is not quiet.
True
1
proof
[(triple8)]
("Harry" "is" "quiet" "-")
triple8
Dave is not quiet.
False
1
inv-proof
[(triple5)]
("Dave" "is" "quiet" "-")
triple5
Bob is not white.
Unknown
inv-rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Anne is red.[(triple2)] Anne is young.[(triple3 OR ((triple1) -> rule5) OR ((triple2 ((triple2) -> rule2)) -> rule6) OR ((triple2 ((triple2 triple1) -> rule1)) -> rule6))] Bob is quiet.[(triple4)] Dave is quiet.[(triple5)] Dave is round.[(triple6)] Dave is young.[(triple7)] Harry is not quiet.[(triple8)] Harry is not red.[(triple9)] Harry is rough.[(triple10)] @1: Anne is round.[(((triple3 triple1) -> rule7) OR ((((triple1) -> rule5) triple1) -> rule7) OR ((((triple2 ((triple2) -> rule2)) -> rule6) triple1) -> rule7) OR ((((triple2 ((triple2 triple1) -> rule1)) -> rule6) triple1) -> rule7))] Anne is white.[(((triple2) -> rule2) OR ((triple3) -> rule3) OR ((triple2 triple1) -> rule1) OR ((((triple1) -> rule5)) -> rule3))] Dave is white.[(((triple7) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((triple2 ((triple2 triple1) -> (rule1 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple8
Harry is not red.
("Harry" "is" "red" "-")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Anne is round.
("Anne" "is" "round" "+")
((triple3 triple1) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple1) -> (rule5 % int2)) triple1) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((triple2 ((triple2 triple1) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((triple2) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple3) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple2 triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((triple7) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1