Anne is kind. Anne is not quiet. Dave is kind. Dave is round. Erin is kind. Harry is kind. Harry is round. If someone is green and kind then they are furry. Big, kind people are not quiet. Kind people are green. If someone is quiet then they are white. Round, furry people are white. If someone is round and quiet then they are big.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is green and kind then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Big, kind people are not quiet.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "-"))
Kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Round, furry people are white.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If someone is round and quiet then they are big.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Harry is kind.
True
1
proof
[(triple6)]
("Harry" "is" "kind" "+")
triple6
Anne is quiet.
False
1
inv-proof
[(triple2)]
("Anne" "is" "quiet" "+")
triple2
Anne is green.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "green" "+")
((triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple3) -> rule3))]
("Dave" "is" "green" "-")
((triple3) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
True
4
proof
[(((((triple3) -> rule3) triple3) -> rule1))]
("Dave" "is" "furry" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Anne is not furry.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule1))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Harry is white.
True
6
proof
[(((triple7 ((((triple6) -> rule3) triple6) -> rule1)) -> rule5))]
("Harry" "is" "white" "+")
((triple7 ((((triple6) -> (rule3 % int3)) triple6) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not white.
False
6
inv-proof
[(((triple7 ((((triple6) -> rule3) triple6) -> rule1)) -> rule5))]
("Harry" "is" "white" "-")
((triple7 ((((triple6) -> (rule3 % int3)) triple6) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "big" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "big" "+")
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "white" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "big" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Anne is kind.[(triple1)] Anne is not quiet.[(triple2)] Dave is kind.[(triple3)] Dave is round.[(triple4)] Erin is kind.[(triple5)] Harry is kind.[(triple6)] Harry is round.[(triple7)] @1: Anne is green.[(((triple1) -> rule3))] Dave is green.[(((triple3) -> rule3))] Erin is green.[(((triple5) -> rule3))] Harry is green.[(((triple6) -> rule3))] @2: Anne is furry.[(((((triple1) -> rule3) triple1) -> rule1))] Dave is furry.[(((((triple3) -> rule3) triple3) -> rule1))] Erin is furry.[(((((triple5) -> rule3) triple5) -> rule1))] Harry is furry.[(((((triple6) -> rule3) triple6) -> rule1))] @3: Dave is white.[(((triple4 ((((triple3) -> rule3) triple3) -> rule1)) -> rule5))] Harry is white.[(((triple7 ((((triple6) -> rule3) triple6) -> rule1)) -> rule5))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple3) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple5) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple6) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((triple5) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((triple6) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((triple4 ((((triple3) -> (rule3 % int3)) triple3) -> (rule1 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((triple7 ((((triple6) -> (rule3 % int3)) triple6) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3