Erin is kind. Fiona is red. Harry is rough. All green things are kind. All cold, green things are kind. If something is red then it is cold. If Fiona is cold then Fiona is blue. All red things are rough. If something is blue then it is not quiet.
Erin is kind.
("Erin" "is" "kind" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
All cold, green things are kind.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If Fiona is cold then Fiona is blue.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "blue" "+"))
All red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is blue then it is not quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "-"))
Harry is rough.
True
1
proof
[(triple3)]
("Harry" "is" "rough" "+")
triple3
Fiona is not red.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "red" "-")
triple2
Fiona is cold.
True
2
proof
[(((triple2) -> rule3))]
("Fiona" "is" "cold" "+")
((triple2) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is not rough.
False
2
inv-proof
[(((triple2) -> rule5))]
("Fiona" "is" "rough" "-")
((triple2) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is blue.
True
3
proof
[(((((triple2) -> rule3)) -> rule4))]
("Fiona" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not blue.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule4))]
("Fiona" "is" "blue" "-")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not quiet.
True
4
proof
[(((((((triple2) -> rule3)) -> rule4)) -> rule6))]
("Fiona" "is" "quiet" "-")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is quiet.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule4)) -> rule6))]
("Fiona" "is" "quiet" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "kind" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "cold" "+")
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "cold" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Erin is kind.[(triple1)] Fiona is red.[(triple2)] Harry is rough.[(triple3)] @1: Fiona is cold.[(((triple2) -> rule3))] Fiona is rough.[(((triple2) -> rule5))] @2: Fiona is blue.[(((((triple2) -> rule3)) -> rule4))] @3: Fiona is not quiet.[(((((((triple2) -> rule3)) -> rule4)) -> rule6))]
Erin is kind.
("Erin" "is" "kind" "+")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple2) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple2) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3