Dave is blue. Dave is furry. Dave is green. Dave is kind. Dave is nice. Dave is red. Dave is smart. All smart people are nice. Red, kind people are smart. If someone is kind then they are smart. All nice, green people are smart. All red, green people are blue. If Dave is kind and Dave is nice then Dave is green. All furry, red people are nice. Green people are smart.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Red, kind people are smart.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is kind then they are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
All nice, green people are smart.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
All red, green people are blue.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If Dave is kind and Dave is nice then Dave is green.
((("Dave" "is" "kind" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "green" "+"))
All furry, red people are nice.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Dave is blue.
True
1
proof
[(triple1 OR ((triple6 triple3) -> rule5) OR ((triple6 ((triple4 triple5) -> rule6)) -> rule5) OR ((triple6 ((triple4 ((triple7) -> rule1)) -> rule6)) -> rule5) OR ((triple6 ((triple4 ((triple2 triple6) -> rule7)) -> rule6)) -> rule5) OR ((triple6 ((triple4 ((((triple4) -> rule3)) -> rule1)) -> rule6)) -> rule5) OR ((triple6 ((triple4 ((((triple6 triple4) -> rule2)) -> rule1)) -> rule6)) -> rule5))]
("Dave" "is" "blue" "+")
triple1
((triple6 triple3) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple6 ((triple4 triple5) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((triple6 ((triple4 ((triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((triple6 ((triple4 ((triple2 triple6) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((triple6 ((triple4 ((((triple4) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
((triple6 ((triple4 ((((triple6 triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is not furry.
False
1
inv-proof
[(triple2)]
("Dave" "is" "furry" "-")
triple2
@0: Dave is blue.[(triple1 OR ((triple6 triple3) -> rule5) OR ((triple6 ((triple4 triple5) -> rule6)) -> rule5) OR ((triple6 ((triple4 ((triple7) -> rule1)) -> rule6)) -> rule5) OR ((triple6 ((triple4 ((triple2 triple6) -> rule7)) -> rule6)) -> rule5) OR ((triple6 ((triple4 ((((triple4) -> rule3)) -> rule1)) -> rule6)) -> rule5) OR ((triple6 ((triple4 ((((triple6 triple4) -> rule2)) -> rule1)) -> rule6)) -> rule5))] Dave is furry.[(triple2)] Dave is green.[(triple3 OR ((triple4 triple5) -> rule6) OR ((triple4 ((triple7) -> rule1)) -> rule6) OR ((triple4 ((triple2 triple6) -> rule7)) -> rule6) OR ((triple4 ((((triple4) -> rule3)) -> rule1)) -> rule6) OR ((triple4 ((((triple6 triple4) -> rule2)) -> rule1)) -> rule6))] Dave is kind.[(triple4)] Dave is nice.[(triple5 OR ((triple7) -> rule1) OR ((triple2 triple6) -> rule7) OR ((((triple3) -> rule8)) -> rule1) OR ((((triple4) -> rule3)) -> rule1) OR ((((triple6 triple4) -> rule2)) -> rule1))] Dave is red.[(triple6)] Dave is smart.[(triple7 OR ((triple3) -> rule8) OR ((triple4) -> rule3) OR ((triple5 triple3) -> rule4) OR ((triple6 triple4) -> rule2) OR ((((triple4 triple5) -> rule6)) -> rule8) OR ((triple5 ((triple4 triple5) -> rule6)) -> rule4) OR ((((triple2 triple6) -> rule7) triple3) -> rule4) OR ((((triple2 triple6) -> rule7) ((triple4 triple5) -> rule6)) -> rule4) OR ((((triple4 ((triple2 triple6) -> rule7)) -> rule6)) -> rule8) OR ((triple5 ((triple4 ((triple2 triple6) -> rule7)) -> rule6)) -> rule4) OR ((((triple2 triple6) -> rule7) ((triple4 ((triple2 triple6) -> rule7)) -> rule6)) -> rule4))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple6 triple3) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple6 ((triple4 triple5) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((triple6 ((triple4 ((triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((triple6 ((triple4 ((triple2 triple6) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((triple6 ((triple4 ((((triple4) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
((triple6 ((triple4 ((((triple6 triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
((triple4 triple5) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple4 ((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((triple4 ((triple2 triple6) -> (rule7 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((triple4 ((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((triple4 ((((triple6 triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
((triple7) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple2 triple6) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple6 triple4) -> (rule2 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
((triple3) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple4) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple5 triple3) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple6 triple4) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple4 triple5) -> (rule6 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((triple5 ((triple4 triple5) -> (rule6 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple2 triple6) -> (rule7 % int2)) triple3) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple2 triple6) -> (rule7 % int3)) ((triple4 triple5) -> (rule6 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((triple4 ((triple2 triple6) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((triple5 ((triple4 ((triple2 triple6) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((triple2 triple6) -> (rule7 % int3)) ((triple4 ((triple2 triple6) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3