Anne is not quiet. Dave is smart. Erin is young. Gary is nice. Nice, red things are kind. All young, red things are kind. If Erin is nice and Erin is smart then Erin is kind. All red things are not quiet. Smart things are nice. Smart things are red.
Anne is not quiet.
("Anne" "is" "quiet" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Nice, red things are kind.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
All young, red things are kind.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If Erin is nice and Erin is smart then Erin is kind.
((("Erin" "is" "nice" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "kind" "+"))
All red things are not quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "-"))
Smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Anne is not quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Anne is quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Dave is red.
True
2
proof
[(((triple2) -> rule6))]
("Dave" "is" "red" "+")
((triple2) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple2) -> rule5))]
("Dave" "is" "nice" "-")
((triple2) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
True
5
proof
[(((((triple2) -> rule5) ((triple2) -> rule6)) -> rule1))]
("Dave" "is" "kind" "+")
((((triple2) -> (rule5 % int3)) ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is quiet.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule4))]
("Dave" "is" "quiet" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "nice" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "nice" "+")
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Gary" "is" "kind" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Anne is not quiet.[(triple1)] Dave is smart.[(triple2)] Erin is young.[(triple3)] Gary is nice.[(triple4)] @1: Dave is nice.[(((triple2) -> rule5))] Dave is red.[(((triple2) -> rule6))] @2: Dave is kind.[(((((triple2) -> rule5) ((triple2) -> rule6)) -> rule1))] Dave is not quiet.[(((((triple2) -> rule6)) -> rule4))]
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple2) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple2) -> (rule5 % int3)) ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not quiet.
("Dave" "is" "quiet" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2