Anne is big. Anne is blue. Anne is not furry. Anne is smart. Dave is big. Dave is not blue. Dave is not furry. Dave is rough. Dave is smart. Dave is not young. If someone is blue then they are smart. All young, big people are red. If someone is smart then they are red. All blue, smart people are red. If Anne is blue then Anne is big. If Dave is red and Dave is furry then Dave is not young. Furry people are blue. All blue, big people are not rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is not furry.
("Anne" "is" "furry" "-")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is not young.
("Dave" "is" "young" "-")
If someone is blue then they are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
All young, big people are red.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is smart then they are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
All blue, smart people are red.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If Anne is blue then Anne is big.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "big" "+"))
If Dave is red and Dave is furry then Dave is not young.
((("Dave" "is" "red" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "young" "-"))
Furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
All blue, big people are not rough.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "-"))
Anne is not furry.
True
1
proof
[(triple3)]
("Anne" "is" "furry" "-")
triple3
Anne is not smart.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule1))]
("Anne" "is" "smart" "-")
triple4
((triple2) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
True
2
proof
[(((triple4) -> rule3) OR ((triple2 triple4) -> rule4) OR ((((triple2) -> rule1)) -> rule3) OR ((triple2 ((triple2) -> rule1)) -> rule4))]
("Anne" "is" "red" "+")
((triple4) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2 triple4) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not red.
False
2
inv-proof
[(((triple4) -> rule3) OR ((triple2 triple4) -> rule4) OR ((((triple2) -> rule1)) -> rule3) OR ((triple2 ((triple2) -> rule1)) -> rule4))]
("Anne" "is" "red" "-")
((triple4) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2 triple4) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
@0: Anne is big.[(triple1 OR ((triple2) -> rule5))] Anne is blue.[(triple2)] Anne is not furry.[(triple3)] Anne is smart.[(triple4 OR ((triple2) -> rule1))] Dave is big.[(triple5)] Dave is not blue.[(triple6)] Dave is not furry.[(triple7)] Dave is not young.[(triple10)] Dave is rough.[(triple8)] Dave is smart.[(triple9)] @1: Anne is not rough.[(((triple2 triple1) -> rule8) OR ((triple2 ((triple2) -> rule5)) -> rule8))] Anne is red.[(((triple4) -> rule3) OR ((triple2 triple4) -> rule4) OR ((((triple2) -> rule1)) -> rule3) OR ((triple2 ((triple2) -> rule1)) -> rule4))] Dave is red.[(((triple9) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is not furry.
("Anne" "is" "furry" "-")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
((triple2) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is not blue.
("Dave" "is" "blue" "-")
triple6
Dave is not furry.
("Dave" "is" "furry" "-")
triple7
Dave is not young.
("Dave" "is" "young" "-")
triple10
Dave is rough.
("Dave" "is" "rough" "+")
triple8
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Anne is not rough.
("Anne" "is" "rough" "-")
((triple2 triple1) -> (rule8 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
((triple2 ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((triple4) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2 triple4) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((triple9) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1