Anne is kind. Bob is young. Dave is kind. Harry is not rough. All young things are round. If something is smart and not young then it is not round. All young, kind things are not green. If something is round then it is not green. All kind things are rough. If Dave is not kind then Dave is smart.
Anne is kind.
("Anne" "is" "kind" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
All young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is smart and not young then it is not round.
((("something" "is" "smart" "+") ("something" "is" "young" "~")) -> ("something" "is" "round" "-"))
All young, kind things are not green.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "-"))
If something is round then it is not green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "-"))
All kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If Dave is not kind then Dave is smart.
((("Dave" "is" "kind" "~")) -> ("Dave" "is" "smart" "+"))
Dave is kind.
True
1
proof
[(triple3)]
("Dave" "is" "kind" "+")
triple3
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Bob is round.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "round" "+")
((triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple3) -> rule5))]
("Dave" "is" "rough" "-")
((triple3) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Bob is not green.
True
3
proof
[(((((triple2) -> rule1)) -> rule4))]
("Bob" "is" "green" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4))]
("Bob" "is" "green" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "smart" "+")
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "round" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is kind.[(triple1)] Bob is young.[(triple2)] Dave is kind.[(triple3)] Harry is not rough.[(triple4)] @1: Anne is rough.[(((triple1) -> rule5))] Bob is round.[(((triple2) -> rule1))] Dave is rough.[(((triple3) -> rule5))] @2: Bob is not green.[(((((triple2) -> rule1)) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Harry is not rough.
("Harry" "is" "rough" "-")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2