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