Anne is big. Anne is furry. Anne is kind. Anne is rough. Anne is smart. Anne is young. Charlie is big. Charlie is blue. Charlie is furry. Charlie is kind. Dave is rough. Dave is smart. Dave is young. Erin is furry. Erin is smart. If Anne is big then Anne is young. If something is smart then it is furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If Anne is big then Anne is young.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "young" "+"))
If something is smart then it is furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Dave is not rough.
False
1
inv-proof
[(triple11)]
("Dave" "is" "rough" "-")
triple11
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2 OR ((triple5) -> rule2))] Anne is kind.[(triple3)] Anne is rough.[(triple4)] Anne is smart.[(triple5)] Anne is young.[(triple6 OR ((triple1) -> rule1))] Charlie is big.[(triple7)] Charlie is blue.[(triple8)] Charlie is furry.[(triple9)] Charlie is kind.[(triple10)] Dave is rough.[(triple11)] Dave is smart.[(triple12)] Dave is young.[(triple13)] Erin is furry.[(triple14 OR ((triple15) -> rule2))] Erin is smart.[(triple15)] @1: Dave is furry.[(((triple12) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple5) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is young.
("Anne" "is" "young" "+")
triple6
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
Charlie is kind.
("Charlie" "is" "kind" "+")
triple10
Dave is rough.
("Dave" "is" "rough" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
triple12
Dave is young.
("Dave" "is" "young" "+")
triple13
Erin is furry.
("Erin" "is" "furry" "+")
triple14
((triple15) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple15
Dave is furry.
("Dave" "is" "furry" "+")
((triple12) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1