Charlie is red. Fiona is kind. If someone is kind then they are red. All red people are blue. If Charlie is kind and Charlie is red then Charlie is white. All blue people are red. If Charlie is red and Charlie is rough then Charlie is kind. Rough, red people are kind.
Charlie is red.
("Charlie" "is" "red" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
If someone is kind then they are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is kind and Charlie is red then Charlie is white.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "red" "+")) -> ("Charlie" "is" "white" "+"))
All blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If Charlie is red and Charlie is rough then Charlie is kind.
((("Charlie" "is" "red" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "kind" "+"))
Rough, red people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Fiona is kind.
True
1
proof
[(triple2)]
("Fiona" "is" "kind" "+")
triple2
Charlie is not red.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "red" "-")
triple1
Charlie is blue.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "blue" "-")
((triple1) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Fiona is blue.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("Fiona" "is" "blue" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not blue.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("Fiona" "is" "blue" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is white.
Unknown
rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Charlie" "is" "white" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is red.[(triple1)] Fiona is kind.[(triple2)] @1: Charlie is blue.[(((triple1) -> rule2))] Fiona is red.[(((triple2) -> rule1))] @2: Fiona is blue.[(((((triple2) -> rule1)) -> rule2))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple2) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2