Charlie is red. Dave is cold. Gary is red. All cold things are rough. If something is red then it is green. If Gary is kind then Gary is blue. If something is green then it is cold. Red things are cold. If something is red and cold then it is kind.
Charlie is red.
("Charlie" "is" "red" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Gary is red.
("Gary" "is" "red" "+")
All cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something is red then it is green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If Gary is kind then Gary is blue.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "blue" "+"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is red and cold then it is kind.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Dave is cold.
True
1
proof
[(triple2)]
("Dave" "is" "cold" "+")
triple2
Charlie is not red.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "red" "-")
triple1
Charlie is green.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "green" "+")
((triple1) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple3) -> rule5) OR ((((triple3) -> rule2)) -> rule4))]
("Gary" "is" "cold" "-")
((triple3) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is rough.
True
3
proof
[(((((triple3) -> rule5)) -> rule1) OR ((((((triple3) -> rule2)) -> rule4)) -> rule1))]
("Gary" "is" "rough" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Charlie is not kind.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule6) OR ((triple1 ((((triple1) -> rule2)) -> rule4)) -> rule6))]
("Charlie" "is" "kind" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Gary is blue.
True
5
proof
[(((((triple3 ((triple3) -> rule5)) -> rule6)) -> rule3) OR ((((triple3 ((((triple3) -> rule2)) -> rule4)) -> rule6)) -> rule3))]
("Gary" "is" "blue" "+")
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple3 ((((triple3) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is not blue.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule5)) -> rule6)) -> rule3) OR ((((triple3 ((((triple3) -> rule2)) -> rule4)) -> rule6)) -> rule3))]
("Gary" "is" "blue" "-")
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple3 ((((triple3) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "kind" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Charlie is red.[(triple1)] Dave is cold.[(triple2)] Gary is red.[(triple3)] @1: Charlie is cold.[(((triple1) -> rule5) OR ((((triple1) -> rule2)) -> rule4))] Charlie is green.[(((triple1) -> rule2))] Dave is rough.[(((triple2) -> rule1))] Gary is cold.[(((triple3) -> rule5) OR ((((triple3) -> rule2)) -> rule4))] Gary is green.[(((triple3) -> rule2))] @2: Charlie is kind.[(((triple1 ((triple1) -> rule5)) -> rule6) OR ((triple1 ((((triple1) -> rule2)) -> rule4)) -> rule6))] Charlie is rough.[(((((triple1) -> rule5)) -> rule1) OR ((((((triple1) -> rule2)) -> rule4)) -> rule1))] Gary is kind.[(((triple3 ((triple3) -> rule5)) -> rule6) OR ((triple3 ((((triple3) -> rule2)) -> rule4)) -> rule6))] Gary is rough.[(((((triple3) -> rule5)) -> rule1) OR ((((((triple3) -> rule2)) -> rule4)) -> rule1))] @3: Gary is blue.[(((((triple3 ((triple3) -> rule5)) -> rule6)) -> rule3) OR ((((triple3 ((((triple3) -> rule2)) -> rule4)) -> rule6)) -> rule3))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple3) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((triple3) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple3 ((((triple3) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4