Dave is big. Dave is green. Dave is kind. Dave is nice. Dave is rough. Dave is smart. Dave is white. Harry is kind. Harry is nice. Harry is rough. Harry is smart. Harry is white. If someone is big then they are smart. White, kind people are green. If someone is green then they are white. Big, nice people are green. If Harry is white and Harry is green then Harry is big. If someone is nice then they are green.
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is big then they are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
White, kind people are green.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Big, nice people are green.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Harry is white and Harry is green then Harry is big.
((("Harry" "is" "white" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "big" "+"))
If someone is nice then they are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Dave is green.
True
1
proof
[(triple2 OR ((triple4) -> rule6) OR ((triple1 triple4) -> rule4) OR ((triple7 triple3) -> rule2))]
("Dave" "is" "green" "+")
triple2
((triple4) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple1 triple4) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple7 triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not white.
False
1
inv-proof
[(triple7 OR ((triple2) -> rule3) OR ((((triple4) -> rule6)) -> rule3) OR ((((triple1 triple4) -> rule4)) -> rule3))]
("Dave" "is" "white" "-")
triple7
((triple2) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple1 triple4) -> (rule4 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Harry is green.
True
2
proof
[(((triple9) -> rule6) OR ((triple12 triple8) -> rule2))]
("Harry" "is" "green" "+")
((triple9) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple12 triple8) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple9) -> rule6) OR ((triple12 triple8) -> rule2))]
("Harry" "is" "green" "-")
((triple9) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple12 triple8) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
True
4
proof
[(((triple12 ((triple9) -> rule6)) -> rule5) OR ((triple12 ((triple12 triple8) -> rule2)) -> rule5) OR ((((((triple9) -> rule6)) -> rule3) ((triple9) -> rule6)) -> rule5) OR ((((((triple9) -> rule6)) -> rule3) ((triple12 triple8) -> rule2)) -> rule5))]
("Harry" "is" "big" "+")
((triple12 ((triple9) -> (rule6 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((triple12 ((triple12 triple8) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple9) -> (rule6 % int3))) -> (rule3 % int2)) ((triple9) -> (rule6 % int3))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple9) -> (rule6 % int3))) -> (rule3 % int2)) ((triple12 triple8) -> (rule2 % int3))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not big.
False
4
inv-proof
[(((triple12 ((triple9) -> rule6)) -> rule5) OR ((triple12 ((triple12 triple8) -> rule2)) -> rule5) OR ((((((triple9) -> rule6)) -> rule3) ((triple9) -> rule6)) -> rule5) OR ((((((triple9) -> rule6)) -> rule3) ((triple12 triple8) -> rule2)) -> rule5))]
("Harry" "is" "big" "-")
((triple12 ((triple9) -> (rule6 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((triple12 ((triple12 triple8) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple9) -> (rule6 % int3))) -> (rule3 % int2)) ((triple9) -> (rule6 % int3))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple9) -> (rule6 % int3))) -> (rule3 % int2)) ((triple12 triple8) -> (rule2 % int3))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
@0: Dave is big.[(triple1)] Dave is green.[(triple2 OR ((triple4) -> rule6) OR ((triple1 triple4) -> rule4) OR ((triple7 triple3) -> rule2))] Dave is kind.[(triple3)] Dave is nice.[(triple4)] Dave is rough.[(triple5)] Dave is smart.[(triple6 OR ((triple1) -> rule1))] Dave is white.[(triple7 OR ((triple2) -> rule3) OR ((((triple4) -> rule6)) -> rule3) OR ((((triple1 triple4) -> rule4)) -> rule3))] Harry is kind.[(triple8)] Harry is nice.[(triple9)] Harry is rough.[(triple10)] Harry is smart.[(triple11 OR ((((triple12 ((triple9) -> rule6)) -> rule5)) -> rule1) OR ((((triple12 ((triple12 triple8) -> rule2)) -> rule5)) -> rule1) OR ((((((((triple9) -> rule6)) -> rule3) ((triple9) -> rule6)) -> rule5)) -> rule1) OR ((((((((triple9) -> rule6)) -> rule3) ((triple12 triple8) -> rule2)) -> rule5)) -> rule1))] Harry is white.[(triple12 OR ((((triple9) -> rule6)) -> rule3))] @1: Harry is green.[(((triple9) -> rule6) OR ((triple12 triple8) -> rule2))] @2: Harry is big.[(((triple12 ((triple9) -> rule6)) -> rule5) OR ((triple12 ((triple12 triple8) -> rule2)) -> rule5) OR ((((((triple9) -> rule6)) -> rule3) ((triple9) -> rule6)) -> rule5) OR ((((((triple9) -> rule6)) -> rule3) ((triple12 triple8) -> rule2)) -> rule5))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
((triple4) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple1 triple4) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple7 triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
((triple1) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple7
((triple2) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple1 triple4) -> (rule4 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
((((triple12 ((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((triple12 ((triple12 triple8) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((((triple9) -> (rule6 % int4))) -> (rule3 % int3)) ((triple9) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
((((((((triple9) -> (rule6 % int4))) -> (rule3 % int3)) ((triple12 triple8) -> (rule2 % int4))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
triple12
((((triple9) -> (rule6 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((triple9) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple12 triple8) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple12 ((triple9) -> (rule6 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((triple12 ((triple12 triple8) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple9) -> (rule6 % int3))) -> (rule3 % int2)) ((triple9) -> (rule6 % int3))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple9) -> (rule6 % int3))) -> (rule3 % int2)) ((triple12 triple8) -> (rule2 % int3))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3