Dave is big. Dave is furry. Dave is quiet. Dave is young. Fiona is big. Fiona is not furry. Fiona is green. Fiona is quiet. Fiona is red. Fiona is round. If Fiona is quiet and Fiona is not furry then Fiona is young. All red people are young. If someone is green and quiet then they are young. Quiet people are young. If someone is quiet then they are big. If Dave is furry and Dave is quiet then Dave is round. All young, furry people are red. If someone is red and not big then they are not round.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is not furry.
("Fiona" "is" "furry" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If Fiona is quiet and Fiona is not furry then Fiona is young.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "furry" "~")) -> ("Fiona" "is" "young" "+"))
All red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is green and quiet then they are young.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
Quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If someone is quiet then they are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If Dave is furry and Dave is quiet then Dave is round.
((("Dave" "is" "furry" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "round" "+"))
All young, furry people are red.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If someone is red and not big then they are not round.
((("someone" "is" "red" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "round" "-"))
Dave is big.
True
1
proof
[(triple1 OR ((triple3) -> rule5))]
("Dave" "is" "big" "+")
triple1
((triple3) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Fiona is not round.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "round" "-")
triple10
Dave is round.
True
3
proof
[(((triple2 triple3) -> rule6))]
("Dave" "is" "round" "+")
((triple2 triple3) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple8) -> rule4) OR ((triple9) -> rule2) OR ((triple7 triple8) -> rule3) OR ((triple8 triple6) -> rule1))]
("Fiona" "is" "young" "-")
((triple8) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple9) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple7 triple8) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple8 triple6) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
@0: Dave is big.[(triple1 OR ((triple3) -> rule5))] Dave is furry.[(triple2)] Dave is quiet.[(triple3)] Dave is young.[(triple4 OR ((triple3) -> rule4))] Fiona is big.[(triple5 OR ((triple8) -> rule5))] Fiona is green.[(triple7)] Fiona is not furry.[(triple6)] Fiona is quiet.[(triple8)] Fiona is red.[(triple9)] Fiona is round.[(triple10)] @1: Dave is red.[(((triple4 triple2) -> rule7) OR ((((triple3) -> rule4) triple2) -> rule7))] Dave is round.[(((triple2 triple3) -> rule6))] Fiona is young.[(((triple8) -> rule4) OR ((triple9) -> rule2) OR ((triple7 triple8) -> rule3) OR ((triple8 triple6) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple3) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
((triple3) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple5
((triple8) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple7
Fiona is not furry.
("Fiona" "is" "furry" "-")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
Fiona is red.
("Fiona" "is" "red" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
Dave is red.
("Dave" "is" "red" "+")
((triple4 triple2) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple3) -> (rule4 % int2)) triple2) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((triple2 triple3) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple8) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple9) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple7 triple8) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple8 triple6) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1