Charlie is not big. Charlie is green. Charlie is kind. Charlie is quiet. Dave is big. Dave is cold. Dave is furry. Dave is green. Dave is kind. Dave is round. Harry is big. Harry is not cold. Harry is furry. Harry is green. Harry is kind. Harry is round. All green people are quiet.
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
All green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Dave is big.
True
1
proof
[(triple5)]
("Dave" "is" "big" "+")
triple5
Charlie is not quiet.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule1))]
("Charlie" "is" "quiet" "-")
triple4
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is quiet.
True
2
proof
[(((triple8) -> rule1))]
("Dave" "is" "quiet" "+")
((triple8) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple8) -> rule1))]
("Dave" "is" "quiet" "-")
((triple8) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is green.[(triple2)] Charlie is kind.[(triple3)] Charlie is not big.[(triple1)] Charlie is quiet.[(triple4 OR ((triple2) -> rule1))] Dave is big.[(triple5)] Dave is cold.[(triple6)] Dave is furry.[(triple7)] Dave is green.[(triple8)] Dave is kind.[(triple9)] Dave is round.[(triple10)] Harry is big.[(triple11)] Harry is furry.[(triple13)] Harry is green.[(triple14)] Harry is kind.[(triple15)] Harry is not cold.[(triple12)] Harry is round.[(triple16)] @1: Dave is quiet.[(((triple8) -> rule1))] Harry is quiet.[(((triple14) -> rule1))]
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is not big.
("Charlie" "is" "big" "-")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple6
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Dave is green.
("Dave" "is" "green" "+")
triple8
Dave is kind.
("Dave" "is" "kind" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is green.
("Harry" "is" "green" "+")
triple14
Harry is kind.
("Harry" "is" "kind" "+")
triple15
Harry is not cold.
("Harry" "is" "cold" "-")
triple12
Harry is round.
("Harry" "is" "round" "+")
triple16
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple8) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple14) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1