Anne is not big. Anne is cold. Anne is kind. Anne is red. Anne is rough. Anne is round. Anne is white. Dave is big. Dave is cold. Dave is red. Dave is rough. Dave is white. If Anne is not white then Anne is not red. All cold, red people are kind. All white people are kind. Cold people are kind. If someone is red and kind then they are round. All rough, red people are cold.
Anne is not big.
("Anne" "is" "big" "-")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
If Anne is not white then Anne is not red.
((("Anne" "is" "white" "~")) -> ("Anne" "is" "red" "-"))
All cold, red people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All white people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
Cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is red and kind then they are round.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
All rough, red people are cold.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Dave is big.
True
1
proof
[(triple8)]
("Dave" "is" "big" "+")
triple8
Dave is not rough.
False
1
inv-proof
[(triple11)]
("Dave" "is" "rough" "-")
triple11
Dave is kind.
True
2
proof
[(((triple12) -> rule3) OR ((triple9) -> rule4) OR ((triple9 triple10) -> rule2) OR ((((triple11 triple10) -> rule6)) -> rule4) OR ((((triple11 triple10) -> rule6) triple10) -> rule2))]
("Dave" "is" "kind" "+")
((triple12) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple9) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple9 triple10) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple11 triple10) -> (rule6 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((triple11 triple10) -> (rule6 % int2)) triple10) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not kind.
False
2
inv-proof
[(((triple12) -> rule3) OR ((triple9) -> rule4) OR ((triple9 triple10) -> rule2) OR ((((triple11 triple10) -> rule6)) -> rule4) OR ((((triple11 triple10) -> rule6) triple10) -> rule2))]
("Dave" "is" "kind" "-")
((triple12) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple9) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple9 triple10) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple11 triple10) -> (rule6 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((triple11 triple10) -> (rule6 % int2)) triple10) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
True
4
proof
[(((triple10 ((triple12) -> rule3)) -> rule5) OR ((triple10 ((triple9) -> rule4)) -> rule5) OR ((triple10 ((triple9 triple10) -> rule2)) -> rule5) OR ((triple10 ((((triple11 triple10) -> rule6)) -> rule4)) -> rule5) OR ((triple10 ((((triple11 triple10) -> rule6) triple10) -> rule2)) -> rule5))]
("Dave" "is" "round" "+")
((triple10 ((triple12) -> (rule3 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple10 ((triple9) -> (rule4 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple10 ((triple9 triple10) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple10 ((((triple11 triple10) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((triple10 ((((triple11 triple10) -> (rule6 % int3)) triple10) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is not round.
False
4
inv-proof
[(((triple10 ((triple12) -> rule3)) -> rule5) OR ((triple10 ((triple9) -> rule4)) -> rule5) OR ((triple10 ((triple9 triple10) -> rule2)) -> rule5) OR ((triple10 ((((triple11 triple10) -> rule6)) -> rule4)) -> rule5) OR ((triple10 ((((triple11 triple10) -> rule6) triple10) -> rule2)) -> rule5))]
("Dave" "is" "round" "-")
((triple10 ((triple12) -> (rule3 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple10 ((triple9) -> (rule4 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple10 ((triple9 triple10) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple10 ((((triple11 triple10) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((triple10 ((((triple11 triple10) -> (rule6 % int3)) triple10) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
@0: Anne is cold.[(triple2 OR ((triple5 triple4) -> rule6))] Anne is kind.[(triple3 OR ((triple2) -> rule4) OR ((triple7) -> rule3) OR ((triple2 triple4) -> rule2) OR ((((triple5 triple4) -> rule6)) -> rule4) OR ((((triple5 triple4) -> rule6) triple4) -> rule2))] Anne is not big.[(triple1)] Anne is red.[(triple4)] Anne is rough.[(triple5)] Anne is round.[(triple6 OR ((triple4 triple3) -> rule5) OR ((triple4 ((triple2) -> rule4)) -> rule5) OR ((triple4 ((triple7) -> rule3)) -> rule5) OR ((triple4 ((triple2 triple4) -> rule2)) -> rule5) OR ((triple4 ((((triple5 triple4) -> rule6)) -> rule4)) -> rule5) OR ((triple4 ((((triple5 triple4) -> rule6) triple4) -> rule2)) -> rule5))] Anne is white.[(triple7)] Dave is big.[(triple8)] Dave is cold.[(triple9 OR ((triple11 triple10) -> rule6))] Dave is red.[(triple10)] Dave is rough.[(triple11)] Dave is white.[(triple12)] @1: Dave is kind.[(((triple12) -> rule3) OR ((triple9) -> rule4) OR ((triple9 triple10) -> rule2) OR ((((triple11 triple10) -> rule6)) -> rule4) OR ((((triple11 triple10) -> rule6) triple10) -> rule2))] @2: Dave is round.[(((triple10 ((triple12) -> rule3)) -> rule5) OR ((triple10 ((triple9) -> rule4)) -> rule5) OR ((triple10 ((triple9 triple10) -> rule2)) -> rule5) OR ((triple10 ((((triple11 triple10) -> rule6)) -> rule4)) -> rule5) OR ((triple10 ((((triple11 triple10) -> rule6) triple10) -> rule2)) -> rule5))]
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple5 triple4) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple2) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple7) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple2 triple4) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple5 triple4) -> (rule6 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple5 triple4) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not big.
("Anne" "is" "big" "-")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple4 triple3) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple4 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((triple4 ((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((triple4 ((triple2 triple4) -> (rule2 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((triple4 ((((triple5 triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((triple4 ((((triple5 triple4) -> (rule6 % int3)) triple4) -> (rule2 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is cold.
("Dave" "is" "cold" "+")
triple9
((triple11 triple10) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple10
Dave is rough.
("Dave" "is" "rough" "+")
triple11
Dave is white.
("Dave" "is" "white" "+")
triple12
Dave is kind.
("Dave" "is" "kind" "+")
((triple12) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple9) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple9 triple10) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple11 triple10) -> (rule6 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((triple11 triple10) -> (rule6 % int2)) triple10) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((triple10 ((triple12) -> (rule3 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple10 ((triple9) -> (rule4 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple10 ((triple9 triple10) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple10 ((((triple11 triple10) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((triple10 ((((triple11 triple10) -> (rule6 % int3)) triple10) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3