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