Anne is kind. Bob is round. Erin is quiet. If someone is smart and cold then they are rough. Round people are quiet. All kind, red people are cold. If Bob is round and Bob is red then Bob is smart. All round, quiet people are kind. All round, red people are rough.
Anne is kind.
("Anne" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
If someone is smart and cold then they are rough.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
Round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
All kind, red people are cold.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If Bob is round and Bob is red then Bob is smart.
((("Bob" "is" "round" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "smart" "+"))
All round, quiet people are kind.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
All round, red people are rough.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Bob is quiet.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule5))]
("Bob" "is" "kind" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not kind.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule5))]
("Bob" "is" "kind" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Bob" "is" "rough" "-")
Anne is cold.
Unknown
rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "cold" "+")
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Anne is kind.[(triple1)] Bob is round.[(triple2)] Erin is quiet.[(triple3)] @1: Bob is quiet.[(((triple2) -> rule2))] @2: Bob is kind.[(((triple2 ((triple2) -> rule2)) -> rule5))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2