Dave is green. Dave is quiet. Dave is red. Dave is young. Erin is green. Erin is rough. Erin is young. Gary is furry. Gary is quiet. Gary is red. If Erin is green then Erin is furry. If someone is red and furry then they are quiet. If someone is white and green then they are young. All quiet people are green. If Gary is red and Gary is white then Gary is green. Furry, young people are rough.
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
If Erin is green then Erin is furry.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "furry" "+"))
If someone is red and furry then they are quiet.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is white and green then they are young.
((("someone" "is" "white" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If Gary is red and Gary is white then Gary is green.
((("Gary" "is" "red" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "green" "+"))
Furry, young people are rough.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
Gary is red.
True
1
proof
[(triple10)]
("Gary" "is" "red" "+")
triple10
Erin is not green.
False
1
inv-proof
[(triple5)]
("Erin" "is" "green" "-")
triple5
Gary is not rough.
Unknown
inv-rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Gary" "is" "rough" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Dave is green.[(triple1 OR ((triple2) -> rule4))] Dave is quiet.[(triple2)] Dave is red.[(triple3)] Dave is young.[(triple4)] Erin is green.[(triple5)] Erin is rough.[(triple6 OR ((((triple5) -> rule1) triple7) -> rule6))] Erin is young.[(triple7)] Gary is furry.[(triple8)] Gary is quiet.[(triple9 OR ((triple10 triple8) -> rule2))] Gary is red.[(triple10)] @1: Erin is furry.[(((triple5) -> rule1))] Gary is green.[(((triple9) -> rule4) OR ((((triple10 triple8) -> rule2)) -> rule4))]
Dave is green.
("Dave" "is" "green" "+")
triple1
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is rough.
("Erin" "is" "rough" "+")
triple6
((((triple5) -> (rule1 % int2)) triple7) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
((triple10 triple8) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple10
Erin is furry.
("Erin" "is" "furry" "+")
((triple5) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple9) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple10 triple8) -> (rule2 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2