Anne is red. Dave is rough. Erin is cold. Fiona is green. Smart things are cold. If something is rough then it is cold. All green things are cold. If Erin is green and Erin is kind then Erin is nice. All smart, rough things are red. All green, cold things are nice. If something is smart then it is kind. Green, kind things are red.
Anne is red.
("Anne" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Smart things are cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If something is rough then it is cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If Erin is green and Erin is kind then Erin is nice.
((("Erin" "is" "green" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "nice" "+"))
All smart, rough things are red.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All green, cold things are nice.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is smart then it is kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Green, kind things are red.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Dave is rough.
True
1
proof
[(triple2)]
("Dave" "is" "rough" "+")
triple2
Dave is not rough.
False
1
inv-proof
[(triple2)]
("Dave" "is" "rough" "-")
triple2
Fiona is cold.
True
2
proof
[(((triple4) -> rule3))]
("Fiona" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "cold" "-")
((triple2) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Fiona is nice.
True
4
proof
[(((triple4 ((triple4) -> rule3)) -> rule6))]
("Fiona" "is" "nice" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not nice.
False
4
inv-proof
[(((triple4 ((triple4) -> rule3)) -> rule6))]
("Fiona" "is" "nice" "-")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "red" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "nice" "+")
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "kind" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Anne is red.[(triple1)] Dave is rough.[(triple2)] Erin is cold.[(triple3)] Fiona is green.[(triple4)] @1: Dave is cold.[(((triple2) -> rule2))] Fiona is cold.[(((triple4) -> rule3))] @2: Fiona is nice.[(((triple4 ((triple4) -> rule3)) -> rule6))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Fiona is green.
("Fiona" "is" "green" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2