Anne is kind. Charlie is big. Charlie is smart. Dave is kind. Dave is smart. Erin is nice. Erin is quiet. If Anne is big then Anne is kind. All smart things are quiet. Cold, quiet things are nice.
Anne is kind.
("Anne" "is" "kind" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
If Anne is big then Anne is kind.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "kind" "+"))
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Cold, quiet things are nice.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
Erin is nice.
True
1
proof
[(triple6)]
("Erin" "is" "nice" "+")
triple6
Erin is not quiet.
False
1
inv-proof
[(triple7)]
("Erin" "is" "quiet" "-")
triple7
Charlie is quiet.
True
2
proof
[(((triple3) -> rule2))]
("Charlie" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple5) -> rule2))]
("Dave" "is" "quiet" "-")
((triple5) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "nice" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "nice" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Anne is kind.[(triple1)] Charlie is big.[(triple2)] Charlie is smart.[(triple3)] Dave is kind.[(triple4)] Dave is smart.[(triple5)] Erin is nice.[(triple6)] Erin is quiet.[(triple7)] @1: Charlie is quiet.[(((triple3) -> rule2))] Dave is quiet.[(((triple5) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple5) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1