Dave is blue. Dave is furry. Dave is green. Dave is red. Dave is rough. Erin is big. Erin is blue. Erin is furry. Erin is green. Erin is quiet. Erin is red. Erin is rough. All big things are quiet. Furry things are big. If Erin is green then Erin is rough.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If Erin is green then Erin is rough.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "rough" "+"))
Erin is furry.
True
1
proof
[(triple8)]
("Erin" "is" "furry" "+")
triple8
Erin is not red.
False
1
inv-proof
[(triple11)]
("Erin" "is" "red" "-")
triple11
Dave is big.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "big" "+")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "big" "-")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Dave" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not quiet.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Dave" "is" "quiet" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
@0: Dave is blue.[(triple1)] Dave is furry.[(triple2)] Dave is green.[(triple3)] Dave is red.[(triple4)] Dave is rough.[(triple5)] Erin is big.[(triple6 OR ((triple8) -> rule2))] Erin is blue.[(triple7)] Erin is furry.[(triple8)] Erin is green.[(triple9)] Erin is quiet.[(triple10 OR ((triple6) -> rule1) OR ((((triple8) -> rule2)) -> rule1))] Erin is red.[(triple11)] Erin is rough.[(triple12 OR ((triple9) -> rule3))] @1: Dave is big.[(((triple2) -> rule2))] @2: Dave is quiet.[(((((triple2) -> rule2)) -> rule1))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
((triple8) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
((triple6) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple11
Erin is rough.
("Erin" "is" "rough" "+")
triple12
((triple9) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2