Bob is big. Bob is blue. Bob is not red. Bob is smart. Bob is young. Fiona is furry. Fiona is nice. Fiona is red. Fiona is young. Harry is big. Harry is blue. Harry is furry. Harry is nice. Harry is red. Harry is smart. Harry is young. If someone is red and not young then they are big. If someone is young and smart then they are big. If Bob is nice and Bob is not young then Bob is blue. All big, young people are blue. Young people are smart. If someone is blue and not red then they are nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is red and not young then they are big.
((("someone" "is" "red" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "big" "+"))
If someone is young and smart then they are big.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If Bob is nice and Bob is not young then Bob is blue.
((("Bob" "is" "nice" "+") ("Bob" "is" "young" "~")) -> ("Bob" "is" "blue" "+"))
All big, young people are blue.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
If someone is blue and not red then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "nice" "+"))
Harry is nice.
True
1
proof
[(triple13)]
("Harry" "is" "nice" "+")
triple13
Harry is not big.
False
1
inv-proof
[(triple10 OR ((triple16 triple15) -> rule2) OR ((triple16 ((triple16) -> rule5)) -> rule2))]
("Harry" "is" "big" "-")
triple10
((triple16 triple15) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple16 ((triple16) -> (rule5 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Fiona is smart.
True
2
proof
[(((triple9) -> rule5))]
("Fiona" "is" "smart" "+")
((triple9) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple9) -> rule5))]
("Fiona" "is" "smart" "-")
((triple9) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
True
4
proof
[(((triple9 ((triple9) -> rule5)) -> rule2))]
("Fiona" "is" "big" "+")
((triple9 ((triple9) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not big.
False
4
inv-proof
[(((triple9 ((triple9) -> rule5)) -> rule2))]
("Fiona" "is" "big" "-")
((triple9 ((triple9) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
@0: Bob is big.[(triple1 OR ((triple5 triple4) -> rule2) OR ((triple5 ((triple5) -> rule5)) -> rule2))] Bob is blue.[(triple2 OR ((triple1 triple5) -> rule4) OR ((((triple5 triple4) -> rule2) triple5) -> rule4) OR ((((triple5 ((triple5) -> rule5)) -> rule2) triple5) -> rule4))] Bob is not red.[(triple3)] Bob is smart.[(triple4 OR ((triple5) -> rule5))] Bob is young.[(triple5)] Fiona is furry.[(triple6)] Fiona is nice.[(triple7)] Fiona is red.[(triple8)] Fiona is young.[(triple9)] Harry is big.[(triple10 OR ((triple16 triple15) -> rule2) OR ((triple16 ((triple16) -> rule5)) -> rule2))] Harry is blue.[(triple11 OR ((triple10 triple16) -> rule4) OR ((((triple16 triple15) -> rule2) triple16) -> rule4) OR ((((triple16 ((triple16) -> rule5)) -> rule2) triple16) -> rule4))] Harry is furry.[(triple12)] Harry is nice.[(triple13)] Harry is red.[(triple14)] Harry is smart.[(triple15 OR ((triple16) -> rule5))] Harry is young.[(triple16)] @1: Bob is nice.[(((triple2 triple3) -> rule6) OR ((((triple1 triple5) -> rule4) triple3) -> rule6) OR ((((((triple5 triple4) -> rule2) triple5) -> rule4) triple3) -> rule6) OR ((((((triple5 ((triple5) -> rule5)) -> rule2) triple5) -> rule4) triple3) -> rule6))] Fiona is smart.[(((triple9) -> rule5))] @2: Fiona is big.[(((triple9 ((triple9) -> rule5)) -> rule2))] @3: Fiona is blue.[(((((triple9 ((triple9) -> rule5)) -> rule2) triple9) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple5 triple4) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple5 ((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple1 triple5) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple5 triple4) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple5 ((triple5) -> (rule5 % int3))) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not red.
("Bob" "is" "red" "-")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
((triple5) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple5
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
triple8
Fiona is young.
("Fiona" "is" "young" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
((triple16 triple15) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple16 ((triple16) -> (rule5 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
triple11
((triple10 triple16) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple16 triple15) -> (rule2 % int2)) triple16) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple16 ((triple16) -> (rule5 % int3))) -> (rule2 % int2)) triple16) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
triple13
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
((triple16) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple16
Bob is nice.
("Bob" "is" "nice" "+")
((triple2 triple3) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1 triple5) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple5 triple4) -> (rule2 % int3)) triple5) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple5 ((triple5) -> (rule5 % int4))) -> (rule2 % int3)) triple5) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple9) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple9 ((triple9) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple9 ((triple9) -> (rule5 % int3))) -> (rule2 % int2)) triple9) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3