Charlie is kind. Dave is red. Erin is cold. Fiona is white. All cold things are red. If Dave is young then Dave is red. If Fiona is young and Fiona is kind then Fiona is rough. Rough, green things are red. Green, red things are kind. Kind, rough things are red. All green, red things are cold. If something is rough and white then it is cold.
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Fiona is white.
("Fiona" "is" "white" "+")
All cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If Dave is young then Dave is red.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "red" "+"))
If Fiona is young and Fiona is kind then Fiona is rough.
((("Fiona" "is" "young" "+") ("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "rough" "+"))
Rough, green things are red.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Green, red things are kind.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Kind, rough things are red.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All green, red things are cold.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is rough and white then it is cold.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Charlie is kind.
True
1
proof
[(triple1)]
("Charlie" "is" "kind" "+")
triple1
Dave is not red.
False
1
inv-proof
[(triple2)]
("Dave" "is" "red" "-")
triple2
Erin is red.
True
2
proof
[(((triple3) -> rule1))]
("Erin" "is" "red" "+")
((triple3) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple3) -> rule1))]
("Erin" "is" "red" "-")
((triple3) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Fiona is not red.
Unknown
inv-rconc
[@3: Fiona is red.[CWA. Example of deepest failure = (rule1 <- rule8 <- rule3 <- FAIL)]]
("Fiona" "is" "red" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "cold" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Charlie is kind.[(triple1)] Dave is red.[(triple2)] Erin is cold.[(triple3)] Fiona is white.[(triple4)] @1: Erin is red.[(((triple3) -> rule1))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Fiona is white.
("Fiona" "is" "white" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
((triple3) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1