Dave is big. Dave is cold. Dave is furry. Dave is kind. Dave is quiet. Dave is white. Dave is young. Fiona is big. Fiona is cold. Fiona is furry. Fiona is kind. Fiona is quiet. Fiona is white. Fiona is young. If someone is furry then they are big.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If someone is furry then they are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Fiona is big.
True
1
proof
[(triple8 OR ((triple10) -> rule1))]
("Fiona" "is" "big" "+")
triple8
((triple10) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not quiet.
False
1
inv-proof
[(triple12)]
("Fiona" "is" "quiet" "-")
triple12
@0: Dave is big.[(triple1 OR ((triple3) -> rule1))] Dave is cold.[(triple2)] Dave is furry.[(triple3)] Dave is kind.[(triple4)] Dave is quiet.[(triple5)] Dave is white.[(triple6)] Dave is young.[(triple7)] Fiona is big.[(triple8 OR ((triple10) -> rule1))] Fiona is cold.[(triple9)] Fiona is furry.[(triple10)] Fiona is kind.[(triple11)] Fiona is quiet.[(triple12)] Fiona is white.[(triple13)] Fiona is young.[(triple14)]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple3) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
triple8
((triple10) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple9
Fiona is furry.
("Fiona" "is" "furry" "+")
triple10
Fiona is kind.
("Fiona" "is" "kind" "+")
triple11
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple12
Fiona is white.
("Fiona" "is" "white" "+")
triple13
Fiona is young.
("Fiona" "is" "young" "+")
triple14