Bob is big. Bob is kind. Bob is quiet. Bob is red. Bob is rough. Dave is big. Dave is blue. Dave is kind. Dave is red. Dave is rough. All kind, rough people are blue. If Bob is quiet then Bob is rough. If someone is blue then they are quiet. All big people are smart. If someone is blue and rough then they are kind. All kind, red people are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
All kind, rough people are blue.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If Bob is quiet then Bob is rough.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "rough" "+"))
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
All big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If someone is blue and rough then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
All kind, red people are big.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Bob is big.
True
1
proof
[(triple1 OR ((triple2 triple4) -> rule6))]
("Bob" "is" "big" "+")
triple1
((triple2 triple4) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not rough.
False
1
inv-proof
[(triple5 OR ((triple3) -> rule2))]
("Bob" "is" "rough" "-")
triple5
((triple3) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
@0: Bob is big.[(triple1 OR ((triple2 triple4) -> rule6))] Bob is kind.[(triple2)] Bob is quiet.[(triple3 OR ((((triple2 triple5) -> rule1)) -> rule3))] Bob is red.[(triple4)] Bob is rough.[(triple5 OR ((triple3) -> rule2))] Dave is big.[(triple6 OR ((triple8 triple9) -> rule6) OR ((((triple7 triple10) -> rule5) triple9) -> rule6))] Dave is blue.[(triple7 OR ((triple8 triple10) -> rule1))] Dave is kind.[(triple8 OR ((triple7 triple10) -> rule5))] Dave is red.[(triple9)] Dave is rough.[(triple10)] @1: Bob is blue.[(((triple2 triple5) -> rule1) OR ((triple2 ((triple3) -> rule2)) -> rule1))] Bob is smart.[(((triple1) -> rule4) OR ((((triple2 triple4) -> rule6)) -> rule4))] Dave is quiet.[(((triple7) -> rule3) OR ((((triple8 triple10) -> rule1)) -> rule3))] Dave is smart.[(((triple6) -> rule4) OR ((((triple8 triple9) -> rule6)) -> rule4) OR ((((((triple7 triple10) -> rule5) triple9) -> rule6)) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2 triple4) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((((triple2 triple5) -> (rule1 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple3) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple6
((triple8 triple9) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple7 triple10) -> (rule5 % int2)) triple9) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple7
((triple8 triple10) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple8
((triple7 triple10) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple9
Dave is rough.
("Dave" "is" "rough" "+")
triple10
Bob is blue.
("Bob" "is" "blue" "+")
((triple2 triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple2 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple2 triple4) -> (rule6 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple7) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple8 triple10) -> (rule1 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple6) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple8 triple9) -> (rule6 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((((triple7 triple10) -> (rule5 % int3)) triple9) -> (rule6 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3