Dave is big. Dave is not kind. Dave is quiet. Dave is not red. Dave is smart. Erin is big. Erin is not cold. Erin is not kind. Erin is smart. Erin is not young. Gary is big. Gary is cold. Gary is quiet. Gary is not red. Gary is smart. Gary is young. If someone is kind then they are big. All kind, young people are smart. All quiet, kind people are red. All red people are not young. If Gary is kind and Gary is red then Gary is cold. If someone is young then they are quiet. All kind, cold people are quiet. Smart, quiet people are not kind.
Dave is big.
("Dave" "is" "big" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is not young.
("Erin" "is" "young" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not red.
("Gary" "is" "red" "-")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
All kind, young people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All quiet, kind people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All red people are not young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "-"))
If Gary is kind and Gary is red then Gary is cold.
((("Gary" "is" "kind" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "cold" "+"))
If someone is young then they are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
All kind, cold people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Smart, quiet people are not kind.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "-"))
Erin is not young.
True
1
proof
[(triple10)]
("Erin" "is" "young" "-")
triple10
Dave is kind.
False
1
inv-proof
[(triple2 OR ((triple5 triple3) -> rule8))]
("Dave" "is" "kind" "+")
triple2
((triple5 triple3) -> (rule8 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Gary is not kind.
True
3
proof
[(((triple15 triple13) -> rule8) OR ((triple15 ((triple16) -> rule6)) -> rule8))]
("Gary" "is" "kind" "-")
((triple15 triple13) -> (rule8 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
((triple15 ((triple16) -> (rule6 % int2))) -> (rule8 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is kind.
False
3
inv-proof
[(((triple15 triple13) -> rule8) OR ((triple15 ((triple16) -> rule6)) -> rule8))]
("Gary" "is" "kind" "+")
((triple15 triple13) -> (rule8 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
((triple15 ((triple16) -> (rule6 % int2))) -> (rule8 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "quiet" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Dave is big.[(triple1)] Dave is not kind.[(triple2 OR ((triple5 triple3) -> rule8))] Dave is not red.[(triple4)] Dave is quiet.[(triple3)] Dave is smart.[(triple5)] Erin is big.[(triple6)] Erin is not cold.[(triple7)] Erin is not kind.[(triple8)] Erin is not young.[(triple10)] Erin is smart.[(triple9)] Gary is big.[(triple11)] Gary is cold.[(triple12)] Gary is not red.[(triple14)] Gary is quiet.[(triple13 OR ((triple16) -> rule6))] Gary is smart.[(triple15)] Gary is young.[(triple16)] @1: Gary is not kind.[(((triple15 triple13) -> rule8) OR ((triple15 ((triple16) -> rule6)) -> rule8))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is not kind.
("Dave" "is" "kind" "-")
triple2
((triple5 triple3) -> (rule8 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is not red.
("Dave" "is" "red" "-")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is not cold.
("Erin" "is" "cold" "-")
triple7
Erin is not kind.
("Erin" "is" "kind" "-")
triple8
Erin is not young.
("Erin" "is" "young" "-")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple9
Gary is big.
("Gary" "is" "big" "+")
triple11
Gary is cold.
("Gary" "is" "cold" "+")
triple12
Gary is not red.
("Gary" "is" "red" "-")
triple14
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
((triple16) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Gary is not kind.
("Gary" "is" "kind" "-")
((triple15 triple13) -> (rule8 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
((triple15 ((triple16) -> (rule6 % int2))) -> (rule8 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2