Dave is kind. Dave is quiet. Dave is not rough. Dave is round. Erin is blue. Erin is kind. Erin is not rough. Erin is round. Erin is young. Harry is blue. Harry is nice. Harry is quiet. Harry is rough. Harry is round. Harry is young. If something is kind and not quiet then it is rough. If Erin is blue then Erin is not nice. If Erin is young then Erin is not nice. If something is round and young then it is blue. All quiet things are blue. If Dave is kind and Dave is not young then Dave is round.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is round.
("Dave" "is" "round" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is kind and not quiet then it is rough.
((("something" "is" "kind" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "rough" "+"))
If Erin is blue then Erin is not nice.
((("Erin" "is" "blue" "+")) -> ("Erin" "is" "nice" "-"))
If Erin is young then Erin is not nice.
((("Erin" "is" "young" "+")) -> ("Erin" "is" "nice" "-"))
If something is round and young then it is blue.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If Dave is kind and Dave is not young then Dave is round.
((("Dave" "is" "kind" "+") ("Dave" "is" "young" "~")) -> ("Dave" "is" "round" "+"))
Erin is not rough.
True
1
proof
[(triple7)]
("Erin" "is" "rough" "-")
triple7
Dave is rough.
False
1
inv-proof
[(triple3)]
("Dave" "is" "rough" "+")
triple3
Dave is blue.
True
2
proof
[(((triple2) -> rule5))]
("Dave" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple2) -> rule5))]
("Dave" "is" "blue" "-")
((triple2) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Dave is kind.[(triple1)] Dave is not rough.[(triple3)] Dave is quiet.[(triple2)] Dave is round.[(triple4)] Erin is blue.[(triple5 OR ((triple8 triple9) -> rule4))] Erin is kind.[(triple6)] Erin is not rough.[(triple7)] Erin is round.[(triple8)] Erin is young.[(triple9)] Harry is blue.[(triple10 OR ((triple12) -> rule5) OR ((triple14 triple15) -> rule4))] Harry is nice.[(triple11)] Harry is quiet.[(triple12)] Harry is rough.[(triple13)] Harry is round.[(triple14)] Harry is young.[(triple15)] @1: Dave is blue.[(((triple2) -> rule5))] Erin is not nice.[(((triple5) -> rule2) OR ((triple9) -> rule3) OR ((((triple8 triple9) -> rule4)) -> rule2))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Dave is not rough.
("Dave" "is" "rough" "-")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
((triple8 triple9) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Erin is not rough.
("Erin" "is" "rough" "-")
triple7
Erin is round.
("Erin" "is" "round" "+")
triple8
Erin is young.
("Erin" "is" "young" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple10
((triple12) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple14 triple15) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
((triple5) -> (rule2 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
((triple9) -> (rule3 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
((((triple8 triple9) -> (rule4 % int2))) -> (rule2 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2