Bob is green. Bob is nice. Bob is quiet. Bob is red. Bob is rough. Bob is round. Bob is young. Harry is green. Harry is nice. Harry is quiet. Harry is red. Harry is round. If someone is red then they are nice. If someone is green and round then they are rough. All nice, red people are young. All red people are quiet. Red, rough people are quiet. All round people are quiet.
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone is green and round then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All nice, red people are young.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
All red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Red, rough people are quiet.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
All round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Harry is red.
True
1
proof
[(triple11)]
("Harry" "is" "red" "+")
triple11
Harry is not round.
False
1
inv-proof
[(triple12)]
("Harry" "is" "round" "-")
triple12
Harry is young.
True
3
proof
[(((triple9 triple11) -> rule3) OR ((((triple11) -> rule1) triple11) -> rule3))]
("Harry" "is" "young" "+")
((triple9 triple11) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple11) -> (rule1 % int2)) triple11) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not rough.
False
3
inv-proof
[(((triple8 triple12) -> rule2))]
("Harry" "is" "rough" "-")
((triple8 triple12) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
@0: Bob is green.[(triple1)] Bob is nice.[(triple2 OR ((triple4) -> rule1))] Bob is quiet.[(triple3 OR ((triple4) -> rule4) OR ((triple6) -> rule6) OR ((triple4 triple5) -> rule5) OR ((triple4 ((triple1 triple6) -> rule2)) -> rule5))] Bob is red.[(triple4)] Bob is rough.[(triple5 OR ((triple1 triple6) -> rule2))] Bob is round.[(triple6)] Bob is young.[(triple7 OR ((triple2 triple4) -> rule3) OR ((((triple4) -> rule1) triple4) -> rule3))] Harry is green.[(triple8)] Harry is nice.[(triple9 OR ((triple11) -> rule1))] Harry is quiet.[(triple10 OR ((triple11) -> rule4) OR ((triple12) -> rule6) OR ((triple11 ((triple8 triple12) -> rule2)) -> rule5))] Harry is red.[(triple11)] Harry is round.[(triple12)] @1: Harry is rough.[(((triple8 triple12) -> rule2))] Harry is young.[(((triple9 triple11) -> rule3) OR ((((triple11) -> rule1) triple11) -> rule3))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
((triple4) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple4) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple6) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple4 triple5) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple4 ((triple1 triple6) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple1 triple6) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple2 triple4) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple4) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
((triple11) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
((triple11) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple12) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple11 ((triple8 triple12) -> (rule2 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
((triple8 triple12) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple9 triple11) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple11) -> (rule1 % int2)) triple11) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2