Erin is big. Erin is blue. Erin is kind. Erin is nice. Erin is quiet. Erin is round. Erin is smart. Harry is big. Harry is kind. Harry is nice. Harry is quiet. Harry is round. If Erin is big then Erin is smart. If something is smart then it is quiet. If Harry is not blue then Harry is kind. If something is big and not blue then it is not nice. If something is quiet and not big then it is nice. If something is round then it is nice. If something is quiet and not smart then it is round. Kind things are round.
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
If Erin is big then Erin is smart.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "smart" "+"))
If something is smart then it is quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If Harry is not blue then Harry is kind.
((("Harry" "is" "blue" "~")) -> ("Harry" "is" "kind" "+"))
If something is big and not blue then it is not nice.
((("something" "is" "big" "+") ("something" "is" "blue" "~")) -> ("something" "is" "nice" "-"))
If something is quiet and not big then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "big" "~")) -> ("something" "is" "nice" "+"))
If something is round then it is nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If something is quiet and not smart then it is round.
((("something" "is" "quiet" "+") ("something" "is" "smart" "~")) -> ("something" "is" "round" "+"))
Kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Harry is quiet.
True
1
proof
[(triple11)]
("Harry" "is" "quiet" "+")
triple11
Erin is not big.
False
1
inv-proof
[(triple1)]
("Erin" "is" "big" "-")
triple1
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Erin is big.[(triple1)] Erin is blue.[(triple2)] Erin is kind.[(triple3)] Erin is nice.[(triple4 OR ((triple6) -> rule6) OR ((((triple3) -> rule8)) -> rule6))] Erin is quiet.[(triple5 OR ((triple7) -> rule2) OR ((((triple1) -> rule1)) -> rule2))] Erin is round.[(triple6 OR ((triple3) -> rule8))] Erin is smart.[(triple7 OR ((triple1) -> rule1))] Harry is big.[(triple8)] Harry is kind.[(triple9)] Harry is nice.[(triple10 OR ((triple12) -> rule6) OR ((((triple9) -> rule8)) -> rule6))] Harry is quiet.[(triple11)] Harry is round.[(triple12 OR ((triple9) -> rule8))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
((triple6) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
((triple7) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
triple6
((triple3) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple7
((triple1) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((triple12) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple9) -> (rule8 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
((triple9) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1