Anne is smart. Dave is kind. Dave is nice. Dave is round. Erin is kind. Erin is nice. Gary is smart. All smart, round people are green. If Anne is nice and Anne is smart then Anne is round. Kind people are smart. All kind, smart people are red. All nice, quiet people are green. All green, round people are smart.
Anne is smart.
("Anne" "is" "smart" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All smart, round people are green.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If Anne is nice and Anne is smart then Anne is round.
((("Anne" "is" "nice" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "round" "+"))
Kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
All kind, smart people are red.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
All nice, quiet people are green.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
All green, round people are smart.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Erin is nice.
True
1
proof
[(triple6)]
("Erin" "is" "nice" "+")
triple6
Gary is not smart.
False
1
inv-proof
[(triple7)]
("Gary" "is" "smart" "-")
triple7
Erin is smart.
True
2
proof
[(((triple5) -> rule3))]
("Erin" "is" "smart" "+")
((triple5) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple5) -> rule3))]
("Erin" "is" "smart" "-")
((triple5) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Dave is green.
True
4
proof
[(((((triple2) -> rule3) triple4) -> rule1))]
("Dave" "is" "green" "+")
((((triple2) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Erin is not red.
False
4
inv-proof
[(((triple5 ((triple5) -> rule3)) -> rule4))]
("Erin" "is" "red" "-")
((triple5 ((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Anne is not green.
Unknown
inv-rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "round" "+")
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "red" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Anne is smart.[(triple1)] Dave is kind.[(triple2)] Dave is nice.[(triple3)] Dave is round.[(triple4)] Erin is kind.[(triple5)] Erin is nice.[(triple6)] Gary is smart.[(triple7)] @1: Dave is smart.[(((triple2) -> rule3))] Erin is smart.[(((triple5) -> rule3))] @2: Dave is green.[(((((triple2) -> rule3) triple4) -> rule1))] Dave is red.[(((triple2 ((triple2) -> rule3)) -> rule4))] Erin is red.[(((triple5 ((triple5) -> rule3)) -> rule4))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple5) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple2) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((triple5 ((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2