Bob is big. Bob is green. Bob is nice. Bob is young. Erin is not big. Erin is blue. Erin is green. Erin is red. Erin is not white. Erin is young. All big, green things are white. Big, blue things are young. All red, blue things are young. Blue things are red. If Bob is white then Bob is blue. If Erin is big then Erin is green. All young things are nice. If something is big and not young then it is nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is not big.
("Erin" "is" "big" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not white.
("Erin" "is" "white" "-")
Erin is young.
("Erin" "is" "young" "+")
All big, green things are white.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Big, blue things are young.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All red, blue things are young.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If Bob is white then Bob is blue.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "blue" "+"))
If Erin is big then Erin is green.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "green" "+"))
All young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is big and not young then it is nice.
((("something" "is" "big" "+") ("something" "is" "young" "~")) -> ("something" "is" "nice" "+"))
Erin is blue.
True
1
proof
[(triple6)]
("Erin" "is" "blue" "+")
triple6
Erin is not blue.
False
1
inv-proof
[(triple6)]
("Erin" "is" "blue" "-")
triple6
Erin is nice.
True
2
proof
[(((triple10) -> rule7) OR ((((triple8 triple6) -> rule3)) -> rule7) OR ((((((triple6) -> rule4) triple6) -> rule3)) -> rule7))]
("Erin" "is" "nice" "+")
((triple10) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple8 triple6) -> (rule3 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((((triple6) -> (rule4 % int3)) triple6) -> (rule3 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Bob is not white.
False
3
inv-proof
[(((triple1 triple2) -> rule1))]
("Bob" "is" "white" "-")
((triple1 triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
True
4
proof
[(((((triple1 triple2) -> rule1)) -> rule5))]
("Bob" "is" "blue" "+")
((((triple1 triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not blue.
False
4
inv-proof
[(((((triple1 triple2) -> rule1)) -> rule5))]
("Bob" "is" "blue" "-")
((((triple1 triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Bob is nice.[(triple3 OR ((triple4) -> rule7) OR ((((triple1 ((((triple1 triple2) -> rule1)) -> rule5)) -> rule2)) -> rule7) OR ((((((((((triple1 triple2) -> rule1)) -> rule5)) -> rule4) ((((triple1 triple2) -> rule1)) -> rule5)) -> rule3)) -> rule7))] Bob is young.[(triple4 OR ((triple1 ((((triple1 triple2) -> rule1)) -> rule5)) -> rule2) OR ((((((((triple1 triple2) -> rule1)) -> rule5)) -> rule4) ((((triple1 triple2) -> rule1)) -> rule5)) -> rule3))] Erin is blue.[(triple6)] Erin is green.[(triple7)] Erin is not big.[(triple5)] Erin is not white.[(triple9)] Erin is red.[(triple8 OR ((triple6) -> rule4))] Erin is young.[(triple10 OR ((triple8 triple6) -> rule3) OR ((((triple6) -> rule4) triple6) -> rule3))] @1: Bob is white.[(((triple1 triple2) -> rule1))] Erin is nice.[(((triple10) -> rule7) OR ((((triple8 triple6) -> rule3)) -> rule7) OR ((((((triple6) -> rule4) triple6) -> rule3)) -> rule7))] @2: Bob is blue.[(((((triple1 triple2) -> rule1)) -> rule5))] @3: Bob is red.[(((((((triple1 triple2) -> rule1)) -> rule5)) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple4) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1 ((((triple1 triple2) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((((((((triple1 triple2) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule4 % int3)) ((((triple1 triple2) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
Bob is young.
("Bob" "is" "young" "+")
triple4
((triple1 ((((triple1 triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((((((triple1 triple2) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) ((((triple1 triple2) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is green.
("Erin" "is" "green" "+")
triple7
Erin is not big.
("Erin" "is" "big" "-")
triple5
Erin is not white.
("Erin" "is" "white" "-")
triple9
Erin is red.
("Erin" "is" "red" "+")
triple8
((triple6) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple10
((triple8 triple6) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple6) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((triple1 triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple10) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple8 triple6) -> (rule3 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((((triple6) -> (rule4 % int3)) triple6) -> (rule3 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1 triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((((triple1 triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3