Bob is blue. Bob is green. Bob is nice. Bob is quiet. Bob is red. Bob is rough. Bob is young. If Bob is nice then Bob is rough. Rough, young things are red. All green things are red. Rough things are nice. If something is rough and red then it is quiet. All young, rough things are green.
Bob is blue.
("Bob" "is" "blue" "+")
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 young.
("Bob" "is" "young" "+")
If Bob is nice then Bob is rough.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "rough" "+"))
Rough, young things are red.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is rough and red then it is quiet.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
All young, rough things are green.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Bob is young.
True
1
proof
[(triple7)]
("Bob" "is" "young" "+")
triple7
Bob is not rough.
False
1
inv-proof
[(triple6 OR ((triple3) -> rule1))]
("Bob" "is" "rough" "-")
triple6
((triple3) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
@0: Bob is blue.[(triple1)] Bob is green.[(triple2 OR ((triple7 triple6) -> rule6) OR ((triple7 ((triple3) -> rule1)) -> rule6))] Bob is nice.[(triple3 OR ((triple6) -> rule4))] Bob is quiet.[(triple4 OR ((triple6 triple5) -> rule5) OR ((triple6 ((triple2) -> rule3)) -> rule5) OR ((triple6 ((triple6 triple7) -> rule2)) -> rule5) OR ((((triple3) -> rule1) triple5) -> rule5) OR ((((triple3) -> rule1) ((triple2) -> rule3)) -> rule5) OR ((((triple3) -> rule1) ((triple6 triple7) -> rule2)) -> rule5) OR ((triple6 ((((triple7 triple6) -> rule6)) -> rule3)) -> rule5) OR ((triple6 ((((triple3) -> rule1) triple7) -> rule2)) -> rule5) OR ((((triple3) -> rule1) ((((triple7 triple6) -> rule6)) -> rule3)) -> rule5) OR ((((triple3) -> rule1) ((((triple3) -> rule1) triple7) -> rule2)) -> rule5) OR ((triple6 ((((triple7 ((triple3) -> rule1)) -> rule6)) -> rule3)) -> rule5) OR ((((triple3) -> rule1) ((((triple7 ((triple3) -> rule1)) -> rule6)) -> rule3)) -> rule5))] Bob is red.[(triple5 OR ((triple2) -> rule3) OR ((triple6 triple7) -> rule2) OR ((((triple7 triple6) -> rule6)) -> rule3) OR ((((triple3) -> rule1) triple7) -> rule2) OR ((((triple7 ((triple3) -> rule1)) -> rule6)) -> rule3))] Bob is rough.[(triple6 OR ((triple3) -> rule1))] Bob is young.[(triple7)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple7 triple6) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple7 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple6) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple6 triple5) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple6 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((triple6 ((triple6 triple7) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple3) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple3) -> (rule1 % int3)) ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((triple3) -> (rule1 % int3)) ((triple6 triple7) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((triple6 ((((triple7 triple6) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((triple6 ((((triple3) -> (rule1 % int3)) triple7) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((triple3) -> (rule1 % int4)) ((((triple7 triple6) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3)) triple7) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((triple6 ((((triple7 ((triple3) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
((((triple3) -> (rule1 % int4)) ((((triple7 ((triple3) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple2) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple6 triple7) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple7 triple6) -> (rule6 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple3) -> (rule1 % int2)) triple7) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple7 ((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
triple6
((triple3) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple7