Anne is cold. Charlie is not blue. Charlie is cold. Charlie is nice. Dave is cold. Dave is not green. Dave is not rough. All green people are kind. If someone is red and rough then they are kind. If someone is green and red then they are cold. Nice people are green. Green people are not rough. Kind people are nice. Blue, cold people are nice. If someone is kind and green then they are not red.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is not rough.
("Dave" "is" "rough" "-")
All green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone is red and rough then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is green and red then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Green people are not rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "-"))
Kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Blue, cold people are nice.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is kind and green then they are not red.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "-"))
Dave is cold.
True
1
proof
[(triple5)]
("Dave" "is" "cold" "+")
triple5
Dave is rough.
False
1
inv-proof
[(triple7)]
("Dave" "is" "rough" "+")
triple7
Charlie is green.
True
2
proof
[(((triple4) -> rule4))]
("Charlie" "is" "green" "+")
((triple4) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple4) -> rule4))]
("Charlie" "is" "green" "-")
((triple4) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
True
3
proof
[(((((triple4) -> rule4)) -> rule1))]
("Charlie" "is" "kind" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule5))]
("Charlie" "is" "rough" "+")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not red.
True
6
proof
[(((((((triple4) -> rule4)) -> rule1) ((triple4) -> rule4)) -> rule8))]
("Charlie" "is" "red" "-")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2)) ((triple4) -> (rule4 % int3))) -> (rule8 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is red.
False
6
inv-proof
[(((((((triple4) -> rule4)) -> rule1) ((triple4) -> rule4)) -> rule8))]
("Charlie" "is" "red" "+")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2)) ((triple4) -> (rule4 % int3))) -> (rule8 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Anne is not green.
Unknown
inv-rconc
[@3: Anne is green.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule1 <- FAIL)]]
("Anne" "is" "green" "-")
Dave is nice.
Unknown
rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Dave" "is" "nice" "+")
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "kind" "-")
Anne is nice.
Unknown
rconc
[@4: Anne is nice.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule4 <- rule7 <- FAIL)]]
("Anne" "is" "nice" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Anne is cold.[(triple1)] Charlie is cold.[(triple3)] Charlie is nice.[(triple4)] Charlie is not blue.[(triple2)] Dave is cold.[(triple5)] Dave is not green.[(triple6)] Dave is not rough.[(triple7)] @1: Charlie is green.[(((triple4) -> rule4))] @2: Charlie is kind.[(((((triple4) -> rule4)) -> rule1))] Charlie is not rough.[(((((triple4) -> rule4)) -> rule5))] @3: Charlie is not red.[(((((((triple4) -> rule4)) -> rule1) ((triple4) -> rule4)) -> rule8))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is not green.
("Dave" "is" "green" "-")
triple6
Dave is not rough.
("Dave" "is" "rough" "-")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple4) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not rough.
("Charlie" "is" "rough" "-")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not red.
("Charlie" "is" "red" "-")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2)) ((triple4) -> (rule4 % int3))) -> (rule8 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3