Bob is blue. Bob is nice. Bob is red. Erin is blue. Erin is nice. Erin is red. Erin is round. Erin is white. Erin is young. Harry is blue. Harry is nice. Harry is quiet. Harry is red. Harry is round. Harry is white. Harry is young. If someone is red then they are young. If someone is blue and red then they are nice. If Erin is blue and Erin is young then Erin is quiet. All young people are white. All white people are round. If Erin is nice then Erin is round. All blue people are young. All red people are quiet.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is red then they are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is blue and red then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If Erin is blue and Erin is young then Erin is quiet.
((("Erin" "is" "blue" "+") ("Erin" "is" "young" "+")) -> ("Erin" "is" "quiet" "+"))
All young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
All white people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If Erin is nice then Erin is round.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "round" "+"))
All blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
All red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Harry is nice.
True
1
proof
[(triple11 OR ((triple10 triple13) -> rule2))]
("Harry" "is" "nice" "+")
triple11
((triple10 triple13) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not white.
False
1
inv-proof
[(triple15 OR ((triple16) -> rule4) OR ((((triple10) -> rule7)) -> rule4) OR ((((triple13) -> rule1)) -> rule4))]
("Harry" "is" "white" "-")
triple15
((triple16) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple10) -> (rule7 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple13) -> (rule1 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Bob is young.
True
2
proof
[(((triple1) -> rule7) OR ((triple3) -> rule1))]
("Bob" "is" "young" "+")
((triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple3) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple1) -> rule7) OR ((triple3) -> rule1))]
("Bob" "is" "young" "-")
((triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple3) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is white.
True
3
proof
[(((((triple1) -> rule7)) -> rule4) OR ((((triple3) -> rule1)) -> rule4))]
("Bob" "is" "white" "+")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule4) OR ((((triple3) -> rule1)) -> rule4))]
("Bob" "is" "white" "-")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is round.
True
4
proof
[(((((((triple1) -> rule7)) -> rule4)) -> rule5) OR ((((((triple3) -> rule1)) -> rule4)) -> rule5))]
("Bob" "is" "round" "+")
((((((triple1) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is not round.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule4)) -> rule5) OR ((((((triple3) -> rule1)) -> rule4)) -> rule5))]
("Bob" "is" "round" "-")
((((((triple1) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
@0: Bob is blue.[(triple1)] Bob is nice.[(triple2 OR ((triple1 triple3) -> rule2))] Bob is red.[(triple3)] Erin is blue.[(triple4)] Erin is nice.[(triple5 OR ((triple4 triple6) -> rule2))] Erin is red.[(triple6)] Erin is round.[(triple7 OR ((triple5) -> rule6) OR ((triple8) -> rule5) OR ((((triple9) -> rule4)) -> rule5) OR ((((triple4 triple6) -> rule2)) -> rule6) OR ((((((triple4) -> rule7)) -> rule4)) -> rule5) OR ((((((triple6) -> rule1)) -> rule4)) -> rule5))] Erin is white.[(triple8 OR ((triple9) -> rule4) OR ((((triple4) -> rule7)) -> rule4) OR ((((triple6) -> rule1)) -> rule4))] Erin is young.[(triple9 OR ((triple4) -> rule7) OR ((triple6) -> rule1))] Harry is blue.[(triple10)] Harry is nice.[(triple11 OR ((triple10 triple13) -> rule2))] Harry is quiet.[(triple12 OR ((triple13) -> rule8))] Harry is red.[(triple13)] Harry is round.[(triple14 OR ((triple15) -> rule5) OR ((((triple16) -> rule4)) -> rule5) OR ((((((triple10) -> rule7)) -> rule4)) -> rule5) OR ((((((triple13) -> rule1)) -> rule4)) -> rule5))] Harry is white.[(triple15 OR ((triple16) -> rule4) OR ((((triple10) -> rule7)) -> rule4) OR ((((triple13) -> rule1)) -> rule4))] Harry is young.[(triple16 OR ((triple10) -> rule7) OR ((triple13) -> rule1))] @1: Bob is quiet.[(((triple3) -> rule8))] Bob is young.[(((triple1) -> rule7) OR ((triple3) -> rule1))] Erin is quiet.[(((triple6) -> rule8) OR ((triple4 triple9) -> rule3) OR ((triple4 ((triple4) -> rule7)) -> rule3) OR ((triple4 ((triple6) -> rule1)) -> rule3))] @2: Bob is white.[(((((triple1) -> rule7)) -> rule4) OR ((((triple3) -> rule1)) -> rule4))] @3: Bob is round.[(((((((triple1) -> rule7)) -> rule4)) -> rule5) OR ((((((triple3) -> rule1)) -> rule4)) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
((triple1 triple3) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Erin is nice.
("Erin" "is" "nice" "+")
triple5
((triple4 triple6) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
((triple5) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple8) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple4 triple6) -> (rule2 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((((triple6) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
triple8
((triple9) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple4) -> (rule7 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple9
((triple4) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple6) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple11
((triple10 triple13) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
((triple13) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
((triple15) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple16) -> (rule4 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((((triple10) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((triple13) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
triple15
((triple16) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple10) -> (rule7 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple13) -> (rule1 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple10) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple13) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple3) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple6) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple4 triple9) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple4 ((triple4) -> (rule7 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((triple4 ((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((((triple1) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3