Bob is big. Bob is blue. Bob is red. Bob is rough. Erin is big. Erin is blue. Erin is kind. Erin is red. Erin is smart. Erin is white. If someone is kind and blue then they are white. If Bob is white then Bob is big. If someone is smart then they are white. All blue, white people are smart. All smart, big people are white. All blue people are kind.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
If someone is kind and blue then they are white.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If Bob is white then Bob is big.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "big" "+"))
If someone is smart then they are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
All blue, white people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
All smart, big people are white.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Erin is smart.
True
1
proof
[(triple9 OR ((triple6 triple10) -> rule4) OR ((triple6 ((triple7 triple6) -> rule1)) -> rule4) OR ((triple6 ((((triple6) -> rule6) triple6) -> rule1)) -> rule4))]
("Erin" "is" "smart" "+")
triple9
((triple6 triple10) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple6 ((triple7 triple6) -> (rule1 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple6 ((((triple6) -> (rule6 % int3)) triple6) -> (rule1 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Bob is not big.
False
1
inv-proof
[(triple1 OR ((((((triple2) -> rule6) triple2) -> rule1)) -> rule2))]
("Bob" "is" "big" "-")
triple1
((((((triple2) -> (rule6 % int3)) triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is kind.
True
2
proof
[(((triple2) -> rule6))]
("Bob" "is" "kind" "+")
((triple2) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple2) -> rule6))]
("Bob" "is" "kind" "-")
((triple2) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
True
4
proof
[(((((triple2) -> rule6) triple2) -> rule1))]
("Bob" "is" "white" "+")
((((triple2) -> (rule6 % int2)) triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not white.
False
4
inv-proof
[(((((triple2) -> rule6) triple2) -> rule1))]
("Bob" "is" "white" "-")
((((triple2) -> (rule6 % int2)) triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
True
6
proof
[(((triple2 ((((triple2) -> rule6) triple2) -> rule1)) -> rule4))]
("Bob" "is" "smart" "+")
((triple2 ((((triple2) -> (rule6 % int3)) triple2) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not smart.
False
6
inv-proof
[(((triple2 ((((triple2) -> rule6) triple2) -> rule1)) -> rule4))]
("Bob" "is" "smart" "-")
((triple2 ((((triple2) -> (rule6 % int3)) triple2) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
@0: Bob is big.[(triple1 OR ((((((triple2) -> rule6) triple2) -> rule1)) -> rule2))] Bob is blue.[(triple2)] Bob is red.[(triple3)] Bob is rough.[(triple4)] Erin is big.[(triple5)] Erin is blue.[(triple6)] Erin is kind.[(triple7 OR ((triple6) -> rule6))] Erin is red.[(triple8)] Erin is smart.[(triple9 OR ((triple6 triple10) -> rule4) OR ((triple6 ((triple7 triple6) -> rule1)) -> rule4) OR ((triple6 ((((triple6) -> rule6) triple6) -> rule1)) -> rule4))] Erin is white.[(triple10 OR ((triple9) -> rule3) OR ((triple7 triple6) -> rule1) OR ((triple9 triple5) -> rule5) OR ((((triple6) -> rule6) triple6) -> rule1))] @1: Bob is kind.[(((triple2) -> rule6))] @2: Bob is white.[(((((triple2) -> rule6) triple2) -> rule1))] @3: Bob is smart.[(((triple2 ((((triple2) -> rule6) triple2) -> rule1)) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((((((triple2) -> (rule6 % int3)) triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple7
((triple6) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple8
Erin is smart.
("Erin" "is" "smart" "+")
triple9
((triple6 triple10) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple6 ((triple7 triple6) -> (rule1 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple6 ((((triple6) -> (rule6 % int3)) triple6) -> (rule1 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
triple10
((triple9) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple7 triple6) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple9 triple5) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple6) -> (rule6 % int2)) triple6) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple2) -> (rule6 % int2)) triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((triple2 ((((triple2) -> (rule6 % int3)) triple2) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3