Dave is kind. Dave is quiet. Dave is red. Dave is not rough. Dave is round. Dave is white. Dave is young. Erin is kind. Erin is red. Erin is rough. Erin is round. Erin is white. Harry is quiet. Harry is rough. Harry is white. Harry is young. If Harry is not rough then Harry is quiet. All kind people are red. If someone is red and not kind then they are not young. All white people are quiet. If someone is young and not red then they are white. If someone is rough and not young then they are white.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is not rough then Harry is quiet.
((("Harry" "is" "rough" "~")) -> ("Harry" "is" "quiet" "+"))
All kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If someone is red and not kind then they are not young.
((("someone" "is" "red" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "young" "-"))
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is young and not red then they are white.
((("someone" "is" "young" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "white" "+"))
If someone is rough and not young then they are white.
((("someone" "is" "rough" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "white" "+"))
Erin is round.
True
1
proof
[(triple11)]
("Erin" "is" "round" "+")
triple11
Harry is not quiet.
False
1
inv-proof
[(triple13 OR ((triple15) -> rule4))]
("Harry" "is" "quiet" "-")
triple13
((triple15) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Dave is kind.[(triple1)] Dave is not rough.[(triple4)] Dave is quiet.[(triple2 OR ((triple6) -> rule4))] Dave is red.[(triple3 OR ((triple1) -> rule2))] Dave is round.[(triple5)] Dave is white.[(triple6)] Dave is young.[(triple7)] Erin is kind.[(triple8)] Erin is red.[(triple9 OR ((triple8) -> rule2))] Erin is rough.[(triple10)] Erin is round.[(triple11)] Erin is white.[(triple12)] Harry is quiet.[(triple13 OR ((triple15) -> rule4))] Harry is rough.[(triple14)] Harry is white.[(triple15)] Harry is young.[(triple16)] @1: Erin is quiet.[(((triple12) -> rule4))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Dave is not rough.
("Dave" "is" "rough" "-")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
((triple6) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple3
((triple1) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is red.
("Erin" "is" "red" "+")
triple9
((triple8) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
Erin is white.
("Erin" "is" "white" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
((triple15) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple12) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1