Bob is blue. Bob is nice. Bob is quiet. Bob is smart. Bob is young. Harry is blue. Harry is nice. Harry is quiet. Harry is red. Harry is round. Harry is smart. Harry is young. Red people are nice. Quiet, young people are round. If someone is smart and round then they are red. If someone is smart and red then they are blue. All blue people are young. If someone is round then they are blue.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "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 smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
Red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Quiet, young people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is smart and round then they are red.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is smart and red then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
All blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is round then they are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Harry is nice.
True
1
proof
[(triple7 OR ((triple9) -> rule1) OR ((((triple11 triple10) -> rule3)) -> rule1) OR ((((triple11 ((triple8 triple12) -> rule2)) -> rule3)) -> rule1) OR ((((triple11 ((triple8 ((triple6) -> rule5)) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "nice" "+")
triple7
((triple9) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple11 triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple11 ((triple8 triple12) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((((triple11 ((triple8 ((triple6) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is not smart.
False
1
inv-proof
[(triple11)]
("Harry" "is" "smart" "-")
triple11
Bob is round.
True
3
proof
[(((triple3 triple5) -> rule2) OR ((triple3 ((triple1) -> rule5)) -> rule2))]
("Bob" "is" "round" "+")
((triple3 triple5) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple3 ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not round.
False
3
inv-proof
[(((triple3 triple5) -> rule2) OR ((triple3 ((triple1) -> rule5)) -> rule2))]
("Bob" "is" "round" "-")
((triple3 triple5) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple3 ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
True
5
proof
[(((triple4 ((triple3 triple5) -> rule2)) -> rule3) OR ((triple4 ((triple3 ((triple1) -> rule5)) -> rule2)) -> rule3))]
("Bob" "is" "red" "+")
((triple4 ((triple3 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((triple4 ((triple3 ((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is not red.
False
5
inv-proof
[(((triple4 ((triple3 triple5) -> rule2)) -> rule3) OR ((triple4 ((triple3 ((triple1) -> rule5)) -> rule2)) -> rule3))]
("Bob" "is" "red" "-")
((triple4 ((triple3 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((triple4 ((triple3 ((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
@0: Bob is blue.[(triple1 OR ((((triple3 triple5) -> rule2)) -> rule6) OR ((triple4 ((triple4 ((triple3 triple5) -> rule2)) -> rule3)) -> rule4))] Bob is nice.[(triple2 OR ((((triple4 ((triple3 triple5) -> rule2)) -> rule3)) -> rule1) OR ((((triple4 ((triple3 ((triple1) -> rule5)) -> rule2)) -> rule3)) -> rule1))] Bob is quiet.[(triple3)] Bob is smart.[(triple4)] Bob is young.[(triple5 OR ((triple1) -> rule5))] Harry is blue.[(triple6 OR ((triple10) -> rule6) OR ((triple11 triple9) -> rule4) OR ((((triple8 triple12) -> rule2)) -> rule6) OR ((triple11 ((triple11 triple10) -> rule3)) -> rule4) OR ((triple11 ((triple11 ((triple8 triple12) -> rule2)) -> rule3)) -> rule4))] Harry is nice.[(triple7 OR ((triple9) -> rule1) OR ((((triple11 triple10) -> rule3)) -> rule1) OR ((((triple11 ((triple8 triple12) -> rule2)) -> rule3)) -> rule1) OR ((((triple11 ((triple8 ((triple6) -> rule5)) -> rule2)) -> rule3)) -> rule1))] Harry is quiet.[(triple8)] Harry is red.[(triple9 OR ((triple11 triple10) -> rule3) OR ((triple11 ((triple8 triple12) -> rule2)) -> rule3) OR ((triple11 ((triple8 ((triple6) -> rule5)) -> rule2)) -> rule3))] Harry is round.[(triple10 OR ((triple8 triple12) -> rule2) OR ((triple8 ((triple6) -> rule5)) -> rule2) OR ((triple8 ((((triple11 triple9) -> rule4)) -> rule5)) -> rule2))] Harry is smart.[(triple11)] Harry is young.[(triple12 OR ((triple6) -> rule5) OR ((((triple10) -> rule6)) -> rule5) OR ((((triple11 triple9) -> rule4)) -> rule5) OR ((((triple11 ((triple11 triple10) -> rule3)) -> rule4)) -> rule5))] @1: Bob is round.[(((triple3 triple5) -> rule2) OR ((triple3 ((triple1) -> rule5)) -> rule2))] @2: Bob is red.[(((triple4 ((triple3 triple5) -> rule2)) -> rule3) OR ((triple4 ((triple3 ((triple1) -> rule5)) -> rule2)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((((triple3 triple5) -> (rule2 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((triple4 ((triple4 ((triple3 triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
triple2
((((triple4 ((triple3 triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((triple4 ((triple3 ((triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
((triple1) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple6
((triple10) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple11 triple9) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple8 triple12) -> (rule2 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple11 ((triple11 triple10) -> (rule3 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((triple11 ((triple11 ((triple8 triple12) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple7
((triple9) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple11 triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple11 ((triple8 triple12) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((((triple11 ((triple8 ((triple6) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is red.
("Harry" "is" "red" "+")
triple9
((triple11 triple10) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple11 ((triple8 triple12) -> (rule2 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple11 ((triple8 ((triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
triple10
((triple8 triple12) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple8 ((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((triple8 ((((triple11 triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple6) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple11 triple9) -> (rule4 % int2))) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple11 ((triple11 triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
((triple3 triple5) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple3 ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple4 ((triple3 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((triple4 ((triple3 ((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3