Dave is blue. Dave is kind. Dave is nice. Dave is red. Erin is big. Erin is blue. Erin is green. Erin is kind. Erin is nice. Erin is young. Gary is big. Gary is blue. Gary is green. Gary is nice. Gary is red. Gary is young. If someone is nice then they are young. If Gary is young then Gary is kind. If someone is big then they are green. If someone is red then they are kind. If someone is big and blue then they are red. If Gary is young and Gary is green then Gary is blue. If someone is kind then they are young. All red people are big.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is nice then they are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If Gary is young then Gary is kind.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "kind" "+"))
If someone is big then they are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone is red then they are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If someone is big and blue then they are red.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If Gary is young and Gary is green then Gary is blue.
((("Gary" "is" "young" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "blue" "+"))
If someone is kind then they are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Erin is young.
True
1
proof
[(triple10 OR ((triple8) -> rule7) OR ((triple9) -> rule1) OR ((((((triple5 triple6) -> rule5)) -> rule4)) -> rule7))]
("Erin" "is" "young" "+")
triple10
((triple8) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple9) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((((triple5 triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not big.
False
1
inv-proof
[(triple5)]
("Erin" "is" "big" "-")
triple5
Gary is kind.
True
2
proof
[(((triple15) -> rule4) OR ((triple16) -> rule2) OR ((((triple14) -> rule1)) -> rule2) OR ((((triple11 triple12) -> rule5)) -> rule4) OR ((((triple11 ((triple16 triple13) -> rule6)) -> rule5)) -> rule4) OR ((((triple11 ((triple16 ((triple11) -> rule3)) -> rule6)) -> rule5)) -> rule4) OR ((((triple11 ((((triple14) -> rule1) triple13) -> rule6)) -> rule5)) -> rule4) OR ((((triple11 ((((triple14) -> rule1) ((triple11) -> rule3)) -> rule6)) -> rule5)) -> rule4))]
("Gary" "is" "kind" "+")
((triple15) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple16) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple11 triple12) -> (rule5 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple11 ((triple16 triple13) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((triple11 ((triple16 ((triple11) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
((((triple11 ((((triple14) -> (rule1 % int4)) triple13) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
((((triple11 ((((triple14) -> (rule1 % int5)) ((triple11) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
int5
Erin is not red.
False
3
inv-proof
[(((triple5 triple6) -> rule5))]
("Erin" "is" "red" "-")
((triple5 triple6) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
@0: Dave is blue.[(triple1)] Dave is kind.[(triple2 OR ((triple4) -> rule4))] Dave is nice.[(triple3)] Dave is red.[(triple4)] Erin is big.[(triple5)] Erin is blue.[(triple6)] Erin is green.[(triple7 OR ((triple5) -> rule3))] Erin is kind.[(triple8 OR ((((triple5 triple6) -> rule5)) -> rule4))] Erin is nice.[(triple9)] Erin is young.[(triple10 OR ((triple8) -> rule7) OR ((triple9) -> rule1) OR ((((((triple5 triple6) -> rule5)) -> rule4)) -> rule7))] Gary is big.[(triple11 OR ((triple15) -> rule8))] Gary is blue.[(triple12 OR ((triple16 triple13) -> rule6) OR ((triple16 ((triple11) -> rule3)) -> rule6) OR ((((triple14) -> rule1) triple13) -> rule6) OR ((((triple14) -> rule1) ((triple11) -> rule3)) -> rule6) OR ((triple16 ((((triple15) -> rule8)) -> rule3)) -> rule6) OR ((((((triple15) -> rule4)) -> rule7) triple13) -> rule6) OR ((((triple14) -> rule1) ((((triple15) -> rule8)) -> rule3)) -> rule6) OR ((((((triple15) -> rule4)) -> rule7) ((triple11) -> rule3)) -> rule6) OR ((((((triple15) -> rule4)) -> rule7) ((((triple15) -> rule8)) -> rule3)) -> rule6))] Gary is green.[(triple13 OR ((triple11) -> rule3) OR ((((triple15) -> rule8)) -> rule3))] Gary is nice.[(triple14)] Gary is red.[(triple15 OR ((triple11 triple12) -> rule5) OR ((triple11 ((triple16 triple13) -> rule6)) -> rule5) OR ((triple11 ((triple16 ((triple11) -> rule3)) -> rule6)) -> rule5) OR ((triple11 ((((triple14) -> rule1) triple13) -> rule6)) -> rule5) OR ((triple11 ((((triple14) -> rule1) ((triple11) -> rule3)) -> rule6)) -> rule5))] Gary is young.[(triple16 OR ((triple14) -> rule1) OR ((((triple15) -> rule4)) -> rule7) OR ((((((triple11 triple12) -> rule5)) -> rule4)) -> rule7))] @1: Dave is big.[(((triple4) -> rule8))] Dave is young.[(((triple2) -> rule7) OR ((triple3) -> rule1) OR ((((triple4) -> rule4)) -> rule7))] Erin is red.[(((triple5 triple6) -> rule5))] Gary is kind.[(((triple15) -> rule4) OR ((triple16) -> rule2) OR ((((triple14) -> rule1)) -> rule2) OR ((((triple11 triple12) -> rule5)) -> rule4) OR ((((triple11 ((triple16 triple13) -> rule6)) -> rule5)) -> rule4) OR ((((triple11 ((triple16 ((triple11) -> rule3)) -> rule6)) -> rule5)) -> rule4) OR ((((triple11 ((((triple14) -> rule1) triple13) -> rule6)) -> rule5)) -> rule4) OR ((((triple11 ((((triple14) -> rule1) ((triple11) -> rule3)) -> rule6)) -> rule5)) -> rule4))] @2: Dave is green.[(((((triple4) -> rule8)) -> rule3))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
((triple4) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is green.
("Erin" "is" "green" "+")
triple7
((triple5) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple8
((((triple5 triple6) -> (rule5 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
((triple8) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple9) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((((triple5 triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
triple11
((triple15) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple12
((triple16 triple13) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple16 ((triple11) -> (rule3 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple14) -> (rule1 % int2)) triple13) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple14) -> (rule1 % int3)) ((triple11) -> (rule3 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
((triple16 ((((triple15) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((triple15) -> (rule4 % int3))) -> (rule7 % int2)) triple13) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((triple14) -> (rule1 % int4)) ((((triple15) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
((((((triple15) -> (rule4 % int4))) -> (rule7 % int3)) ((triple11) -> (rule3 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
((((((triple15) -> (rule4 % int5))) -> (rule7 % int4)) ((((triple15) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
int5
Gary is green.
("Gary" "is" "green" "+")
triple13
((triple11) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple15) -> (rule8 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple14
Gary is red.
("Gary" "is" "red" "+")
triple15
((triple11 triple12) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple11 ((triple16 triple13) -> (rule6 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple11 ((triple16 ((triple11) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((triple11 ((((triple14) -> (rule1 % int3)) triple13) -> (rule6 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
((triple11 ((((triple14) -> (rule1 % int4)) ((triple11) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
triple16
((triple14) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple15) -> (rule4 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((((triple11 triple12) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((triple4) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple2) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple3) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((triple5 triple6) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple15) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple16) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple11 triple12) -> (rule5 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple11 ((triple16 triple13) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((triple11 ((triple16 ((triple11) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
((((triple11 ((((triple14) -> (rule1 % int4)) triple13) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
((((triple11 ((((triple14) -> (rule1 % int5)) ((triple11) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
int5
Dave is green.
("Dave" "is" "green" "+")
((((triple4) -> (rule8 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2