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