Bob is blue. Bob is nice. Bob is red. Bob is rough. Bob is round. Bob is smart. Bob is young. Dave is blue. Dave is nice. Dave is red. Dave is rough. Dave is round. Dave is smart. Dave is young. If something is smart and red then it is young. If Bob is smart then Bob is rough. All red things are rough. If something is red and smart then it is blue. If Dave is rough and Dave is red then Dave is nice. Blue things are round.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is smart and red then it is young.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If Bob is smart then Bob is rough.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "rough" "+"))
All red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is red and smart then it is blue.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If Dave is rough and Dave is red then Dave is nice.
((("Dave" "is" "rough" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "nice" "+"))
Blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Dave is nice.
True
1
proof
[(triple9 OR ((triple11 triple10) -> rule5) OR ((((triple10) -> rule3) triple10) -> rule5))]
("Dave" "is" "nice" "+")
triple9
((triple11 triple10) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple10) -> (rule3 % int2)) triple10) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not round.
False
1
inv-proof
[(triple12 OR ((triple8) -> rule6) OR ((((triple10 triple13) -> rule4)) -> rule6))]
("Dave" "is" "round" "-")
triple12
((triple8) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple10 triple13) -> (rule4 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
@0: Bob is blue.[(triple1 OR ((triple3 triple6) -> rule4))] Bob is nice.[(triple2)] Bob is red.[(triple3)] Bob is rough.[(triple4 OR ((triple3) -> rule3) OR ((triple6) -> rule2))] Bob is round.[(triple5 OR ((triple1) -> rule6) OR ((((triple3 triple6) -> rule4)) -> rule6))] Bob is smart.[(triple6)] Bob is young.[(triple7 OR ((triple6 triple3) -> rule1))] Dave is blue.[(triple8 OR ((triple10 triple13) -> rule4))] Dave is nice.[(triple9 OR ((triple11 triple10) -> rule5) OR ((((triple10) -> rule3) triple10) -> rule5))] Dave is red.[(triple10)] Dave is rough.[(triple11 OR ((triple10) -> rule3))] Dave is round.[(triple12 OR ((triple8) -> rule6) OR ((((triple10 triple13) -> rule4)) -> rule6))] Dave is smart.[(triple13)] Dave is young.[(triple14 OR ((triple13 triple10) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple3 triple6) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
((triple3) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple6) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple5
((triple1) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple3 triple6) -> (rule4 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple6 triple3) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple8
((triple10 triple13) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple9
((triple11 triple10) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple10) -> (rule3 % int2)) triple10) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple10
Dave is rough.
("Dave" "is" "rough" "+")
triple11
((triple10) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple12
((triple8) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple10 triple13) -> (rule4 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple13
Dave is young.
("Dave" "is" "young" "+")
triple14
((triple13 triple10) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1