Anne is rough. Charlie is cold. Fiona is cold. Gary is green. If Anne is rough then Anne is cold. All rough, cold things are kind. Kind, cold things are nice. If something is kind and cold then it is nice. If something is cold and rough then it is nice. All round, rough things are quiet.
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
If Anne is rough then Anne is cold.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "cold" "+"))
All rough, cold things are kind.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Kind, cold things are nice.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is kind and cold then it is nice.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is cold and rough then it is nice.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All round, rough things are quiet.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Anne is cold.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("Anne" "is" "kind" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not kind.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("Anne" "is" "kind" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Fiona is not nice.
Unknown
inv-rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Fiona" "is" "nice" "-")
Gary is quiet.
Unknown
rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "quiet" "+")
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is rough.[(triple1)] Charlie is cold.[(triple2)] Fiona is cold.[(triple3)] Gary is green.[(triple4)] @1: Anne is cold.[(((triple1) -> rule1))] @2: Anne is kind.[(((triple1 ((triple1) -> rule1)) -> rule2))] Anne is nice.[(((((triple1) -> rule1) triple1) -> rule5) OR ((((triple1 ((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule3) OR ((((triple1 ((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule4))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int3))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3