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