Dave is big. Dave is blue. Dave is green. Dave is kind. Dave is nice. Dave is round. Dave is smart. Fiona is big. Fiona is blue. Fiona is green. Fiona is kind. Fiona is nice. Fiona is round. Fiona is smart. If something is green then it is big. Smart, kind things are big. All green, big things are blue. If something is nice and blue then it is big. Green, kind things are smart. If something is round and smart then it is kind.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If something is green then it is big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
Smart, kind things are big.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
All green, big things are blue.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is nice and blue then it is big.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Green, kind things are smart.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If something is round and smart then it is kind.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Dave is round.
True
1
proof
[(triple6)]
("Dave" "is" "round" "+")
triple6
Dave is not blue.
False
1
inv-proof
[(triple2 OR ((triple3 triple1) -> rule3) OR ((triple3 ((triple3) -> rule1)) -> rule3) OR ((triple3 ((triple7 triple4) -> rule2)) -> rule3) OR ((triple3 ((triple7 ((triple6 triple7) -> rule6)) -> rule2)) -> rule3) OR ((triple3 ((((triple3 triple4) -> rule5) triple4) -> rule2)) -> rule3) OR ((triple3 ((((triple3 triple4) -> rule5) ((triple6 triple7) -> rule6)) -> rule2)) -> rule3))]
("Dave" "is" "blue" "-")
triple2
((triple3 triple1) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple3 ((triple7 triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple3 ((triple7 ((triple6 triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((triple3 ((((triple3 triple4) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((triple3 ((((triple3 triple4) -> (rule5 % int4)) ((triple6 triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
@0: Dave is big.[(triple1 OR ((triple3) -> rule1) OR ((triple5 triple2) -> rule4) OR ((triple7 triple4) -> rule2) OR ((triple7 ((triple6 triple7) -> rule6)) -> rule2) OR ((((triple3 triple4) -> rule5) triple4) -> rule2) OR ((((triple3 triple4) -> rule5) ((triple6 triple7) -> rule6)) -> rule2))] Dave is blue.[(triple2 OR ((triple3 triple1) -> rule3) OR ((triple3 ((triple3) -> rule1)) -> rule3) OR ((triple3 ((triple7 triple4) -> rule2)) -> rule3) OR ((triple3 ((triple7 ((triple6 triple7) -> rule6)) -> rule2)) -> rule3) OR ((triple3 ((((triple3 triple4) -> rule5) triple4) -> rule2)) -> rule3) OR ((triple3 ((((triple3 triple4) -> rule5) ((triple6 triple7) -> rule6)) -> rule2)) -> rule3))] Dave is green.[(triple3)] Dave is kind.[(triple4 OR ((triple6 triple7) -> rule6))] Dave is nice.[(triple5)] Dave is round.[(triple6)] Dave is smart.[(triple7 OR ((triple3 triple4) -> rule5))] Fiona is big.[(triple8 OR ((triple10) -> rule1) OR ((triple12 triple9) -> rule4) OR ((triple14 triple11) -> rule2) OR ((triple14 ((triple13 triple14) -> rule6)) -> rule2) OR ((((triple10 triple11) -> rule5) triple11) -> rule2) OR ((((triple10 triple11) -> rule5) ((triple13 triple14) -> rule6)) -> rule2))] Fiona is blue.[(triple9 OR ((triple10 triple8) -> rule3) OR ((triple10 ((triple10) -> rule1)) -> rule3) OR ((triple10 ((triple14 triple11) -> rule2)) -> rule3) OR ((triple10 ((triple14 ((triple13 triple14) -> rule6)) -> rule2)) -> rule3) OR ((triple10 ((((triple10 triple11) -> rule5) triple11) -> rule2)) -> rule3) OR ((triple10 ((((triple10 triple11) -> rule5) ((triple13 triple14) -> rule6)) -> rule2)) -> rule3))] Fiona is green.[(triple10)] Fiona is kind.[(triple11 OR ((triple13 triple14) -> rule6))] Fiona is nice.[(triple12)] Fiona is round.[(triple13)] Fiona is smart.[(triple14 OR ((triple10 triple11) -> rule5))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple3) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple5 triple2) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple7 triple4) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple7 ((triple6 triple7) -> (rule6 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple3 triple4) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple3 triple4) -> (rule5 % int3)) ((triple6 triple7) -> (rule6 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
triple2
((triple3 triple1) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple3 ((triple7 triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple3 ((triple7 ((triple6 triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((triple3 ((((triple3 triple4) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((triple3 ((((triple3 triple4) -> (rule5 % int4)) ((triple6 triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
((triple6 triple7) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
((triple3 triple4) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple8
((triple10) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple12 triple9) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple14 triple11) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple14 ((triple13 triple14) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple10 triple11) -> (rule5 % int2)) triple11) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple10 triple11) -> (rule5 % int3)) ((triple13 triple14) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
((triple10 triple8) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple10 ((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((triple10 ((triple14 triple11) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((triple10 ((triple14 ((triple13 triple14) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((triple10 ((((triple10 triple11) -> (rule5 % int3)) triple11) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
((triple10 ((((triple10 triple11) -> (rule5 % int4)) ((triple13 triple14) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
triple10
Fiona is kind.
("Fiona" "is" "kind" "+")
triple11
((triple13 triple14) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple12
Fiona is round.
("Fiona" "is" "round" "+")
triple13
Fiona is smart.
("Fiona" "is" "smart" "+")
triple14
((triple10 triple11) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1