Dave is big. Dave is kind. Dave is nice. Dave is quiet. Dave is round. Dave is smart. Erin is big. Erin is kind. Erin is nice. Erin is quiet. Erin is round. Erin is smart. Harry is big. Harry is furry. Harry is kind. Harry is quiet. All round, furry people are smart. If Harry is quiet then Harry is round.
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
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 furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All round, furry people are smart.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If Harry is quiet then Harry is round.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "round" "+"))
Dave is round.
True
1
proof
[(triple5)]
("Dave" "is" "round" "+")
triple5
Erin is not big.
False
1
inv-proof
[(triple7)]
("Erin" "is" "big" "-")
triple7
Harry is round.
True
2
proof
[(((triple16) -> rule2))]
("Harry" "is" "round" "+")
((triple16) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple16) -> rule2))]
("Harry" "is" "round" "-")
((triple16) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
True
4
proof
[(((((triple16) -> rule2) triple14) -> rule1))]
("Harry" "is" "smart" "+")
((((triple16) -> (rule2 % int2)) triple14) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not smart.
False
4
inv-proof
[(((((triple16) -> rule2) triple14) -> rule1))]
("Harry" "is" "smart" "-")
((((triple16) -> (rule2 % int2)) triple14) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Dave is big.[(triple1)] Dave is kind.[(triple2)] Dave is nice.[(triple3)] Dave is quiet.[(triple4)] Dave is round.[(triple5)] Dave is smart.[(triple6)] Erin is big.[(triple7)] Erin is kind.[(triple8)] Erin is nice.[(triple9)] Erin is quiet.[(triple10)] Erin is round.[(triple11)] Erin is smart.[(triple12)] Harry is big.[(triple13)] Harry is furry.[(triple14)] Harry is kind.[(triple15)] Harry is quiet.[(triple16)] @1: Harry is round.[(((triple16) -> rule2))] @2: Harry is smart.[(((((triple16) -> rule2) triple14) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is nice.
("Erin" "is" "nice" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Harry is big.
("Harry" "is" "big" "+")
triple13
Harry is furry.
("Harry" "is" "furry" "+")
triple14
Harry is kind.
("Harry" "is" "kind" "+")
triple15
Harry is quiet.
("Harry" "is" "quiet" "+")
triple16
Harry is round.
("Harry" "is" "round" "+")
((triple16) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple16) -> (rule2 % int2)) triple14) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2