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