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