Anne is big. Anne is blue. Anne is kind. Anne is nice. Anne is quiet. Anne is red. Anne is young. Bob is big. Bob is blue. Bob is kind. Bob is quiet. Bob is young. Big people are quiet. All red, kind people are quiet. If Bob is nice then Bob is red. All kind people are red. If someone is nice then they are big. Red, kind people are young. Blue people are nice. If Bob is red then Bob is blue.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is young.
("Bob" "is" "young" "+")
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
All red, kind people are quiet.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is nice then Bob is red.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "red" "+"))
All kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Red, kind people are young.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If Bob is red then Bob is blue.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "blue" "+"))
Anne is big.
True
1
proof
[(triple1 OR ((triple4) -> rule5) OR ((((triple2) -> rule7)) -> rule5))]
("Anne" "is" "big" "+")
triple1
((triple4) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not red.
False
1
inv-proof
[(triple6 OR ((triple3) -> rule4))]
("Anne" "is" "red" "-")
triple6
((triple3) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
@0: Anne is big.[(triple1 OR ((triple4) -> rule5) OR ((((triple2) -> rule7)) -> rule5))] Anne is blue.[(triple2)] Anne is kind.[(triple3)] Anne is nice.[(triple4 OR ((triple2) -> rule7))] Anne is quiet.[(triple5 OR ((triple1) -> rule1) OR ((triple6 triple3) -> rule2) OR ((((triple4) -> rule5)) -> rule1) OR ((((triple3) -> rule4) triple3) -> rule2) OR ((((((triple2) -> rule7)) -> rule5)) -> rule1))] Anne is red.[(triple6 OR ((triple3) -> rule4))] Anne is young.[(triple7 OR ((triple6 triple3) -> rule6) OR ((((triple3) -> rule4) triple3) -> rule6))] Bob is big.[(triple8 OR ((((triple9) -> rule7)) -> rule5) OR ((((((((triple10) -> rule4)) -> rule8)) -> rule7)) -> rule5))] Bob is blue.[(triple9 OR ((((triple10) -> rule4)) -> rule8))] Bob is kind.[(triple10)] Bob is quiet.[(triple11 OR ((triple8) -> rule1) OR ((((triple10) -> rule4) triple10) -> rule2) OR ((((((triple9) -> rule7)) -> rule5)) -> rule1) OR ((((((triple9) -> rule7)) -> rule3) triple10) -> rule2) OR ((((((((((triple10) -> rule4)) -> rule8)) -> rule7)) -> rule5)) -> rule1))] Bob is young.[(triple12 OR ((((triple10) -> rule4) triple10) -> rule6) OR ((((((triple9) -> rule7)) -> rule3) triple10) -> rule6))] @1: Bob is nice.[(((triple9) -> rule7) OR ((((((triple10) -> rule4)) -> rule8)) -> rule7))] Bob is red.[(((triple10) -> rule4) OR ((((triple9) -> rule7)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple4) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple2) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple6 triple3) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple3) -> (rule4 % int2)) triple3) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((triple2) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
triple6
((triple3) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple6 triple3) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple3) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
triple8
((((triple9) -> (rule7 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((((triple10) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is blue.
("Bob" "is" "blue" "+")
triple9
((((triple10) -> (rule4 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple10
Bob is quiet.
("Bob" "is" "quiet" "+")
triple11
((triple8) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple10) -> (rule4 % int2)) triple10) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((((triple9) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((triple9) -> (rule7 % int3))) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((((((triple10) -> (rule4 % int5))) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
Bob is young.
("Bob" "is" "young" "+")
triple12
((((triple10) -> (rule4 % int2)) triple10) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((((triple9) -> (rule7 % int3))) -> (rule3 % int2)) triple10) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
((triple9) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((((triple10) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((triple10) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple9) -> (rule7 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2