Dave is big. Dave is furry. Dave is green. Dave is nice. Dave is red. Dave is round. Dave is white. Harry is big. Harry is furry. Harry is green. Harry is nice. Harry is red. Harry is round. Harry is white. All round people are furry. All white, round people are red. Red people are green.
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 round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
All round people are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
All white, round people are red.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Harry is big.
True
1
proof
[(triple8)]
("Harry" "is" "big" "+")
triple8
Dave is not white.
False
1
inv-proof
[(triple7)]
("Dave" "is" "white" "-")
triple7
@0: Dave is big.[(triple1)] Dave is furry.[(triple2 OR ((triple6) -> rule1))] Dave is green.[(triple3 OR ((triple5) -> rule3) OR ((((triple7 triple6) -> rule2)) -> rule3))] Dave is nice.[(triple4)] Dave is red.[(triple5 OR ((triple7 triple6) -> rule2))] Dave is round.[(triple6)] Dave is white.[(triple7)] Harry is big.[(triple8)] Harry is furry.[(triple9 OR ((triple13) -> rule1))] Harry is green.[(triple10 OR ((triple12) -> rule3) OR ((((triple14 triple13) -> rule2)) -> rule3))] Harry is nice.[(triple11)] Harry is red.[(triple12 OR ((triple14 triple13) -> rule2))] Harry is round.[(triple13)] Harry is white.[(triple14)]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple6) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple3
((triple5) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple7 triple6) -> (rule2 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple7 triple6) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
((triple13) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple10
((triple12) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple14 triple13) -> (rule2 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
((triple14 triple13) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple14