Dave is big. Dave is kind. Dave is nice. If Dave is white and Dave is big then Dave is blue. All blue, nice things are kind. Nice, red things are blue. All blue things are red. All nice things are red. If something is red and nice then it is big. All smart things are nice. All big things are white.
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
If Dave is white and Dave is big then Dave is blue.
((("Dave" "is" "white" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "blue" "+"))
All blue, nice things are kind.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Nice, red things are blue.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
All blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
All nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is red and nice then it is big.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
All smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
All big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Dave is nice.
True
1
proof
[(triple3)]
("Dave" "is" "nice" "+")
triple3
Dave is not big.
False
1
inv-proof
[(triple1 OR ((((triple3) -> rule5) triple3) -> rule6))]
("Dave" "is" "big" "-")
triple1
((((triple3) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
@0: Dave is big.[(triple1 OR ((((triple3) -> rule5) triple3) -> rule6))] Dave is kind.[(triple2 OR ((((triple3 ((triple3) -> rule5)) -> rule3) triple3) -> rule2) OR ((((((triple1) -> rule8) triple1) -> rule1) triple3) -> rule2) OR ((((((triple1) -> rule8) ((((triple3) -> rule5) triple3) -> rule6)) -> rule1) triple3) -> rule2) OR ((((((((((triple3) -> rule5) triple3) -> rule6)) -> rule8) triple1) -> rule1) triple3) -> rule2) OR ((((((((((triple3) -> rule5) triple3) -> rule6)) -> rule8) ((((triple3) -> rule5) triple3) -> rule6)) -> rule1) triple3) -> rule2))] Dave is nice.[(triple3)] @1: Dave is red.[(((triple3) -> rule5) OR ((((((triple1) -> rule8) triple1) -> rule1)) -> rule4))] Dave is white.[(((triple1) -> rule8) OR ((((((triple3) -> rule5) triple3) -> rule6)) -> rule8))] @2: Dave is blue.[(((triple3 ((triple3) -> rule5)) -> rule3) OR ((((triple1) -> rule8) triple1) -> rule1) OR ((((triple1) -> rule8) ((((triple3) -> rule5) triple3) -> rule6)) -> rule1) OR ((((((((triple3) -> rule5) triple3) -> rule6)) -> rule8) triple1) -> rule1) OR ((((((((triple3) -> rule5) triple3) -> rule6)) -> rule8) ((((triple3) -> rule5) triple3) -> rule6)) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((((triple3) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple2
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((triple1) -> (rule8 % int3)) triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((triple1) -> (rule8 % int5)) ((((triple3) -> (rule5 % int4)) triple3) -> (rule6 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
((((((((((triple3) -> (rule5 % int5)) triple3) -> (rule6 % int4))) -> (rule8 % int3)) triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5
((((((((((triple3) -> (rule5 % int5)) triple3) -> (rule6 % int4))) -> (rule8 % int3)) ((((triple3) -> (rule5 % int5)) triple3) -> (rule6 % int4))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
((triple3) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((((triple1) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((triple1) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((((triple3) -> (rule5 % int3)) triple3) -> (rule6 % int2))) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple1) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple1) -> (rule8 % int4)) ((((triple3) -> (rule5 % int3)) triple3) -> (rule6 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((((((triple3) -> (rule5 % int4)) triple3) -> (rule6 % int3))) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
((((((((triple3) -> (rule5 % int4)) triple3) -> (rule6 % int3))) -> (rule8 % int2)) ((((triple3) -> (rule5 % int4)) triple3) -> (rule6 % int3))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4