Bob is big. Bob is blue. Bob is kind. Bob is nice. Bob is rough. Bob is round. Bob is young. Harry is blue. Harry is not kind. Harry is rough. Harry is round. Harry is young. If something is round and not young then it is nice. If something is nice and not round then it is not kind. If Bob is nice and Bob is not kind then Bob is not blue. If something is blue and not kind then it is rough. All young, nice things are rough. Round, blue things are big. Young things are big. If something is blue then it is 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 rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is round and not young then it is nice.
((("something" "is" "round" "+") ("something" "is" "young" "~")) -> ("something" "is" "nice" "+"))
If something is nice and not round then it is not kind.
((("something" "is" "nice" "+") ("something" "is" "round" "~")) -> ("something" "is" "kind" "-"))
If Bob is nice and Bob is not kind then Bob is not blue.
((("Bob" "is" "nice" "+") ("Bob" "is" "kind" "~")) -> ("Bob" "is" "blue" "-"))
If something is blue and not kind then it is rough.
((("something" "is" "blue" "+") ("something" "is" "kind" "~")) -> ("something" "is" "rough" "+"))
All young, nice things are rough.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Round, blue things are big.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Harry is young.
True
1
proof
[(triple12)]
("Harry" "is" "young" "+")
triple12
Bob is not rough.
False
1
inv-proof
[(triple5 OR ((triple7 triple4) -> rule5))]
("Bob" "is" "rough" "-")
triple5
((triple7 triple4) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Harry is big.
True
2
proof
[(((triple12) -> rule7) OR ((triple8) -> rule8) OR ((triple11 triple8) -> rule6))]
("Harry" "is" "big" "+")
((triple12) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple8) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple11 triple8) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple12) -> rule7) OR ((triple8) -> rule8) OR ((triple11 triple8) -> rule6))]
("Harry" "is" "big" "-")
((triple12) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple8) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple11 triple8) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
@0: Bob is big.[(triple1 OR ((triple2) -> rule8) OR ((triple7) -> rule7) OR ((triple6 triple2) -> rule6))] Bob is blue.[(triple2)] Bob is kind.[(triple3)] Bob is nice.[(triple4)] Bob is rough.[(triple5 OR ((triple7 triple4) -> rule5))] Bob is round.[(triple6)] Bob is young.[(triple7)] Harry is blue.[(triple8)] Harry is not kind.[(triple9)] Harry is rough.[(triple10 OR ((triple8 triple9) -> rule4))] Harry is round.[(triple11)] Harry is young.[(triple12)] @1: Harry is big.[(((triple12) -> rule7) OR ((triple8) -> rule8) OR ((triple11 triple8) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple7) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple6 triple2) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple7 triple4) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is not kind.
("Harry" "is" "kind" "-")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
((triple8 triple9) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Harry is big.
("Harry" "is" "big" "+")
((triple12) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple8) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple11 triple8) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1