Bob is big. Bob is blue. Bob is kind. Bob is nice. Bob is quiet. Bob is rough. Bob is round. Fiona is big. Fiona is blue. Fiona is rough. Fiona is round. Harry is big. Harry is nice. Harry is quiet. Harry is rough. If someone is rough and round then they are nice. Rough, kind people are round. All blue people are kind. If Harry is big then Harry is blue. Round people are quiet. All blue people are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is rough and round then they are nice.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
Rough, kind people are round.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If Harry is big then Harry is blue.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "blue" "+"))
Round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
All blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Bob is quiet.
True
1
proof
[(triple5 OR ((triple7) -> rule5) OR ((((triple6 triple3) -> rule2)) -> rule5) OR ((((triple6 ((triple2) -> rule3)) -> rule2)) -> rule5))]
("Bob" "is" "quiet" "+")
triple5
((triple7) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple6 triple3) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple6 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not round.
False
1
inv-proof
[(triple7 OR ((triple6 triple3) -> rule2) OR ((triple6 ((triple2) -> rule3)) -> rule2))]
("Bob" "is" "round" "-")
triple7
((triple6 triple3) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple6 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Fiona is quiet.
True
2
proof
[(((triple11) -> rule5) OR ((((triple10 ((triple9) -> rule3)) -> rule2)) -> rule5))]
("Fiona" "is" "quiet" "+")
((triple11) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple10 ((triple9) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is not nice.
False
3
inv-proof
[(((triple10 triple11) -> rule1) OR ((triple10 ((triple10 ((triple9) -> rule3)) -> rule2)) -> rule1))]
("Fiona" "is" "nice" "-")
((triple10 triple11) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((triple10 ((triple10 ((triple9) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Harry is kind.
True
3
proof
[(((((triple12) -> rule4)) -> rule3))]
("Harry" "is" "kind" "+")
((((triple12) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not kind.
False
3
inv-proof
[(((((triple12) -> rule4)) -> rule3))]
("Harry" "is" "kind" "-")
((((triple12) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
True
5
proof
[(((triple15 ((((triple12) -> rule4)) -> rule3)) -> rule2))]
("Harry" "is" "round" "+")
((triple15 ((((triple12) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not round.
False
5
inv-proof
[(((triple15 ((((triple12) -> rule4)) -> rule3)) -> rule2))]
("Harry" "is" "round" "-")
((triple15 ((((triple12) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
@0: Bob is big.[(triple1 OR ((triple2) -> rule6))] Bob is blue.[(triple2)] Bob is kind.[(triple3 OR ((triple2) -> rule3))] Bob is nice.[(triple4 OR ((triple6 triple7) -> rule1) OR ((triple6 ((triple6 triple3) -> rule2)) -> rule1) OR ((triple6 ((triple6 ((triple2) -> rule3)) -> rule2)) -> rule1))] Bob is quiet.[(triple5 OR ((triple7) -> rule5) OR ((((triple6 triple3) -> rule2)) -> rule5) OR ((((triple6 ((triple2) -> rule3)) -> rule2)) -> rule5))] Bob is rough.[(triple6)] Bob is round.[(triple7 OR ((triple6 triple3) -> rule2) OR ((triple6 ((triple2) -> rule3)) -> rule2))] Fiona is big.[(triple8 OR ((triple9) -> rule6))] Fiona is blue.[(triple9)] Fiona is rough.[(triple10)] Fiona is round.[(triple11 OR ((triple10 ((triple9) -> rule3)) -> rule2))] Harry is big.[(triple12)] Harry is nice.[(triple13 OR ((triple15 ((triple15 ((((triple12) -> rule4)) -> rule3)) -> rule2)) -> rule1))] Harry is quiet.[(triple14 OR ((((triple15 ((((triple12) -> rule4)) -> rule3)) -> rule2)) -> rule5))] Harry is rough.[(triple15)] @1: Fiona is kind.[(((triple9) -> rule3))] Fiona is nice.[(((triple10 triple11) -> rule1) OR ((triple10 ((triple10 ((triple9) -> rule3)) -> rule2)) -> rule1))] Fiona is quiet.[(((triple11) -> rule5) OR ((((triple10 ((triple9) -> rule3)) -> rule2)) -> rule5))] Harry is blue.[(((triple12) -> rule4))] @2: Harry is kind.[(((((triple12) -> rule4)) -> rule3))] @3: Harry is round.[(((triple15 ((((triple12) -> rule4)) -> rule3)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((triple6 triple7) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple6 ((triple6 triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((triple6 ((triple6 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple7) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple6 triple3) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple6 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Bob is round.
("Bob" "is" "round" "+")
triple7
((triple6 triple3) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple6 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
triple8
((triple9) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Fiona is rough.
("Fiona" "is" "rough" "+")
triple10
Fiona is round.
("Fiona" "is" "round" "+")
triple11
((triple10 ((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
triple13
((triple15 ((triple15 ((((triple12) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
((((triple15 ((((triple12) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple9) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple10 triple11) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((triple10 ((triple10 ((triple9) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple11) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple10 ((triple9) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
((triple12) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple12) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple15 ((((triple12) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3