Dave is furry. Dave is kind. Dave is quiet. Erin is green. Erin is kind. Erin is round. Erin is smart. Gary is green. Gary is kind. Gary is nice. Gary is smart. Harry is furry. Harry is green. Harry is nice. Harry is quiet. Harry is smart. Green, kind things are quiet. Quiet, nice things are furry. If Erin is smart and Erin is quiet then Erin is kind. All kind, nice things are green. If something is nice then it is round. Kind, smart things are quiet. If Erin is kind and Erin is furry then Erin is nice. All quiet things are furry.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Green, kind things are quiet.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
Quiet, nice things are furry.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If Erin is smart and Erin is quiet then Erin is kind.
((("Erin" "is" "smart" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "kind" "+"))
All kind, nice things are green.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is nice then it is round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Kind, smart things are quiet.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If Erin is kind and Erin is furry then Erin is nice.
((("Erin" "is" "kind" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "nice" "+"))
All quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Erin is green.
True
1
proof
[(triple4 OR ((triple5 ((triple5 ((((triple5 triple7) -> rule6)) -> rule8)) -> rule7)) -> rule4))]
("Erin" "is" "green" "+")
triple4
((triple5 ((triple5 ((((triple5 triple7) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is not kind.
False
1
inv-proof
[(triple5)]
("Erin" "is" "kind" "-")
triple5
Harry is round.
True
2
proof
[(((triple14) -> rule5))]
("Harry" "is" "round" "+")
((triple14) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Erin is not quiet.
False
3
inv-proof
[(((triple4 triple5) -> rule1) OR ((triple5 triple7) -> rule6))]
("Erin" "is" "quiet" "-")
((triple4 triple5) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple5 triple7) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
True
4
proof
[(((((triple4 triple5) -> rule1)) -> rule8) OR ((((triple5 triple7) -> rule6)) -> rule8))]
("Erin" "is" "furry" "+")
((((triple4 triple5) -> (rule1 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple5 triple7) -> (rule6 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not furry.
False
4
inv-proof
[(((((triple4 triple5) -> rule1)) -> rule8) OR ((((triple5 triple7) -> rule6)) -> rule8))]
("Erin" "is" "furry" "-")
((((triple4 triple5) -> (rule1 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple5 triple7) -> (rule6 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is nice.
True
6
proof
[(((triple5 ((((triple4 triple5) -> rule1)) -> rule8)) -> rule7) OR ((triple5 ((((triple5 triple7) -> rule6)) -> rule8)) -> rule7))]
("Erin" "is" "nice" "+")
((triple5 ((((triple4 triple5) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((triple5 ((((triple5 triple7) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is not nice.
False
6
inv-proof
[(((triple5 ((((triple4 triple5) -> rule1)) -> rule8)) -> rule7) OR ((triple5 ((((triple5 triple7) -> rule6)) -> rule8)) -> rule7))]
("Erin" "is" "nice" "-")
((triple5 ((((triple4 triple5) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((triple5 ((((triple5 triple7) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "round" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is furry.[(triple1 OR ((triple3) -> rule8))] Dave is kind.[(triple2)] Dave is quiet.[(triple3)] Erin is green.[(triple4 OR ((triple5 ((triple5 ((((triple5 triple7) -> rule6)) -> rule8)) -> rule7)) -> rule4))] Erin is kind.[(triple5)] Erin is round.[(triple6 OR ((((triple5 ((((triple4 triple5) -> rule1)) -> rule8)) -> rule7)) -> rule5) OR ((((triple5 ((((triple5 triple7) -> rule6)) -> rule8)) -> rule7)) -> rule5))] Erin is smart.[(triple7)] Gary is green.[(triple8 OR ((triple9 triple10) -> rule4))] Gary is kind.[(triple9)] Gary is nice.[(triple10)] Gary is smart.[(triple11)] Harry is furry.[(triple12 OR ((triple15) -> rule8) OR ((triple15 triple14) -> rule2))] Harry is green.[(triple13)] Harry is nice.[(triple14)] Harry is quiet.[(triple15)] Harry is smart.[(triple16)] @1: Erin is quiet.[(((triple4 triple5) -> rule1) OR ((triple5 triple7) -> rule6))] Gary is quiet.[(((triple8 triple9) -> rule1) OR ((triple9 triple11) -> rule6) OR ((((triple9 triple10) -> rule4) triple9) -> rule1))] Gary is round.[(((triple10) -> rule5))] Harry is round.[(((triple14) -> rule5))] @2: Erin is furry.[(((((triple4 triple5) -> rule1)) -> rule8) OR ((((triple5 triple7) -> rule6)) -> rule8))] Gary is furry.[(((((triple8 triple9) -> rule1)) -> rule8) OR ((((triple9 triple11) -> rule6)) -> rule8) OR ((((triple8 triple9) -> rule1) triple10) -> rule2) OR ((((triple9 triple11) -> rule6) triple10) -> rule2) OR ((((((triple9 triple10) -> rule4) triple9) -> rule1)) -> rule8) OR ((((((triple9 triple10) -> rule4) triple9) -> rule1) triple10) -> rule2))] @3: Erin is nice.[(((triple5 ((((triple4 triple5) -> rule1)) -> rule8)) -> rule7) OR ((triple5 ((((triple5 triple7) -> rule6)) -> rule8)) -> rule7))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
((triple3) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
((triple5 ((triple5 ((((triple5 triple7) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
((((triple5 ((((triple4 triple5) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((triple5 ((((triple5 triple7) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple8
((triple9 triple10) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
triple11
Harry is furry.
("Harry" "is" "furry" "+")
triple12
((triple15) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple15 triple14) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple13
Harry is nice.
("Harry" "is" "nice" "+")
triple14
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
triple16
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple4 triple5) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple5 triple7) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple8 triple9) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple9 triple11) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple9 triple10) -> (rule4 % int2)) triple9) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple10) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple14) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple4 triple5) -> (rule1 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple5 triple7) -> (rule6 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((triple8 triple9) -> (rule1 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple9 triple11) -> (rule6 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple8 triple9) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple9 triple11) -> (rule6 % int2)) triple10) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((((triple9 triple10) -> (rule4 % int3)) triple9) -> (rule1 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((triple9 triple10) -> (rule4 % int3)) triple9) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((triple5 ((((triple4 triple5) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((triple5 ((((triple5 triple7) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3