Charlie is kind. Fiona is rough. Gary is not red. Green, red people are white. If someone is smart and not kind then they are white. If Charlie is cold then Charlie is green. All white people are cold. If someone is green then they are not red. If someone is red and not kind then they are smart. If Fiona is kind then Fiona is cold. If Charlie is kind then Charlie is white.
Charlie is kind.
("Charlie" "is" "kind" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is not red.
("Gary" "is" "red" "-")
Green, red people are white.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If someone is smart and not kind then they are white.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "white" "+"))
If Charlie is cold then Charlie is green.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "green" "+"))
All white people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If someone is green then they are not red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "-"))
If someone is red and not kind then they are smart.
((("someone" "is" "red" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "smart" "+"))
If Fiona is kind then Fiona is cold.
((("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "cold" "+"))
If Charlie is kind then Charlie is white.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "white" "+"))
Fiona is rough.
True
1
proof
[(triple2)]
("Fiona" "is" "rough" "+")
triple2
Charlie is not kind.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "kind" "-")
triple1
Charlie is white.
True
2
proof
[(((triple1) -> rule8))]
("Charlie" "is" "white" "+")
((triple1) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple1) -> rule8))]
("Charlie" "is" "white" "-")
((triple1) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
True
3
proof
[(((((triple1) -> rule8)) -> rule4))]
("Charlie" "is" "cold" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not cold.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule4))]
("Charlie" "is" "cold" "-")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is green.
True
4
proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule3))]
("Charlie" "is" "green" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not green.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule3))]
("Charlie" "is" "green" "-")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "smart" "-")
Gary is cold.
Unknown
rconc
[@2: Gary is cold.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Gary" "is" "cold" "+")
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "smart" "-")
Fiona is cold.
Unknown
rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Fiona" "is" "cold" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Charlie is kind.[(triple1)] Fiona is rough.[(triple2)] Gary is not red.[(triple3)] @1: Charlie is white.[(((triple1) -> rule8))] @2: Charlie is cold.[(((((triple1) -> rule8)) -> rule4))] @3: Charlie is green.[(((((((triple1) -> rule8)) -> rule4)) -> rule3))] @4: Charlie is not red.[(((((((((triple1) -> rule8)) -> rule4)) -> rule3)) -> rule5))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple2
Gary is not red.
("Gary" "is" "red" "-")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not red.
("Charlie" "is" "red" "-")
((((((((triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4