Dave is big. Dave is blue. Dave is not green. Dave is kind. Dave is nice. Dave is not round. Dave is young. Fiona is big. Fiona is blue. Fiona is green. Fiona is kind. Fiona is nice. Fiona is round. Fiona is young. All young things are blue. If Fiona is round and Fiona is not big then Fiona is green.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not round.
("Dave" "is" "round" "-")
Dave is young.
("Dave" "is" "young" "+")
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 young.
("Fiona" "is" "young" "+")
All young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If Fiona is round and Fiona is not big then Fiona is green.
((("Fiona" "is" "round" "+") ("Fiona" "is" "big" "~")) -> ("Fiona" "is" "green" "+"))
Fiona is blue.
True
1
proof
[(triple9 OR ((triple14) -> rule1))]
("Fiona" "is" "blue" "+")
triple9
((triple14) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is not nice.
False
1
inv-proof
[(triple12)]
("Fiona" "is" "nice" "-")
triple12
@0: Dave is big.[(triple1)] Dave is blue.[(triple2 OR ((triple7) -> rule1))] Dave is kind.[(triple4)] Dave is nice.[(triple5)] Dave is not green.[(triple3)] Dave is not round.[(triple6)] Dave is young.[(triple7)] Fiona is big.[(triple8)] Fiona is blue.[(triple9 OR ((triple14) -> rule1))] Fiona is green.[(triple10)] Fiona is kind.[(triple11)] Fiona is nice.[(triple12)] Fiona is round.[(triple13)] Fiona is young.[(triple14)]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
((triple7) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is not green.
("Dave" "is" "green" "-")
triple3
Dave is not round.
("Dave" "is" "round" "-")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
triple8
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
((triple14) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple10
Fiona is kind.
("Fiona" "is" "kind" "+")
triple11
Fiona is nice.
("Fiona" "is" "nice" "+")
triple12
Fiona is round.
("Fiona" "is" "round" "+")
triple13
Fiona is young.
("Fiona" "is" "young" "+")
triple14