Dave is big. Dave is furry. Dave is green. Dave is nice. Dave is red. Dave is smart. Erin is big. Erin is blue. Erin is not furry. Erin is green. Erin is red. Erin is smart. Blue people are not nice. If someone is red and green then they are smart. Red, nice people are furry. If Erin is red and Erin is not smart then Erin is not furry. If someone is furry then they are big. If someone is furry and red then they are big. If someone is blue and not smart then they are big. If Erin is furry then Erin is not nice.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Blue people are not nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "-"))
If someone is red and green then they are smart.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Red, nice people are furry.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If Erin is red and Erin is not smart then Erin is not furry.
((("Erin" "is" "red" "+") ("Erin" "is" "smart" "~")) -> ("Erin" "is" "furry" "-"))
If someone is furry then they are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If someone is furry and red then they are big.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is blue and not smart then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "big" "+"))
If Erin is furry then Erin is not nice.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "nice" "-"))
Erin is blue.
True
1
proof
[(triple8)]
("Erin" "is" "blue" "+")
triple8
Dave is not nice.
False
1
inv-proof
[(triple4)]
("Dave" "is" "nice" "-")
triple4
@0: Dave is big.[(triple1 OR ((triple2) -> rule5) OR ((triple2 triple5) -> rule6) OR ((((triple5 triple4) -> rule3)) -> rule5) OR ((((triple5 triple4) -> rule3) triple5) -> rule6))] Dave is furry.[(triple2 OR ((triple5 triple4) -> rule3))] Dave is green.[(triple3)] Dave is nice.[(triple4)] Dave is red.[(triple5)] Dave is smart.[(triple6 OR ((triple5 triple3) -> rule2))] Erin is big.[(triple7)] Erin is blue.[(triple8)] Erin is green.[(triple10)] Erin is not furry.[(triple9)] Erin is red.[(triple11)] Erin is smart.[(triple12 OR ((triple11 triple10) -> rule2))] @1: Erin is not nice.[(((triple8) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple2) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple2 triple5) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple5 triple4) -> (rule3 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((triple5 triple4) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple5 triple4) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
((triple5 triple3) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is not furry.
("Erin" "is" "furry" "-")
triple9
Erin is red.
("Erin" "is" "red" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
((triple11 triple10) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
((triple8) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1