Anne is blue. Anne is round. Anne is young. Erin is blue. Erin is furry. Erin is green. Erin is rough. Erin is not round. Erin is smart. Erin is young. All young, round things are rough. If Anne is blue then Anne is young. If Anne is not round and Anne is not blue then Anne is young. All rough, smart things are young. If Erin is not blue then Erin is rough. If Anne is round and Anne is rough then Anne is not smart. If something is rough and not young then it is furry. If something is rough then it is furry.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is not round.
("Erin" "is" "round" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
All young, round things are rough.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If Anne is blue then Anne is young.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "young" "+"))
If Anne is not round and Anne is not blue then Anne is young.
((("Anne" "is" "round" "~") ("Anne" "is" "blue" "~")) -> ("Anne" "is" "young" "+"))
All rough, smart things are young.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If Erin is not blue then Erin is rough.
((("Erin" "is" "blue" "~")) -> ("Erin" "is" "rough" "+"))
If Anne is round and Anne is rough then Anne is not smart.
((("Anne" "is" "round" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "smart" "-"))
If something is rough and not young then it is furry.
((("something" "is" "rough" "+") ("something" "is" "young" "~")) -> ("something" "is" "furry" "+"))
If something is rough then it is furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
Erin is blue.
True
1
proof
[(triple4)]
("Erin" "is" "blue" "+")
triple4
Erin is not blue.
False
1
inv-proof
[(triple4)]
("Erin" "is" "blue" "-")
triple4
Anne is rough.
True
3
proof
[(((triple3 triple2) -> rule1) OR ((((triple1) -> rule2) triple2) -> rule1))]
("Anne" "is" "rough" "+")
((triple3 triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not rough.
False
3
inv-proof
[(((triple3 triple2) -> rule1) OR ((((triple1) -> rule2) triple2) -> rule1))]
("Anne" "is" "rough" "-")
((triple3 triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
True
4
proof
[(((((triple3 triple2) -> rule1)) -> rule8) OR ((((((triple1) -> rule2) triple2) -> rule1)) -> rule8))]
("Anne" "is" "furry" "+")
((((triple3 triple2) -> (rule1 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((((triple1) -> (rule2 % int3)) triple2) -> (rule1 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not furry.
False
4
inv-proof
[(((((triple3 triple2) -> rule1)) -> rule8) OR ((((((triple1) -> rule2) triple2) -> rule1)) -> rule8))]
("Anne" "is" "furry" "-")
((((triple3 triple2) -> (rule1 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((((triple1) -> (rule2 % int3)) triple2) -> (rule1 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
@0: Anne is blue.[(triple1)] Anne is round.[(triple2)] Anne is young.[(triple3 OR ((triple1) -> rule2))] Erin is blue.[(triple4)] Erin is furry.[(triple5 OR ((triple7) -> rule8))] Erin is green.[(triple6)] Erin is not round.[(triple8)] Erin is rough.[(triple7)] Erin is smart.[(triple9)] Erin is young.[(triple10 OR ((triple7 triple9) -> rule4))] @1: Anne is rough.[(((triple3 triple2) -> rule1) OR ((((triple1) -> rule2) triple2) -> rule1))] @2: Anne is furry.[(((((triple3 triple2) -> rule1)) -> rule8) OR ((((((triple1) -> rule2) triple2) -> rule1)) -> rule8))] Anne is not smart.[(((triple2 ((triple3 triple2) -> rule1)) -> rule6) OR ((triple2 ((((triple1) -> rule2) triple2) -> rule1)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
triple5
((triple7) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is not round.
("Erin" "is" "round" "-")
triple8
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
((triple7 triple9) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple3 triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((triple3 triple2) -> (rule1 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((((triple1) -> (rule2 % int3)) triple2) -> (rule1 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not smart.
("Anne" "is" "smart" "-")
((triple2 ((triple3 triple2) -> (rule1 % int2))) -> (rule6 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((triple2 ((((triple1) -> (rule2 % int3)) triple2) -> (rule1 % int2))) -> (rule6 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3