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