Dave is red. Harry is kind. Harry is round. If someone is round then they are big. If someone is red then they are kind. If Dave is kind then Dave is quiet. All kind people are round. If someone is round and not young then they are green. If Dave is not kind and Dave is not quiet then Dave is big. If Dave is quiet and Dave is round then Dave is big. If Dave is not young and Dave is not quiet then Dave is big.
Dave is red.
("Dave" "is" "red" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is round then they are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is red then they are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If Dave is kind then Dave is quiet.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "quiet" "+"))
All kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If someone is round and not young then they are green.
((("someone" "is" "round" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "green" "+"))
If Dave is not kind and Dave is not quiet then Dave is big.
((("Dave" "is" "kind" "~") ("Dave" "is" "quiet" "~")) -> ("Dave" "is" "big" "+"))
If Dave is quiet and Dave is round then Dave is big.
((("Dave" "is" "quiet" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "big" "+"))
If Dave is not young and Dave is not quiet then Dave is big.
((("Dave" "is" "young" "~") ("Dave" "is" "quiet" "~")) -> ("Dave" "is" "big" "+"))
Dave is red.
True
1
proof
[(triple1)]
("Dave" "is" "red" "+")
triple1
Dave is not red.
False
1
inv-proof
[(triple1)]
("Dave" "is" "red" "-")
triple1
Harry is big.
True
2
proof
[(((triple3) -> rule1) OR ((((triple2) -> rule4)) -> rule1))]
("Harry" "is" "big" "+")
((triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not big.
False
2
inv-proof
[(((triple3) -> rule1) OR ((((triple2) -> rule4)) -> rule1))]
("Harry" "is" "big" "-")
((triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Dave is quiet.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Dave" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not round.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("Dave" "is" "round" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
True
4
proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule1) OR ((((((triple1) -> rule2)) -> rule3) ((((triple1) -> rule2)) -> rule4)) -> rule7))]
("Dave" "is" "big" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((((triple1) -> (rule2 % int4))) -> (rule3 % int3)) ((((triple1) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is not big.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule1) OR ((((((triple1) -> rule2)) -> rule3) ((((triple1) -> rule2)) -> rule4)) -> rule7))]
("Dave" "is" "big" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((((triple1) -> (rule2 % int4))) -> (rule3 % int3)) ((((triple1) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "green" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "green" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Dave is red.[(triple1)] Harry is kind.[(triple2)] Harry is round.[(triple3 OR ((triple2) -> rule4))] @1: Dave is kind.[(((triple1) -> rule2))] Harry is big.[(((triple3) -> rule1) OR ((((triple2) -> rule4)) -> rule1))] @2: Dave is quiet.[(((((triple1) -> rule2)) -> rule3))] Dave is round.[(((((triple1) -> rule2)) -> rule4))] @3: Dave is big.[(((((((triple1) -> rule2)) -> rule4)) -> rule1) OR ((((((triple1) -> rule2)) -> rule3) ((((triple1) -> rule2)) -> rule4)) -> rule7))]
Dave is red.
("Dave" "is" "red" "+")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
((triple2) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((((triple1) -> (rule2 % int4))) -> (rule3 % int3)) ((((triple1) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4