Dave is blue. Dave is not nice. Dave is quiet. Dave is round. Dave is smart. Fiona is blue. Fiona is furry. Fiona is nice. Fiona is quiet. Fiona is round. Fiona is not smart. Fiona is not white. If someone is nice and smart then they are furry. Round people are furry. If someone is nice then they are round. If someone is quiet then they are round. If Dave is not blue then Dave is smart. If Fiona is blue then Fiona is nice.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is not smart.
("Fiona" "is" "smart" "-")
Fiona is not white.
("Fiona" "is" "white" "-")
If someone is nice and smart then they are furry.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
Round people are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is quiet then they are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If Dave is not blue then Dave is smart.
((("Dave" "is" "blue" "~")) -> ("Dave" "is" "smart" "+"))
If Fiona is blue then Fiona is nice.
((("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "nice" "+"))
Fiona is not smart.
True
1
proof
[(triple11)]
("Fiona" "is" "smart" "-")
triple11
Fiona is not furry.
False
1
inv-proof
[(triple7 OR ((triple10) -> rule2) OR ((((triple8) -> rule3)) -> rule2) OR ((((triple9) -> rule4)) -> rule2) OR ((((((triple6) -> rule6)) -> rule3)) -> rule2))]
("Fiona" "is" "furry" "-")
triple7
((triple10) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((triple9) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Dave is furry.
True
2
proof
[(((triple4) -> rule2) OR ((((triple3) -> rule4)) -> rule2))]
("Dave" "is" "furry" "+")
((triple4) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not furry.
False
2
inv-proof
[(((triple4) -> rule2) OR ((((triple3) -> rule4)) -> rule2))]
("Dave" "is" "furry" "-")
((triple4) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
@0: Dave is blue.[(triple1)] Dave is not nice.[(triple2)] Dave is quiet.[(triple3)] Dave is round.[(triple4 OR ((triple3) -> rule4))] Dave is smart.[(triple5)] Fiona is blue.[(triple6)] Fiona is furry.[(triple7 OR ((triple10) -> rule2) OR ((((triple8) -> rule3)) -> rule2) OR ((((triple9) -> rule4)) -> rule2) OR ((((((triple6) -> rule6)) -> rule3)) -> rule2))] Fiona is nice.[(triple8 OR ((triple6) -> rule6))] Fiona is not smart.[(triple11)] Fiona is not white.[(triple12)] Fiona is quiet.[(triple9)] Fiona is round.[(triple10 OR ((triple8) -> rule3) OR ((triple9) -> rule4) OR ((((triple6) -> rule6)) -> rule3))] @1: Dave is furry.[(((triple4) -> rule2) OR ((((triple3) -> rule4)) -> rule2))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is not nice.
("Dave" "is" "nice" "-")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
((triple3) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
((triple10) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((triple9) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple8
((triple6) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not smart.
("Fiona" "is" "smart" "-")
triple11
Fiona is not white.
("Fiona" "is" "white" "-")
triple12
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
((triple8) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple9) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((triple4) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2