Bob is big. Bob is furry. Bob is nice. Bob is red. Harry is big. Harry is not cold. Harry is red. Red people are big. If someone is nice then they are white. Big people are nice. If Bob is quiet then Bob is big. If someone is white then they are quiet. Nice people are furry. If Bob is not white then Bob is not furry. If someone is big and not quiet then they are cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is red.
("Harry" "is" "red" "+")
Red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is nice then they are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
Big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If Bob is quiet then Bob is big.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "big" "+"))
If someone is white then they are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If Bob is not white then Bob is not furry.
((("Bob" "is" "white" "~")) -> ("Bob" "is" "furry" "-"))
If someone is big and not quiet then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "cold" "+"))
Harry is not cold.
True
1
proof
[(triple6)]
("Harry" "is" "cold" "-")
triple6
Harry is not big.
False
1
inv-proof
[(triple5 OR ((triple7) -> rule1))]
("Harry" "is" "big" "-")
triple5
((triple7) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
True
2
proof
[(((triple5) -> rule3) OR ((((triple7) -> rule1)) -> rule3))]
("Harry" "is" "nice" "+")
((triple5) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not nice.
False
2
inv-proof
[(((triple5) -> rule3) OR ((((triple7) -> rule1)) -> rule3))]
("Harry" "is" "nice" "-")
((triple5) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
True
3
proof
[(((((triple5) -> rule3)) -> rule2) OR ((((((triple7) -> rule1)) -> rule3)) -> rule2))]
("Harry" "is" "white" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not white.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule2) OR ((((((triple7) -> rule1)) -> rule3)) -> rule2))]
("Harry" "is" "white" "-")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
@0: Bob is big.[(triple1 OR ((triple4) -> rule1) OR ((((((triple3) -> rule2)) -> rule5)) -> rule4))] Bob is furry.[(triple2 OR ((triple3) -> rule6) OR ((((triple1) -> rule3)) -> rule6) OR ((((((triple4) -> rule1)) -> rule3)) -> rule6))] Bob is nice.[(triple3 OR ((triple1) -> rule3) OR ((((triple4) -> rule1)) -> rule3))] Bob is red.[(triple4)] Harry is big.[(triple5 OR ((triple7) -> rule1))] Harry is not cold.[(triple6)] Harry is red.[(triple7)] @1: Bob is white.[(((triple3) -> rule2) OR ((((triple1) -> rule3)) -> rule2) OR ((((((triple4) -> rule1)) -> rule3)) -> rule2))] Harry is nice.[(((triple5) -> rule3) OR ((((triple7) -> rule1)) -> rule3))] @2: Bob is quiet.[(((((triple3) -> rule2)) -> rule5) OR ((((((triple1) -> rule3)) -> rule2)) -> rule5) OR ((((((((triple4) -> rule1)) -> rule3)) -> rule2)) -> rule5))] Harry is furry.[(((((triple5) -> rule3)) -> rule6) OR ((((((triple7) -> rule1)) -> rule3)) -> rule6))] Harry is white.[(((((triple5) -> rule3)) -> rule2) OR ((((((triple7) -> rule1)) -> rule3)) -> rule2))] @3: Harry is quiet.[(((((((triple5) -> rule3)) -> rule2)) -> rule5) OR ((((((((triple7) -> rule1)) -> rule3)) -> rule2)) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple4) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple3) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple1) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple4
Harry is big.
("Harry" "is" "big" "+")
triple5
((triple7) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
Bob is white.
("Bob" "is" "white" "+")
((triple3) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((triple5) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((((triple4) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((((((triple5) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((((triple7) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4