Anne is rough. Charlie is quiet. Erin is cold. Gary is red. Cold things are red. All big things are red. If something is red then it is not green. All cold, nice things are green. If Gary is nice then Gary is cold. Rough things are cold. Cold, green things are big. If something is quiet and rough then it is not nice.
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is red.
("Gary" "is" "red" "+")
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is red then it is not green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "-"))
All cold, nice things are green.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If Gary is nice then Gary is cold.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "cold" "+"))
Rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Cold, green things are big.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is quiet and rough then it is not nice.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "-"))
Erin is cold.
True
1
proof
[(triple3)]
("Erin" "is" "cold" "+")
triple3
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Erin is red.
True
2
proof
[(((triple3) -> rule1))]
("Erin" "is" "red" "+")
((triple3) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is green.
False
2
inv-proof
[(((triple4) -> rule3))]
("Gary" "is" "green" "+")
((triple4) -> (rule3 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Erin is not green.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("Erin" "is" "green" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("Erin" "is" "green" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Anne is not green.
True
4
proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule3))]
("Anne" "is" "green" "-")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is green.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule3))]
("Anne" "is" "green" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "green" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "big" "+")
Charlie is not red.
Unknown
inv-rconc
[@3: Charlie is red.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule6 <- FAIL)]]
("Charlie" "is" "red" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "big" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Anne is rough.[(triple1)] Charlie is quiet.[(triple2)] Erin is cold.[(triple3)] Gary is red.[(triple4)] @1: Anne is cold.[(((triple1) -> rule6))] Erin is red.[(((triple3) -> rule1))] Gary is not green.[(((triple4) -> rule3))] @2: Anne is red.[(((((triple1) -> rule6)) -> rule1))] Erin is not green.[(((((triple3) -> rule1)) -> rule3))] @3: Anne is not green.[(((((((triple1) -> rule6)) -> rule1)) -> rule3))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
triple4
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple3) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is not green.
("Gary" "is" "green" "-")
((triple4) -> (rule3 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Erin is not green.
("Erin" "is" "green" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Anne is not green.
("Anne" "is" "green" "-")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3