Anne is not blue. Anne is kind. Anne is red. Anne is rough. Anne is round. Anne is white. Bob is not kind. Bob is red. Bob is not rough. Bob is round. Harry is cold. Harry is kind. Harry is red. Harry is rough. Harry is round. Harry is white. If Anne is red and Anne is round then Anne is cold. All kind, red things are cold. All cold, red things are white. All rough things are white. If something is white and not red then it is blue. If something is rough then it is kind.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is red.
("Bob" "is" "red" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is round.
("Bob" "is" "round" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Anne is red and Anne is round then Anne is cold.
((("Anne" "is" "red" "+") ("Anne" "is" "round" "+")) -> ("Anne" "is" "cold" "+"))
All kind, red things are cold.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
All cold, red things are white.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
All rough things are white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If something is white and not red then it is blue.
((("something" "is" "white" "+") ("something" "is" "red" "~")) -> ("something" "is" "blue" "+"))
If something is rough then it is kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Harry is red.
True
1
proof
[(triple13)]
("Harry" "is" "red" "+")
triple13
Bob is not round.
False
1
inv-proof
[(triple10)]
("Bob" "is" "round" "-")
triple10
Anne is cold.
True
3
proof
[(((triple2 triple3) -> rule2) OR ((triple3 triple5) -> rule1) OR ((((triple4) -> rule6) triple3) -> rule2))]
("Anne" "is" "cold" "+")
((triple2 triple3) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple3 triple5) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple4) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((triple2 triple3) -> rule2) OR ((triple3 triple5) -> rule1) OR ((((triple4) -> rule6) triple3) -> rule2))]
("Anne" "is" "cold" "-")
((triple2 triple3) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple3 triple5) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple4) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "cold" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "blue" "+")
@0: Anne is kind.[(triple2 OR ((triple4) -> rule6))] Anne is not blue.[(triple1)] Anne is red.[(triple3)] Anne is rough.[(triple4)] Anne is round.[(triple5)] Anne is white.[(triple6 OR ((triple4) -> rule4) OR ((((triple2 triple3) -> rule2) triple3) -> rule3) OR ((((triple3 triple5) -> rule1) triple3) -> rule3) OR ((((((triple4) -> rule6) triple3) -> rule2) triple3) -> rule3))] Bob is not kind.[(triple7)] Bob is not rough.[(triple9)] Bob is red.[(triple8)] Bob is round.[(triple10)] Harry is cold.[(triple11 OR ((triple12 triple13) -> rule2) OR ((((triple14) -> rule6) triple13) -> rule2))] Harry is kind.[(triple12 OR ((triple14) -> rule6))] Harry is red.[(triple13)] Harry is rough.[(triple14)] Harry is round.[(triple15)] Harry is white.[(triple16 OR ((triple14) -> rule4) OR ((triple11 triple13) -> rule3) OR ((((triple12 triple13) -> rule2) triple13) -> rule3) OR ((((((triple14) -> rule6) triple13) -> rule2) triple13) -> rule3))] @1: Anne is cold.[(((triple2 triple3) -> rule2) OR ((triple3 triple5) -> rule1) OR ((((triple4) -> rule6) triple3) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple4) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple4) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple2 triple3) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple3 triple5) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((((triple4) -> (rule6 % int3)) triple3) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Bob is not kind.
("Bob" "is" "kind" "-")
triple7
Bob is not rough.
("Bob" "is" "rough" "-")
triple9
Bob is red.
("Bob" "is" "red" "+")
triple8
Bob is round.
("Bob" "is" "round" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
((triple12 triple13) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple14) -> (rule6 % int2)) triple13) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple12
((triple14) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
((triple14) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple11 triple13) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple12 triple13) -> (rule2 % int2)) triple13) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((triple14) -> (rule6 % int3)) triple13) -> (rule2 % int2)) triple13) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
((triple2 triple3) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple3 triple5) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple4) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2