Charlie is nice. Erin is cold. Erin is nice. Gary is big. Gary is not rough. Gary is smart. Harry is nice. If someone is nice then they are round. Smart, furry people are cold. If someone is furry then they are cold. Big people are smart. If someone is smart then they are furry. If Gary is round and Gary is big then Gary is not nice. If someone is round and nice then they are big. If Gary is rough and Gary is round then Gary is smart. If Charlie is furry and Charlie is rough then Charlie is round.
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Smart, furry people are cold.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry then they are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart then they are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If Gary is round and Gary is big then Gary is not nice.
((("Gary" "is" "round" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "nice" "-"))
If someone is round and nice then they are big.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If Gary is rough and Gary is round then Gary is smart.
((("Gary" "is" "rough" "+") ("Gary" "is" "round" "+")) -> ("Gary" "is" "smart" "+"))
If Charlie is furry and Charlie is rough then Charlie is round.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "round" "+"))
Harry is nice.
True
1
proof
[(triple7)]
("Harry" "is" "nice" "+")
triple7
Erin is not cold.
False
1
inv-proof
[(triple2 OR ((((((((((triple3) -> rule1) triple3) -> rule7)) -> rule4)) -> rule5)) -> rule3) OR ((((((((triple3) -> rule1) triple3) -> rule7)) -> rule4) ((((((((triple3) -> rule1) triple3) -> rule7)) -> rule4)) -> rule5)) -> rule2))]
("Erin" "is" "cold" "-")
triple2
((((((((((triple3) -> (rule1 % int5)) triple3) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
int5
((((((((triple3) -> (rule1 % int5)) triple3) -> (rule7 % int4))) -> (rule4 % int3)) ((((((((triple3) -> (rule1 % int5)) triple3) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
int5
Gary is furry.
True
2
proof
[(((triple6) -> rule5) OR ((((triple4) -> rule4)) -> rule5))]
("Gary" "is" "furry" "+")
((triple6) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not furry.
False
2
inv-proof
[(((triple6) -> rule5) OR ((((triple4) -> rule4)) -> rule5))]
("Gary" "is" "furry" "-")
((triple6) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Erin is big.
True
4
proof
[(((((triple3) -> rule1) triple3) -> rule7))]
("Erin" "is" "big" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not big.
False
4
inv-proof
[(((((triple3) -> rule1) triple3) -> rule7))]
("Erin" "is" "big" "-")
((((triple3) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is smart.
True
5
proof
[(((((((triple3) -> rule1) triple3) -> rule7)) -> rule4))]
("Erin" "is" "smart" "+")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Charlie is not smart.
False
5
inv-proof
[(((((((triple1) -> rule1) triple1) -> rule7)) -> rule4))]
("Charlie" "is" "smart" "-")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Erin is furry.
True
6
proof
[(((((((((triple3) -> rule1) triple3) -> rule7)) -> rule4)) -> rule5))]
("Erin" "is" "furry" "+")
((((((((triple3) -> (rule1 % int4)) triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Charlie is not furry.
False
6
inv-proof
[(((((((((triple1) -> rule1) triple1) -> rule7)) -> rule4)) -> rule5))]
("Charlie" "is" "furry" "-")
((((((((triple1) -> (rule1 % int4)) triple1) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is cold.
True
7
proof
[(((((((((((triple1) -> rule1) triple1) -> rule7)) -> rule4)) -> rule5)) -> rule3) OR ((((((((triple1) -> rule1) triple1) -> rule7)) -> rule4) ((((((((triple1) -> rule1) triple1) -> rule7)) -> rule4)) -> rule5)) -> rule2))]
("Charlie" "is" "cold" "+")
((((((((((triple1) -> (rule1 % int5)) triple1) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5
((((((((triple1) -> (rule1 % int5)) triple1) -> (rule7 % int4))) -> (rule4 % int3)) ((((((((triple1) -> (rule1 % int5)) triple1) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5
Charlie is not cold.
False
7
inv-proof
[(((((((((((triple1) -> rule1) triple1) -> rule7)) -> rule4)) -> rule5)) -> rule3) OR ((((((((triple1) -> rule1) triple1) -> rule7)) -> rule4) ((((((((triple1) -> rule1) triple1) -> rule7)) -> rule4)) -> rule5)) -> rule2))]
("Charlie" "is" "cold" "-")
((((((((((triple1) -> (rule1 % int5)) triple1) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5
((((((((triple1) -> (rule1 % int5)) triple1) -> (rule7 % int4))) -> (rule4 % int3)) ((((((((triple1) -> (rule1 % int5)) triple1) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is nice.[(triple1)] Erin is cold.[(triple2 OR ((((((((((triple3) -> rule1) triple3) -> rule7)) -> rule4)) -> rule5)) -> rule3) OR ((((((((triple3) -> rule1) triple3) -> rule7)) -> rule4) ((((((((triple3) -> rule1) triple3) -> rule7)) -> rule4)) -> rule5)) -> rule2))] Erin is nice.[(triple3)] Gary is big.[(triple4)] Gary is not rough.[(triple5)] Gary is smart.[(triple6 OR ((triple4) -> rule4))] Harry is nice.[(triple7)] @1: Charlie is round.[(((triple1) -> rule1))] Erin is round.[(((triple3) -> rule1))] Gary is furry.[(((triple6) -> rule5) OR ((((triple4) -> rule4)) -> rule5))] Harry is round.[(((triple7) -> rule1))] @2: Charlie is big.[(((((triple1) -> rule1) triple1) -> rule7))] Erin is big.[(((((triple3) -> rule1) triple3) -> rule7))] Gary is cold.[(((((triple6) -> rule5)) -> rule3) OR ((triple6 ((triple6) -> rule5)) -> rule2) OR ((((triple4) -> rule4) ((triple6) -> rule5)) -> rule2) OR ((((((triple4) -> rule4)) -> rule5)) -> rule3) OR ((triple6 ((((triple4) -> rule4)) -> rule5)) -> rule2) OR ((((triple4) -> rule4) ((((triple4) -> rule4)) -> rule5)) -> rule2))] Harry is big.[(((((triple7) -> rule1) triple7) -> rule7))] @3: Charlie is smart.[(((((((triple1) -> rule1) triple1) -> rule7)) -> rule4))] Erin is smart.[(((((((triple3) -> rule1) triple3) -> rule7)) -> rule4))] Harry is smart.[(((((((triple7) -> rule1) triple7) -> rule7)) -> rule4))] @4: Charlie is furry.[(((((((((triple1) -> rule1) triple1) -> rule7)) -> rule4)) -> rule5))] Erin is furry.[(((((((((triple3) -> rule1) triple3) -> rule7)) -> rule4)) -> rule5))] Harry is furry.[(((((((((triple7) -> rule1) triple7) -> rule7)) -> rule4)) -> rule5))] @5: Charlie is cold.[(((((((((((triple1) -> rule1) triple1) -> rule7)) -> rule4)) -> rule5)) -> rule3) OR ((((((((triple1) -> rule1) triple1) -> rule7)) -> rule4) ((((((((triple1) -> rule1) triple1) -> rule7)) -> rule4)) -> rule5)) -> rule2))] Harry is cold.[(((((((((((triple7) -> rule1) triple7) -> rule7)) -> rule4)) -> rule5)) -> rule3) OR ((((((((triple7) -> rule1) triple7) -> rule7)) -> rule4) ((((((((triple7) -> rule1) triple7) -> rule7)) -> rule4)) -> rule5)) -> rule2))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((((((((((triple3) -> (rule1 % int5)) triple3) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
int5
((((((((triple3) -> (rule1 % int5)) triple3) -> (rule7 % int4))) -> (rule4 % int3)) ((((((((triple3) -> (rule1 % int5)) triple3) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
int5
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Gary is not rough.
("Gary" "is" "rough" "-")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
((triple4) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple3) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple6) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((triple6 ((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple4) -> (rule4 % int3)) ((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((triple6 ((((triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple4) -> (rule4 % int3)) ((((triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((((triple7) -> (rule1 % int2)) triple7) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple7) -> (rule1 % int3)) triple7) -> (rule7 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((((triple1) -> (rule1 % int4)) triple1) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Erin is furry.
("Erin" "is" "furry" "+")
((((((((triple3) -> (rule1 % int4)) triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
((((((((triple7) -> (rule1 % int4)) triple7) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((((((triple1) -> (rule1 % int5)) triple1) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5
((((((((triple1) -> (rule1 % int5)) triple1) -> (rule7 % int4))) -> (rule4 % int3)) ((((((((triple1) -> (rule1 % int5)) triple1) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5
Harry is cold.
("Harry" "is" "cold" "+")
((((((((((triple7) -> (rule1 % int5)) triple7) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
int5
((((((((triple7) -> (rule1 % int5)) triple7) -> (rule7 % int4))) -> (rule4 % int3)) ((((((((triple7) -> (rule1 % int5)) triple7) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
int5