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