Dave is cold. Dave is furry. Dave is not smart. Dave is white. Dave is not young. Fiona is cold. Fiona is furry. Fiona is quiet. Fiona is round. Fiona is smart. Fiona is white. Fiona is young. If something is young then it is cold. If Fiona is smart then Fiona is cold. All quiet things are round. If Dave is young and Dave is round then Dave is white. If Dave is furry and Dave is white then Dave is quiet. If something is smart and not cold then it is quiet.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
Dave is white.
("Dave" "is" "white" "+")
Dave is not young.
("Dave" "is" "young" "-")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
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 something is young then it is cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If Fiona is smart then Fiona is cold.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "cold" "+"))
All quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If Dave is young and Dave is round then Dave is white.
((("Dave" "is" "young" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "white" "+"))
If Dave is furry and Dave is white then Dave is quiet.
((("Dave" "is" "furry" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "quiet" "+"))
If something is smart and not cold then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "cold" "~")) -> ("something" "is" "quiet" "+"))
Dave is not smart.
True
1
proof
[(triple3)]
("Dave" "is" "smart" "-")
triple3
Dave is young.
False
1
inv-proof
[(triple5)]
("Dave" "is" "young" "+")
triple5
Dave is quiet.
True
3
proof
[(((triple2 triple4) -> rule5))]
("Dave" "is" "quiet" "+")
((triple2 triple4) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
3
inv-proof
[(((triple2 triple4) -> rule5))]
("Dave" "is" "quiet" "-")
((triple2 triple4) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
True
4
proof
[(((((triple2 triple4) -> rule5)) -> rule3))]
("Dave" "is" "round" "+")
((((triple2 triple4) -> (rule5 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not round.
False
4
inv-proof
[(((((triple2 triple4) -> rule5)) -> rule3))]
("Dave" "is" "round" "-")
((((triple2 triple4) -> (rule5 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
@0: Dave is cold.[(triple1)] Dave is furry.[(triple2)] Dave is not smart.[(triple3)] Dave is not young.[(triple5)] Dave is white.[(triple4)] Fiona is cold.[(triple6 OR ((triple10) -> rule2) OR ((triple12) -> rule1))] Fiona is furry.[(triple7)] Fiona is quiet.[(triple8)] Fiona is round.[(triple9 OR ((triple8) -> rule3))] Fiona is smart.[(triple10)] Fiona is white.[(triple11)] Fiona is young.[(triple12)] @1: Dave is quiet.[(((triple2 triple4) -> rule5))] @2: Dave is round.[(((((triple2 triple4) -> rule5)) -> rule3))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is not smart.
("Dave" "is" "smart" "-")
triple3
Dave is not young.
("Dave" "is" "young" "-")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple4
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
((triple10) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple12) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
Fiona is round.
("Fiona" "is" "round" "+")
triple9
((triple8) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Fiona is white.
("Fiona" "is" "white" "+")
triple11
Fiona is young.
("Fiona" "is" "young" "+")
triple12
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2 triple4) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple2 triple4) -> (rule5 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2