Anne is furry. Anne is nice. Anne is round. Anne is smart. Dave is blue. Dave is furry. Dave is green. Dave is kind. Dave is nice. Dave is round. Dave is smart. Erin is furry. Erin is kind. Erin is nice. Erin is round. Erin is smart. If something is green and round then it is blue. All smart things are green.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If something is green and round then it is blue.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Anne is smart.
True
1
proof
[(triple4)]
("Anne" "is" "smart" "+")
triple4
Anne is not round.
False
1
inv-proof
[(triple3)]
("Anne" "is" "round" "-")
triple3
Erin is green.
True
2
proof
[(((triple16) -> rule2))]
("Erin" "is" "green" "+")
((triple16) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple16) -> rule2))]
("Erin" "is" "green" "-")
((triple16) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Anne is blue.
True
4
proof
[(((((triple4) -> rule2) triple3) -> rule1))]
("Anne" "is" "blue" "+")
((((triple4) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Erin is not blue.
False
4
inv-proof
[(((((triple16) -> rule2) triple15) -> rule1))]
("Erin" "is" "blue" "-")
((((triple16) -> (rule2 % int2)) triple15) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
@0: Anne is furry.[(triple1)] Anne is nice.[(triple2)] Anne is round.[(triple3)] Anne is smart.[(triple4)] Dave is blue.[(triple5 OR ((triple7 triple10) -> rule1) OR ((((triple11) -> rule2) triple10) -> rule1))] Dave is furry.[(triple6)] Dave is green.[(triple7 OR ((triple11) -> rule2))] Dave is kind.[(triple8)] Dave is nice.[(triple9)] Dave is round.[(triple10)] Dave is smart.[(triple11)] Erin is furry.[(triple12)] Erin is kind.[(triple13)] Erin is nice.[(triple14)] Erin is round.[(triple15)] Erin is smart.[(triple16)] @1: Anne is green.[(((triple4) -> rule2))] Erin is green.[(((triple16) -> rule2))] @2: Anne is blue.[(((((triple4) -> rule2) triple3) -> rule1))] Erin is blue.[(((((triple16) -> rule2) triple15) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
((triple7 triple10) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple11) -> (rule2 % int2)) triple10) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Dave is green.
("Dave" "is" "green" "+")
triple7
((triple11) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is nice.
("Dave" "is" "nice" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Dave is smart.
("Dave" "is" "smart" "+")
triple11
Erin is furry.
("Erin" "is" "furry" "+")
triple12
Erin is kind.
("Erin" "is" "kind" "+")
triple13
Erin is nice.
("Erin" "is" "nice" "+")
triple14
Erin is round.
("Erin" "is" "round" "+")
triple15
Erin is smart.
("Erin" "is" "smart" "+")
triple16
Anne is green.
("Anne" "is" "green" "+")
((triple4) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple16) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple4) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((((triple16) -> (rule2 % int2)) triple15) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2