Anne is cold. Anne is furry. Anne is quiet. Anne is white. Dave is blue. Dave is cold. Dave is furry. Dave is kind. Dave is quiet. Dave is round. Dave is white. Harry is cold. Harry is furry. Harry is kind. Harry is round. Harry is white. If someone is cold then they are white. Kind people are blue. Blue people are white. If someone is blue and cold then they are quiet. If Anne is white and Anne is kind then Anne is furry. All quiet people are round.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is cold then they are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If someone is blue and cold then they are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is white and Anne is kind then Anne is furry.
((("Anne" "is" "white" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "furry" "+"))
All quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Harry is cold.
True
1
proof
[(triple12)]
("Harry" "is" "cold" "+")
triple12
Dave is not quiet.
False
1
inv-proof
[(triple9 OR ((triple5 triple6) -> rule4) OR ((((triple8) -> rule2) triple6) -> rule4))]
("Dave" "is" "quiet" "-")
triple9
((triple5 triple6) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple8) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Anne is round.
True
2
proof
[(((triple3) -> rule6))]
("Anne" "is" "round" "+")
((triple3) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple14) -> rule2))]
("Harry" "is" "blue" "-")
((triple14) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
True
4
proof
[(((((triple14) -> rule2) triple12) -> rule4))]
("Harry" "is" "quiet" "+")
((((triple14) -> (rule2 % int2)) triple12) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not quiet.
False
4
inv-proof
[(((((triple14) -> rule2) triple12) -> rule4))]
("Harry" "is" "quiet" "-")
((((triple14) -> (rule2 % int2)) triple12) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2)] Anne is quiet.[(triple3)] Anne is white.[(triple4 OR ((triple1) -> rule1))] Dave is blue.[(triple5 OR ((triple8) -> rule2))] Dave is cold.[(triple6)] Dave is furry.[(triple7)] Dave is kind.[(triple8)] Dave is quiet.[(triple9 OR ((triple5 triple6) -> rule4) OR ((((triple8) -> rule2) triple6) -> rule4))] Dave is round.[(triple10 OR ((triple9) -> rule6) OR ((((triple5 triple6) -> rule4)) -> rule6) OR ((((((triple8) -> rule2) triple6) -> rule4)) -> rule6))] Dave is white.[(triple11 OR ((triple5) -> rule3) OR ((triple6) -> rule1) OR ((((triple8) -> rule2)) -> rule3))] Harry is cold.[(triple12)] Harry is furry.[(triple13)] Harry is kind.[(triple14)] Harry is round.[(triple15 OR ((((((triple14) -> rule2) triple12) -> rule4)) -> rule6))] Harry is white.[(triple16 OR ((triple12) -> rule1) OR ((((triple14) -> rule2)) -> rule3))] @1: Anne is round.[(((triple3) -> rule6))] Harry is blue.[(((triple14) -> rule2))] @2: Harry is quiet.[(((((triple14) -> rule2) triple12) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
((triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple5
((triple8) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple6
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
((triple5 triple6) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple8) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple10
((triple9) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple5 triple6) -> (rule4 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((((triple8) -> (rule2 % int3)) triple6) -> (rule4 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
triple11
((triple5) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple6) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
((((((triple14) -> (rule2 % int3)) triple12) -> (rule4 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
triple16
((triple12) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple14) -> (rule2 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((triple3) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple14) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple14) -> (rule2 % int2)) triple12) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2