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