Dave is big. Dave is green. Dave is not kind. Dave is red. Dave is not round. Dave is smart. Harry is not kind. Harry is red. Harry is smart. Harry is white. If something is smart then it is green. If Dave is white and Dave is red then Dave is big.
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is not round.
("Dave" "is" "round" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is smart then it is green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If Dave is white and Dave is red then Dave is big.
((("Dave" "is" "white" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "big" "+"))
Dave is smart.
True
1
proof
[(triple6)]
("Dave" "is" "smart" "+")
triple6
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Harry is green.
True
2
proof
[(((triple9) -> rule1))]
("Harry" "is" "green" "+")
((triple9) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple9) -> rule1))]
("Harry" "is" "green" "-")
((triple9) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Dave is big.[(triple1)] Dave is green.[(triple2 OR ((triple6) -> rule1))] Dave is not kind.[(triple3)] Dave is not round.[(triple5)] Dave is red.[(triple4)] Dave is smart.[(triple6)] Harry is not kind.[(triple7)] Harry is red.[(triple8)] Harry is smart.[(triple9)] Harry is white.[(triple10)] @1: Harry is green.[(((triple9) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
((triple6) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not kind.
("Dave" "is" "kind" "-")
triple3
Dave is not round.
("Dave" "is" "round" "-")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Harry is not kind.
("Harry" "is" "kind" "-")
triple7
Harry is red.
("Harry" "is" "red" "+")
triple8
Harry is smart.
("Harry" "is" "smart" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
((triple9) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1