Anne is round. Anne is smart. Anne is young. Bob is furry. Bob is green. Bob is rough. Bob is round. Bob is smart. Bob is young. Dave is green. Dave is kind. Dave is rough. If someone is rough then they are young.
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
If someone is rough then they are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
Bob is furry.
True
1
proof
[(triple4)]
("Bob" "is" "furry" "+")
triple4
Dave is not kind.
False
1
inv-proof
[(triple11)]
("Dave" "is" "kind" "-")
triple11
Dave is young.
True
2
proof
[(((triple12) -> rule1))]
("Dave" "is" "young" "+")
((triple12) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple12) -> rule1))]
("Dave" "is" "young" "-")
((triple12) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Anne is round.[(triple1)] Anne is smart.[(triple2)] Anne is young.[(triple3)] Bob is furry.[(triple4)] Bob is green.[(triple5)] Bob is rough.[(triple6)] Bob is round.[(triple7)] Bob is smart.[(triple8)] Bob is young.[(triple9 OR ((triple6) -> rule1))] Dave is green.[(triple10)] Dave is kind.[(triple11)] Dave is rough.[(triple12)] @1: Dave is young.[(((triple12) -> rule1))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
triple5
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Bob is round.
("Bob" "is" "round" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
triple8
Bob is young.
("Bob" "is" "young" "+")
triple9
((triple6) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple10
Dave is kind.
("Dave" "is" "kind" "+")
triple11
Dave is rough.
("Dave" "is" "rough" "+")
triple12
Dave is young.
("Dave" "is" "young" "+")
((triple12) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1