Gary is not big. Gary is not green. Gary is nice. Gary is red. Gary is not round. Gary is not smart. Gary is white. Harry is big. Harry is green. Harry is nice. Harry is red. Harry is round. Harry is smart. Harry is white. If someone is white and big then they are round. If Gary is nice and Gary is green then Gary is not big. All green people are white. If Harry is white and Harry is big then Harry is red. If someone is round and smart then they are big. All green, smart people are big. If Harry is big and Harry is round then Harry is nice. Round people are nice.
Gary is not big.
("Gary" "is" "big" "-")
Gary is not green.
("Gary" "is" "green" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is not round.
("Gary" "is" "round" "-")
Gary is not smart.
("Gary" "is" "smart" "-")
Gary is white.
("Gary" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
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 smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is white and big then they are round.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If Gary is nice and Gary is green then Gary is not big.
((("Gary" "is" "nice" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "big" "-"))
All green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If Harry is white and Harry is big then Harry is red.
((("Harry" "is" "white" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "red" "+"))
If someone is round and smart then they are big.
((("someone" "is" "round" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
All green, smart people are big.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If Harry is big and Harry is round then Harry is nice.
((("Harry" "is" "big" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "nice" "+"))
Round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
Harry is green.
True
1
proof
[(triple9)]
("Harry" "is" "green" "+")
triple9
Gary is not white.
False
1
inv-proof
[(triple7)]
("Gary" "is" "white" "-")
triple7
@0: Gary is nice.[(triple3)] Gary is not big.[(triple1)] Gary is not green.[(triple2)] Gary is not round.[(triple5)] Gary is not smart.[(triple6)] Gary is red.[(triple4)] Gary is white.[(triple7)] Harry is big.[(triple8 OR ((triple12 triple13) -> rule5) OR ((triple9 triple13) -> rule6))] Harry is green.[(triple9)] Harry is nice.[(triple10 OR ((triple12) -> rule8) OR ((triple8 triple12) -> rule7) OR ((((triple14 triple8) -> rule1)) -> rule8) OR ((triple8 ((triple14 triple8) -> rule1)) -> rule7) OR ((((triple12 triple13) -> rule5) triple12) -> rule7) OR ((((triple9 triple13) -> rule6) triple12) -> rule7) OR ((((triple12 triple13) -> rule5) ((triple14 triple8) -> rule1)) -> rule7) OR ((((triple9 triple13) -> rule6) ((triple14 triple8) -> rule1)) -> rule7) OR ((((triple14 ((triple9 triple13) -> rule6)) -> rule1)) -> rule8) OR ((((((triple9) -> rule3) triple8) -> rule1)) -> rule8) OR ((triple8 ((triple14 ((triple9 triple13) -> rule6)) -> rule1)) -> rule7) OR ((triple8 ((((triple9) -> rule3) triple8) -> rule1)) -> rule7) OR ((((((triple9) -> rule3) ((triple9 triple13) -> rule6)) -> rule1)) -> rule8) OR ((triple8 ((((triple9) -> rule3) ((triple9 triple13) -> rule6)) -> rule1)) -> rule7) OR ((((triple12 triple13) -> rule5) ((triple14 ((triple9 triple13) -> rule6)) -> rule1)) -> rule7) OR ((((triple12 triple13) -> rule5) ((((triple9) -> rule3) triple8) -> rule1)) -> rule7) OR ((((triple9 triple13) -> rule6) ((triple14 ((triple9 triple13) -> rule6)) -> rule1)) -> rule7) OR ((((triple9 triple13) -> rule6) ((((triple9) -> rule3) triple8) -> rule1)) -> rule7) OR ((((triple12 triple13) -> rule5) ((((triple9) -> rule3) ((triple9 triple13) -> rule6)) -> rule1)) -> rule7) OR ((((triple9 triple13) -> rule6) ((((triple9) -> rule3) ((triple9 triple13) -> rule6)) -> rule1)) -> rule7))] Harry is red.[(triple11 OR ((triple14 triple8) -> rule4) OR ((triple14 ((triple12 triple13) -> rule5)) -> rule4) OR ((triple14 ((triple9 triple13) -> rule6)) -> rule4) OR ((((triple9) -> rule3) triple8) -> rule4) OR ((((triple9) -> rule3) ((triple12 triple13) -> rule5)) -> rule4) OR ((((triple9) -> rule3) ((triple9 triple13) -> rule6)) -> rule4))] Harry is round.[(triple12 OR ((triple14 triple8) -> rule1) OR ((triple14 ((triple9 triple13) -> rule6)) -> rule1) OR ((((triple9) -> rule3) triple8) -> rule1) OR ((((triple9) -> rule3) ((triple9 triple13) -> rule6)) -> rule1))] Harry is smart.[(triple13)] Harry is white.[(triple14 OR ((triple9) -> rule3))]
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Gary is not big.
("Gary" "is" "big" "-")
triple1
Gary is not green.
("Gary" "is" "green" "-")
triple2
Gary is not round.
("Gary" "is" "round" "-")
triple5
Gary is not smart.
("Gary" "is" "smart" "-")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple4
Gary is white.
("Gary" "is" "white" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple12 triple13) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple9 triple13) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((triple12) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple8 triple12) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple14 triple8) -> (rule1 % int2))) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple8 ((triple14 triple8) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((triple12 triple13) -> (rule5 % int2)) triple12) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple9 triple13) -> (rule6 % int2)) triple12) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple12 triple13) -> (rule5 % int3)) ((triple14 triple8) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((triple9 triple13) -> (rule6 % int3)) ((triple14 triple8) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((triple14 ((triple9 triple13) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((((triple9) -> (rule3 % int3)) triple8) -> (rule1 % int2))) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((triple8 ((triple14 ((triple9 triple13) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((triple8 ((((triple9) -> (rule3 % int3)) triple8) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((triple9) -> (rule3 % int4)) ((triple9 triple13) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
((triple8 ((((triple9) -> (rule3 % int4)) ((triple9 triple13) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
((((triple12 triple13) -> (rule5 % int3)) ((triple14 ((triple9 triple13) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((triple12 triple13) -> (rule5 % int4)) ((((triple9) -> (rule3 % int3)) triple8) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((triple9 triple13) -> (rule6 % int3)) ((triple14 ((triple9 triple13) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((triple9 triple13) -> (rule6 % int4)) ((((triple9) -> (rule3 % int3)) triple8) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((triple12 triple13) -> (rule5 % int4)) ((((triple9) -> (rule3 % int3)) ((triple9 triple13) -> (rule6 % int4))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((triple9 triple13) -> (rule6 % int4)) ((((triple9) -> (rule3 % int3)) ((triple9 triple13) -> (rule6 % int4))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
triple11
((triple14 triple8) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple14 ((triple12 triple13) -> (rule5 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((triple14 ((triple9 triple13) -> (rule6 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple9) -> (rule3 % int2)) triple8) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple9) -> (rule3 % int3)) ((triple12 triple13) -> (rule5 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((triple9) -> (rule3 % int3)) ((triple9 triple13) -> (rule6 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
triple12
((triple14 triple8) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple14 ((triple9 triple13) -> (rule6 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple9) -> (rule3 % int2)) triple8) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple9) -> (rule3 % int3)) ((triple9 triple13) -> (rule6 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple14
((triple9) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1