Anne is furry. Anne is quiet. Bob is blue. Bob is furry. Bob is rough. Bob is smart. Dave is kind. Fiona is blue. Fiona is furry. Fiona is kind. Fiona is rough. Fiona is round. If someone is smart then they are rough. All quiet, furry people are smart. If someone is furry and rough then they are kind.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If someone is smart then they are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
All quiet, furry people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If someone is furry and rough then they are kind.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Fiona is round.
True
1
proof
[(triple12)]
("Fiona" "is" "round" "+")
triple12
Fiona is not kind.
False
1
inv-proof
[(triple10 OR ((triple9 triple11) -> rule3))]
("Fiona" "is" "kind" "-")
triple10
((triple9 triple11) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Bob is kind.
True
3
proof
[(((triple4 triple5) -> rule3) OR ((triple4 ((triple6) -> rule1)) -> rule3))]
("Bob" "is" "kind" "+")
((triple4 triple5) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple4 ((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Anne is not smart.
False
3
inv-proof
[(((triple2 triple1) -> rule2))]
("Anne" "is" "smart" "-")
((triple2 triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
True
4
proof
[(((((triple2 triple1) -> rule2)) -> rule1))]
("Anne" "is" "rough" "+")
((((triple2 triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not rough.
False
4
inv-proof
[(((((triple2 triple1) -> rule2)) -> rule1))]
("Anne" "is" "rough" "-")
((((triple2 triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
True
6
proof
[(((triple1 ((((triple2 triple1) -> rule2)) -> rule1)) -> rule3))]
("Anne" "is" "kind" "+")
((triple1 ((((triple2 triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not kind.
False
6
inv-proof
[(((triple1 ((((triple2 triple1) -> rule2)) -> rule1)) -> rule3))]
("Anne" "is" "kind" "-")
((triple1 ((((triple2 triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "smart" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "smart" "+")
Dave is not rough.
Unknown
inv-rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "rough" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Anne is furry.[(triple1)] Anne is quiet.[(triple2)] Bob is blue.[(triple3)] Bob is furry.[(triple4)] Bob is rough.[(triple5 OR ((triple6) -> rule1))] Bob is smart.[(triple6)] Dave is kind.[(triple7)] Fiona is blue.[(triple8)] Fiona is furry.[(triple9)] Fiona is kind.[(triple10 OR ((triple9 triple11) -> rule3))] Fiona is rough.[(triple11)] Fiona is round.[(triple12)] @1: Anne is smart.[(((triple2 triple1) -> rule2))] Bob is kind.[(((triple4 triple5) -> rule3) OR ((triple4 ((triple6) -> rule1)) -> rule3))] @2: Anne is rough.[(((((triple2 triple1) -> rule2)) -> rule1))] @3: Anne is kind.[(((triple1 ((((triple2 triple1) -> rule2)) -> rule1)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple6) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
Fiona is furry.
("Fiona" "is" "furry" "+")
triple9
Fiona is kind.
("Fiona" "is" "kind" "+")
triple10
((triple9 triple11) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple11
Fiona is round.
("Fiona" "is" "round" "+")
triple12
Anne is smart.
("Anne" "is" "smart" "+")
((triple2 triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple4 triple5) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple4 ((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((triple2 triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 ((((triple2 triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3