Charlie is not big. Charlie is blue. Charlie is cold. Charlie is furry. Charlie is green. Charlie is nice. Charlie is rough. Dave is big. Dave is blue. Dave is cold. Dave is furry. Dave is green. Dave is nice. Dave is rough. All nice people are furry. If Dave is not furry then Dave is blue. Rough people are cold. If someone is big and not green then they are cold. If someone is cold and green then they are rough. If Dave is blue and Dave is furry then Dave is cold.
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
All nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If Dave is not furry then Dave is blue.
((("Dave" "is" "furry" "~")) -> ("Dave" "is" "blue" "+"))
Rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is big and not green then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "cold" "+"))
If someone is cold and green then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If Dave is blue and Dave is furry then Dave is cold.
((("Dave" "is" "blue" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "cold" "+"))
Charlie is furry.
True
1
proof
[(triple4 OR ((triple6) -> rule1))]
("Charlie" "is" "furry" "+")
triple4
((triple6) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
@0: Charlie is blue.[(triple2)] Charlie is cold.[(triple3 OR ((triple7) -> rule3))] Charlie is furry.[(triple4 OR ((triple6) -> rule1))] Charlie is green.[(triple5)] Charlie is nice.[(triple6)] Charlie is not big.[(triple1)] Charlie is rough.[(triple7 OR ((triple3 triple5) -> rule5))] Dave is big.[(triple8)] Dave is blue.[(triple9)] Dave is cold.[(triple10 OR ((triple14) -> rule3) OR ((triple9 triple11) -> rule6) OR ((triple9 ((triple13) -> rule1)) -> rule6))] Dave is furry.[(triple11 OR ((triple13) -> rule1))] Dave is green.[(triple12)] Dave is nice.[(triple13)] Dave is rough.[(triple14 OR ((triple10 triple12) -> rule5) OR ((((triple9 triple11) -> rule6) triple12) -> rule5) OR ((((triple9 ((triple13) -> rule1)) -> rule6) triple12) -> rule5))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
((triple7) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
((triple6) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is not big.
("Charlie" "is" "big" "-")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
((triple3 triple5) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is blue.
("Dave" "is" "blue" "+")
triple9
Dave is cold.
("Dave" "is" "cold" "+")
triple10
((triple14) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple9 triple11) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple9 ((triple13) -> (rule1 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple11
((triple13) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple12
Dave is nice.
("Dave" "is" "nice" "+")
triple13
Dave is rough.
("Dave" "is" "rough" "+")
triple14
((triple10 triple12) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple9 triple11) -> (rule6 % int2)) triple12) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((triple9 ((triple13) -> (rule1 % int3))) -> (rule6 % int2)) triple12) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3