Dave is not big. Dave is cold. Dave is furry. Dave is nice. Dave is red. Dave is smart. Dave is young. Fiona is not cold. Fiona is furry. Fiona is nice. Fiona is smart. Fiona is young. If Fiona is nice then Fiona is furry. If someone is smart and not cold then they are big. Nice people are smart. If Fiona is cold then Fiona is smart. If someone is red and nice then they are young. If someone is young and smart then they are nice. If someone is cold and not smart then they are furry. If someone is big and not smart then they are furry.
Dave is not big.
("Dave" "is" "big" "-")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If Fiona is nice then Fiona is furry.
((("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "furry" "+"))
If someone is smart and not cold then they are big.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "big" "+"))
Nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If Fiona is cold then Fiona is smart.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "smart" "+"))
If someone is red and nice then they are young.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone is young and smart then they are nice.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold and not smart then they are furry.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "furry" "+"))
If someone is big and not smart then they are furry.
((("someone" "is" "big" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "furry" "+"))
Dave is furry.
True
1
proof
[(triple3)]
("Dave" "is" "furry" "+")
triple3
Fiona is not furry.
False
1
inv-proof
[(triple9 OR ((triple10) -> rule1) OR ((((triple12 triple11) -> rule6)) -> rule1))]
("Fiona" "is" "furry" "-")
triple9
((triple10) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple12 triple11) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is big.
True
3
proof
[(((triple11 triple8) -> rule2) OR ((((triple10) -> rule3) triple8) -> rule2))]
("Fiona" "is" "big" "+")
((triple11 triple8) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple10) -> (rule3 % int2)) triple8) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not big.
False
3
inv-proof
[(((triple11 triple8) -> rule2) OR ((((triple10) -> rule3) triple8) -> rule2))]
("Fiona" "is" "big" "-")
((triple11 triple8) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple10) -> (rule3 % int2)) triple8) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
@0: Dave is cold.[(triple2)] Dave is furry.[(triple3)] Dave is nice.[(triple4 OR ((triple7 triple6) -> rule6))] Dave is not big.[(triple1)] Dave is red.[(triple5)] Dave is smart.[(triple6 OR ((triple4) -> rule3))] Dave is young.[(triple7 OR ((triple5 triple4) -> rule5))] Fiona is furry.[(triple9 OR ((triple10) -> rule1) OR ((((triple12 triple11) -> rule6)) -> rule1))] Fiona is nice.[(triple10 OR ((triple12 triple11) -> rule6))] Fiona is not cold.[(triple8)] Fiona is smart.[(triple11 OR ((triple10) -> rule3))] Fiona is young.[(triple12)] @1: Fiona is big.[(((triple11 triple8) -> rule2) OR ((((triple10) -> rule3) triple8) -> rule2))]
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
((triple7 triple6) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not big.
("Dave" "is" "big" "-")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
((triple4) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple5 triple4) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple9
((triple10) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple12 triple11) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
((triple12 triple11) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple8
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
((triple10) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple12
Fiona is big.
("Fiona" "is" "big" "+")
((triple11 triple8) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple10) -> (rule3 % int2)) triple8) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2