Anne is big. Anne is blue. Anne is red. Anne is round. Anne is smart. Anne is white. Anne is young. Harry is big. Harry is red. Harry is smart. Harry is white. Harry is young. All white, big people are young. Blue people are round. All big, red people are young. Round people are young. All red, round people are blue. If someone is big then they are blue.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
All white, big people are young.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
All big, red people are young.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
All red, round people are blue.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is big then they are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Harry is big.
True
1
proof
[(triple8)]
("Harry" "is" "big" "+")
triple8
Harry is not white.
False
1
inv-proof
[(triple11)]
("Harry" "is" "white" "-")
triple11
Harry is blue.
True
2
proof
[(((triple8) -> rule6))]
("Harry" "is" "blue" "+")
((triple8) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple8) -> rule6))]
("Harry" "is" "blue" "-")
((triple8) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
True
3
proof
[(((((triple8) -> rule6)) -> rule2))]
("Harry" "is" "round" "+")
((((triple8) -> (rule6 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple8) -> rule6)) -> rule2))]
("Harry" "is" "round" "-")
((((triple8) -> (rule6 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple1) -> rule6) OR ((triple3 triple4) -> rule5))] Anne is red.[(triple3)] Anne is round.[(triple4 OR ((triple2) -> rule2) OR ((((triple1) -> rule6)) -> rule2))] Anne is smart.[(triple5)] Anne is white.[(triple6)] Anne is young.[(triple7 OR ((triple4) -> rule4) OR ((triple1 triple3) -> rule3) OR ((triple6 triple1) -> rule1) OR ((((triple2) -> rule2)) -> rule4) OR ((((((triple1) -> rule6)) -> rule2)) -> rule4))] Harry is big.[(triple8)] Harry is red.[(triple9)] Harry is smart.[(triple10)] Harry is white.[(triple11)] Harry is young.[(triple12 OR ((triple11 triple8) -> rule1) OR ((triple8 triple9) -> rule3) OR ((((((triple8) -> rule6)) -> rule2)) -> rule4))] @1: Harry is blue.[(((triple8) -> rule6))] @2: Harry is round.[(((((triple8) -> rule6)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple3 triple4) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
((triple2) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple4) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple1 triple3) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple6 triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Harry is white.
("Harry" "is" "white" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple11 triple8) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple8 triple9) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((((triple8) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
((triple8) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple8) -> (rule6 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2