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