Bob is big. Bob is cold. Bob is furry. Bob is kind. Bob is nice. Bob is quiet. Bob is red. Dave is big. Dave is cold. Dave is furry. Dave is kind. Dave is nice. Dave is quiet. Dave is red. If someone is cold then they are nice. Quiet, big people are nice. Red people are big. If someone is cold and not kind then they are quiet. Nice, big people are quiet. All red people are cold.
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 nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
If someone is cold then they are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
Quiet, big people are nice.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is cold and not kind then they are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "quiet" "+"))
Nice, big people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
All red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Dave is kind.
True
1
proof
[(triple11)]
("Dave" "is" "kind" "+")
triple11
Bob is not nice.
False
1
inv-proof
[(triple5 OR ((triple2) -> rule1) OR ((triple6 triple1) -> rule2) OR ((((triple7) -> rule6)) -> rule1) OR ((triple6 ((triple7) -> rule3)) -> rule2))]
("Bob" "is" "nice" "-")
triple5
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple6 triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((triple6 ((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
@0: Bob is big.[(triple1 OR ((triple7) -> rule3))] Bob is cold.[(triple2 OR ((triple7) -> rule6))] Bob is furry.[(triple3)] Bob is kind.[(triple4)] Bob is nice.[(triple5 OR ((triple2) -> rule1) OR ((triple6 triple1) -> rule2) OR ((((triple7) -> rule6)) -> rule1) OR ((triple6 ((triple7) -> rule3)) -> rule2))] Bob is quiet.[(triple6 OR ((triple5 triple1) -> rule5) OR ((triple5 ((triple7) -> rule3)) -> rule5) OR ((((triple2) -> rule1) triple1) -> rule5) OR ((((triple2) -> rule1) ((triple7) -> rule3)) -> rule5) OR ((((((triple7) -> rule6)) -> rule1) triple1) -> rule5) OR ((((((triple7) -> rule6)) -> rule1) ((triple7) -> rule3)) -> rule5))] Bob is red.[(triple7)] Dave is big.[(triple8 OR ((triple14) -> rule3))] Dave is cold.[(triple9 OR ((triple14) -> rule6))] Dave is furry.[(triple10)] Dave is kind.[(triple11)] Dave is nice.[(triple12 OR ((triple9) -> rule1) OR ((triple13 triple8) -> rule2) OR ((((triple14) -> rule6)) -> rule1) OR ((triple13 ((triple14) -> rule3)) -> rule2))] Dave is quiet.[(triple13 OR ((triple12 triple8) -> rule5) OR ((triple12 ((triple14) -> rule3)) -> rule5) OR ((((triple9) -> rule1) triple8) -> rule5) OR ((((triple9) -> rule1) ((triple14) -> rule3)) -> rule5) OR ((((((triple14) -> rule6)) -> rule1) triple8) -> rule5) OR ((((((triple14) -> rule6)) -> rule1) ((triple14) -> rule3)) -> rule5))] Dave is red.[(triple14)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple7) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple7) -> (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 nice.
("Bob" "is" "nice" "+")
triple5
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple6 triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((triple6 ((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
((triple5 triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple5 ((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple2) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2) -> (rule1 % int3)) ((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((triple7) -> (rule6 % int3))) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((((triple7) -> (rule6 % int4))) -> (rule1 % int3)) ((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
((triple14) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple9
((triple14) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple10
Dave is kind.
("Dave" "is" "kind" "+")
triple11
Dave is nice.
("Dave" "is" "nice" "+")
triple12
((triple9) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple13 triple8) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple14) -> (rule6 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((triple13 ((triple14) -> (rule3 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple13
((triple12 triple8) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple12 ((triple14) -> (rule3 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple9) -> (rule1 % int2)) triple8) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple9) -> (rule1 % int3)) ((triple14) -> (rule3 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((((triple14) -> (rule6 % int3))) -> (rule1 % int2)) triple8) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((((triple14) -> (rule6 % int4))) -> (rule1 % int3)) ((triple14) -> (rule3 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
triple14