Anne is furry. Anne is rough. Anne is smart. Anne is young. Bob is big. Bob is furry. Bob is not green. Bob is not nice. Bob is young. Charlie is big. Charlie is not green. Charlie is not nice. Charlie is rough. Charlie is smart. Charlie is young. Furry, big things are young. If Anne is nice and Anne is furry then Anne is not young. All young, big things are furry. If something is young then it is big. Nice, furry things are not green. If Anne is rough and Anne is not furry then Anne is smart.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is young.
("Bob" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Furry, big things are young.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If Anne is nice and Anne is furry then Anne is not young.
((("Anne" "is" "nice" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "young" "-"))
All young, big things are furry.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is young then it is big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Nice, furry things are not green.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "-"))
If Anne is rough and Anne is not furry then Anne is smart.
((("Anne" "is" "rough" "+") ("Anne" "is" "furry" "~")) -> ("Anne" "is" "smart" "+"))
Bob is not nice.
True
1
proof
[(triple8)]
("Bob" "is" "nice" "-")
triple8
Charlie is not rough.
False
1
inv-proof
[(triple13)]
("Charlie" "is" "rough" "-")
triple13
Charlie is furry.
True
3
proof
[(((triple15 triple10) -> rule3) OR ((triple15 ((triple15) -> rule4)) -> rule3))]
("Charlie" "is" "furry" "+")
((triple15 triple10) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple15 ((triple15) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not furry.
False
3
inv-proof
[(((triple15 triple10) -> rule3) OR ((triple15 ((triple15) -> rule4)) -> rule3))]
("Charlie" "is" "furry" "-")
((triple15 triple10) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple15 ((triple15) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Anne is furry.[(triple1 OR ((triple4 ((triple4) -> rule4)) -> rule3))] Anne is rough.[(triple2)] Anne is smart.[(triple3)] Anne is young.[(triple4)] Bob is big.[(triple5 OR ((triple9) -> rule4))] Bob is furry.[(triple6 OR ((triple9 triple5) -> rule3) OR ((triple9 ((triple9) -> rule4)) -> rule3))] Bob is not green.[(triple7)] Bob is not nice.[(triple8)] Bob is young.[(triple9 OR ((triple6 triple5) -> rule1))] Charlie is big.[(triple10 OR ((triple15) -> rule4))] Charlie is not green.[(triple11)] Charlie is not nice.[(triple12)] Charlie is rough.[(triple13)] Charlie is smart.[(triple14)] Charlie is young.[(triple15)] @1: Anne is big.[(((triple4) -> rule4))] Charlie is furry.[(((triple15 triple10) -> rule3) OR ((triple15 ((triple15) -> rule4)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple4 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
triple5
((triple9) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple6
((triple9 triple5) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple9 ((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not green.
("Bob" "is" "green" "-")
triple7
Bob is not nice.
("Bob" "is" "nice" "-")
triple8
Bob is young.
("Bob" "is" "young" "+")
triple9
((triple6 triple5) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple10
((triple15) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not green.
("Charlie" "is" "green" "-")
triple11
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple12
Charlie is rough.
("Charlie" "is" "rough" "+")
triple13
Charlie is smart.
("Charlie" "is" "smart" "+")
triple14
Charlie is young.
("Charlie" "is" "young" "+")
triple15
Anne is big.
("Anne" "is" "big" "+")
((triple4) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple15 triple10) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple15 ((triple15) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2