Anne is red. Anne is round. Anne is white. Anne is young. Bob is cold. Bob is white. Harry is white. If Bob is round and Bob is nice then Bob is red. If Anne is cold and Anne is red then Anne is white. All cold things are kind. All cold things are round. If something is cold and white then it is kind. Red, cold things are nice. If something is kind and white then it is red. If Anne is white and Anne is nice then Anne is round.
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is white.
("Bob" "is" "white" "+")
Harry is white.
("Harry" "is" "white" "+")
If Bob is round and Bob is nice then Bob is red.
((("Bob" "is" "round" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "red" "+"))
If Anne is cold and Anne is red then Anne is white.
((("Anne" "is" "cold" "+") ("Anne" "is" "red" "+")) -> ("Anne" "is" "white" "+"))
All cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
All cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is cold and white then it is kind.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Red, cold things are nice.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is kind and white then it is red.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If Anne is white and Anne is nice then Anne is round.
((("Anne" "is" "white" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "round" "+"))
Anne is round.
True
1
proof
[(triple2)]
("Anne" "is" "round" "+")
triple2
Anne is not red.
False
1
inv-proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Bob is kind.
True
2
proof
[(((triple5) -> rule3) OR ((triple5 triple6) -> rule5))]
("Bob" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple5 triple6) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple5) -> rule3) OR ((triple5 triple6) -> rule5))]
("Bob" "is" "kind" "-")
((triple5) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple5 triple6) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
True
4
proof
[(((((triple5) -> rule3) triple6) -> rule7) OR ((((triple5 triple6) -> rule5) triple6) -> rule7))]
("Bob" "is" "red" "+")
((((triple5) -> (rule3 % int2)) triple6) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple5 triple6) -> (rule5 % int2)) triple6) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not red.
False
4
inv-proof
[(((((triple5) -> rule3) triple6) -> rule7) OR ((((triple5 triple6) -> rule5) triple6) -> rule7))]
("Bob" "is" "red" "-")
((((triple5) -> (rule3 % int2)) triple6) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple5 triple6) -> (rule5 % int2)) triple6) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Harry is not red.
Unknown
inv-rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "round" "+")
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is red.[(triple1)] Anne is round.[(triple2)] Anne is white.[(triple3)] Anne is young.[(triple4)] Bob is cold.[(triple5)] Bob is white.[(triple6)] Harry is white.[(triple7)] @1: Bob is kind.[(((triple5) -> rule3) OR ((triple5 triple6) -> rule5))] Bob is round.[(((triple5) -> rule4))] @2: Bob is red.[(((((triple5) -> rule3) triple6) -> rule7) OR ((((triple5 triple6) -> rule5) triple6) -> rule7))] @3: Bob is nice.[(((((((triple5) -> rule3) triple6) -> rule7) triple5) -> rule6) OR ((((((triple5 triple6) -> rule5) triple6) -> rule7) triple5) -> rule6))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Bob is cold.
("Bob" "is" "cold" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple5 triple6) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple5) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple5) -> (rule3 % int2)) triple6) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple5 triple6) -> (rule5 % int2)) triple6) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((((triple5) -> (rule3 % int3)) triple6) -> (rule7 % int2)) triple5) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple5 triple6) -> (rule5 % int3)) triple6) -> (rule7 % int2)) triple5) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3