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