Anne is cold. Anne is green. Anne is nice. Anne is rough. Anne is smart. Anne is white. Anne is young. Dave is green. Dave is nice. Dave is rough. Dave is smart. Dave is white. Dave is young. Harry is cold. Harry is rough. Harry is smart. If Dave is white and Dave is cold then Dave is nice. All smart people are rough.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Dave is white and Dave is cold then Dave is nice.
((("Dave" "is" "white" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "nice" "+"))
All smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Dave is young.
True
1
proof
[(triple13)]
("Dave" "is" "young" "+")
triple13
Harry is not smart.
False
1
inv-proof
[(triple16)]
("Harry" "is" "smart" "-")
triple16
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Anne is nice.[(triple3)] Anne is rough.[(triple4 OR ((triple5) -> rule2))] Anne is smart.[(triple5)] Anne is white.[(triple6)] Anne is young.[(triple7)] Dave is green.[(triple8)] Dave is nice.[(triple9)] Dave is rough.[(triple10 OR ((triple11) -> rule2))] Dave is smart.[(triple11)] Dave is white.[(triple12)] Dave is young.[(triple13)] Harry is cold.[(triple14)] Harry is rough.[(triple15 OR ((triple16) -> rule2))] Harry is smart.[(triple16)]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple5) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
Dave is green.
("Dave" "is" "green" "+")
triple8
Dave is nice.
("Dave" "is" "nice" "+")
triple9
Dave is rough.
("Dave" "is" "rough" "+")
triple10
((triple11) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple11
Dave is white.
("Dave" "is" "white" "+")
triple12
Dave is young.
("Dave" "is" "young" "+")
triple13
Harry is cold.
("Harry" "is" "cold" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
((triple16) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple16