Dave is cold. Dave is green. Dave is nice. Dave is quiet. Dave is red. Dave is white. Gary is big. Gary is cold. Gary is green. Gary is white. If Gary is big and Gary is cold then Gary is white. White, quiet people are red. White, cold people are big. Nice people are cold. All red, nice people are cold. If Gary is white then Gary is red. Cold, green people are nice. If someone is big then they are white.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is white.
("Gary" "is" "white" "+")
If Gary is big and Gary is cold then Gary is white.
((("Gary" "is" "big" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "white" "+"))
White, quiet people are red.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
White, cold people are big.
((("someone" "is" "white" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
Nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
All red, nice people are cold.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If Gary is white then Gary is red.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "red" "+"))
Cold, green people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Dave is red.
True
1
proof
[(triple5 OR ((triple6 triple4) -> rule2))]
("Dave" "is" "red" "+")
triple5
((triple6 triple4) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not quiet.
False
1
inv-proof
[(triple4)]
("Dave" "is" "quiet" "-")
triple4
Gary is red.
True
2
proof
[(((triple10) -> rule6) OR ((((triple7) -> rule8)) -> rule6) OR ((((triple7 triple8) -> rule1)) -> rule6))]
("Gary" "is" "red" "+")
((triple10) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple7) -> (rule8 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple7 triple8) -> (rule1 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Dave is not big.
False
3
inv-proof
[(((triple6 triple1) -> rule3) OR ((triple6 ((triple3) -> rule4)) -> rule3) OR ((triple6 ((triple5 triple3) -> rule5)) -> rule3) OR ((triple6 ((((triple6 triple4) -> rule2) triple3) -> rule5)) -> rule3))]
("Dave" "is" "big" "-")
((triple6 triple1) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple6 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((triple6 ((triple5 triple3) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((triple6 ((((triple6 triple4) -> (rule2 % int3)) triple3) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
@0: Dave is cold.[(triple1 OR ((triple3) -> rule4) OR ((triple5 triple3) -> rule5) OR ((((triple6 triple4) -> rule2) triple3) -> rule5))] Dave is green.[(triple2)] Dave is nice.[(triple3 OR ((triple1 triple2) -> rule7))] Dave is quiet.[(triple4)] Dave is red.[(triple5 OR ((triple6 triple4) -> rule2))] Dave is white.[(triple6)] Gary is big.[(triple7 OR ((triple10 triple8) -> rule3))] Gary is cold.[(triple8)] Gary is green.[(triple9)] Gary is white.[(triple10 OR ((triple7) -> rule8) OR ((triple7 triple8) -> rule1))] @1: Dave is big.[(((triple6 triple1) -> rule3) OR ((triple6 ((triple3) -> rule4)) -> rule3) OR ((triple6 ((triple5 triple3) -> rule5)) -> rule3) OR ((triple6 ((((triple6 triple4) -> rule2) triple3) -> rule5)) -> rule3))] Gary is nice.[(((triple8 triple9) -> rule7))] Gary is red.[(((triple10) -> rule6) OR ((((triple7) -> rule8)) -> rule6) OR ((((triple7 triple8) -> rule1)) -> rule6))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
((triple3) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple5 triple3) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple6 triple4) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple1 triple2) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple6 triple4) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
((triple10 triple8) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
((triple7) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple7 triple8) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple6 triple1) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple6 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((triple6 ((triple5 triple3) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((triple6 ((((triple6 triple4) -> (rule2 % int3)) triple3) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
((triple8 triple9) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple10) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple7) -> (rule8 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple7 triple8) -> (rule1 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2