Anne is round. Charlie is rough. Dave is big. Erin is quiet. All green, big people are rough. Quiet people are smart. Nice, smart people are rough.
Anne is round.
("Anne" "is" "round" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
All green, big people are rough.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Nice, smart people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Erin is quiet.
True
1
proof
[(triple4)]
("Erin" "is" "quiet" "+")
triple4
Charlie is not rough.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "rough" "-")
triple2
Erin is smart.
True
2
proof
[(((triple4) -> rule2))]
("Erin" "is" "smart" "+")
((triple4) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple4) -> rule2))]
("Erin" "is" "smart" "-")
((triple4) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "smart" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "rough" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is round.[(triple1)] Charlie is rough.[(triple2)] Dave is big.[(triple3)] Erin is quiet.[(triple4)] @1: Erin is smart.[(((triple4) -> rule2))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is smart.
("Erin" "is" "smart" "+")
((triple4) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1