Dave is kind. If something is green then it is blue. All kind things are young. If Dave is kind and Dave is young then Dave is green. Young, quiet things are furry. Quiet things are furry. If something is quiet and green then it is kind. All kind things are blue. Blue, young things are smart.
Dave is kind.
("Dave" "is" "kind" "+")
If something is green then it is blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If Dave is kind and Dave is young then Dave is green.
((("Dave" "is" "kind" "+") ("Dave" "is" "young" "+")) -> ("Dave" "is" "green" "+"))
Young, quiet things are furry.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If something is quiet and green then it is kind.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Blue, young things are smart.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Dave is kind.
True
1
proof
[(triple1)]
("Dave" "is" "kind" "+")
triple1
Dave is not kind.
False
1
inv-proof
[(triple1)]
("Dave" "is" "kind" "-")
triple1
Dave is blue.
True
2
proof
[(((triple1) -> rule7) OR ((((triple1 ((triple1) -> rule2)) -> rule3)) -> rule1))]
("Dave" "is" "blue" "+")
((triple1) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not blue.
False
2
inv-proof
[(((triple1) -> rule7) OR ((((triple1 ((triple1) -> rule2)) -> rule3)) -> rule1))]
("Dave" "is" "blue" "-")
((triple1) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is kind.[(triple1)] @1: Dave is blue.[(((triple1) -> rule7) OR ((((triple1 ((triple1) -> rule2)) -> rule3)) -> rule1))] Dave is young.[(((triple1) -> rule2))] @2: Dave is green.[(((triple1 ((triple1) -> rule2)) -> rule3))] Dave is smart.[(((((triple1) -> rule7) ((triple1) -> rule2)) -> rule8) OR ((((((triple1 ((triple1) -> rule2)) -> rule3)) -> rule1) ((triple1) -> rule2)) -> rule8))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
((triple1) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((triple1) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple1) -> (rule7 % int3)) ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((((triple1 ((triple1) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int4))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4