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