Dave is nice. Erin is smart. Gary is green. If someone is quiet then they are green. All green, quiet people are smart. If Dave is blue then Dave is red. If someone is green then they are quiet. If Gary is nice then Gary is blue. If someone is green then they are nice.
Dave is nice.
("Dave" "is" "nice" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is green.
("Gary" "is" "green" "+")
If someone is quiet then they are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
All green, quiet people are smart.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If Dave is blue then Dave is red.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "red" "+"))
If someone is green then they are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is nice then Gary is blue.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "blue" "+"))
If someone is green then they are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Gary is green.
True
1
proof
[(triple3)]
("Gary" "is" "green" "+")
triple3
Gary is not green.
False
1
inv-proof
[(triple3)]
("Gary" "is" "green" "-")
triple3
Gary is nice.
True
2
proof
[(((triple3) -> rule6))]
("Gary" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple3) -> rule4))]
("Gary" "is" "quiet" "-")
((triple3) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
True
3
proof
[(((((triple3) -> rule6)) -> rule5))]
("Gary" "is" "blue" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule5))]
("Gary" "is" "blue" "-")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Dave is not smart.
Unknown
inv-rconc
[@3: Dave is smart.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule4 <- FAIL)]]
("Dave" "is" "smart" "-")
Erin is quiet.
Unknown
rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Erin" "is" "quiet" "+")
Dave is not quiet.
Unknown
inv-rconc
[@2: Dave is quiet.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Dave" "is" "quiet" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Dave is nice.[(triple1)] Erin is smart.[(triple2)] Gary is green.[(triple3)] @1: Gary is nice.[(((triple3) -> rule6))] Gary is quiet.[(((triple3) -> rule4))] @2: Gary is blue.[(((((triple3) -> rule6)) -> rule5))] Gary is smart.[(((triple3 ((triple3) -> rule4)) -> rule2))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2