Dave is big. Dave is cold. Dave is not furry. Dave is round. Dave is not smart. Dave is not white. Dave is not young. Erin is not big. Erin is cold. Erin is furry. Erin is round. Erin is not smart. Erin is white. Erin is young. If someone is furry and not round then they are not cold. All round, big people are cold. If Dave is big and Dave is cold then Dave is not furry. If Erin is young and Erin is not smart then Erin is cold. All big, cold people are not young. If someone is furry then they are not big.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
Dave is not white.
("Dave" "is" "white" "-")
Dave is not young.
("Dave" "is" "young" "-")
Erin is not big.
("Erin" "is" "big" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If someone is furry and not round then they are not cold.
((("someone" "is" "furry" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "cold" "-"))
All round, big people are cold.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If Dave is big and Dave is cold then Dave is not furry.
((("Dave" "is" "big" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "furry" "-"))
If Erin is young and Erin is not smart then Erin is cold.
((("Erin" "is" "young" "+") ("Erin" "is" "smart" "~")) -> ("Erin" "is" "cold" "+"))
All big, cold people are not young.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "-"))
If someone is furry then they are not big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "-"))
Erin is not big.
True
1
proof
[(triple8 OR ((triple10) -> rule6))]
("Erin" "is" "big" "-")
triple8
((triple10) -> (rule6 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is not white.
False
1
inv-proof
[(triple13)]
("Erin" "is" "white" "-")
triple13
@0: Dave is big.[(triple1)] Dave is cold.[(triple2 OR ((triple4 triple1) -> rule2))] Dave is not furry.[(triple3 OR ((triple1 triple2) -> rule3) OR ((triple1 ((triple4 triple1) -> rule2)) -> rule3))] Dave is not smart.[(triple5)] Dave is not white.[(triple6)] Dave is not young.[(triple7 OR ((triple1 triple2) -> rule5) OR ((triple1 ((triple4 triple1) -> rule2)) -> rule5))] Dave is round.[(triple4)] Erin is cold.[(triple9 OR ((triple14 triple12) -> rule4))] Erin is furry.[(triple10)] Erin is not big.[(triple8 OR ((triple10) -> rule6))] Erin is not smart.[(triple12)] Erin is round.[(triple11)] Erin is white.[(triple13)] Erin is young.[(triple14)]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
((triple4 triple1) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
triple3
((triple1 triple2) -> (rule3 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
((triple1 ((triple4 triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not smart.
("Dave" "is" "smart" "-")
triple5
Dave is not white.
("Dave" "is" "white" "-")
triple6
Dave is not young.
("Dave" "is" "young" "-")
triple7
((triple1 triple2) -> (rule5 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
((triple1 ((triple4 triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple9
((triple14 triple12) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple10
Erin is not big.
("Erin" "is" "big" "-")
triple8
((triple10) -> (rule6 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is not smart.
("Erin" "is" "smart" "-")
triple12
Erin is round.
("Erin" "is" "round" "+")
triple11
Erin is white.
("Erin" "is" "white" "+")
triple13
Erin is young.
("Erin" "is" "young" "+")
triple14