Dave is young. Gary is quiet. All red, white things are quiet. If something is green then it is young. If something is kind and white then it is blue. Quiet things are red. If something is quiet and blue then it is white. Quiet, red things are young. Quiet things are green. If Dave is red and Dave is green then Dave is quiet.
Dave is young.
("Dave" "is" "young" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
All red, white things are quiet.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is green then it is young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is kind and white then it is blue.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If something is quiet and blue then it is white.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Quiet, red things are young.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If Dave is red and Dave is green then Dave is quiet.
((("Dave" "is" "red" "+") ("Dave" "is" "green" "+")) -> ("Dave" "is" "quiet" "+"))
Gary is quiet.
True
1
proof
[(triple2)]
("Gary" "is" "quiet" "+")
triple2
Gary is not quiet.
False
1
inv-proof
[(triple2)]
("Gary" "is" "quiet" "-")
triple2
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Dave is young.[(triple1)] Gary is quiet.[(triple2)] @1: Gary is green.[(((triple2) -> rule7))] Gary is red.[(((triple2) -> rule4))] @2: Gary is young.[(((((triple2) -> rule7)) -> rule2) OR ((triple2 ((triple2) -> rule4)) -> rule6))]
Dave is young.
("Dave" "is" "young" "+")
triple1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
((triple2) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple2) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((triple2 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2