Bob is big. Bob is not kind. Bob is smart. Bob is not white. Bob is not young. Dave is big. Dave is furry. Dave is kind. Dave is nice. Dave is smart. Dave is white. Dave is young. If something is white then it is furry. Furry, young things are kind. All young, kind things are white. If something is big and not white then it is smart. Furry things are nice. If something is kind and not smart then it is not nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is not white.
("Bob" "is" "white" "-")
Bob is not young.
("Bob" "is" "young" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is white then it is furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Furry, young things are kind.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All young, kind things are white.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is big and not white then it is smart.
((("something" "is" "big" "+") ("something" "is" "white" "~")) -> ("something" "is" "smart" "+"))
Furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is kind and not smart then it is not nice.
((("something" "is" "kind" "+") ("something" "is" "smart" "~")) -> ("something" "is" "nice" "-"))
Dave is nice.
True
1
proof
[(triple9 OR ((triple7) -> rule5) OR ((((triple11) -> rule1)) -> rule5) OR ((((((triple12 triple8) -> rule3)) -> rule1)) -> rule5))]
("Dave" "is" "nice" "+")
triple9
((triple7) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple12 triple8) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not nice.
False
1
inv-proof
[(triple9 OR ((triple7) -> rule5) OR ((((triple11) -> rule1)) -> rule5) OR ((((((triple12 triple8) -> rule3)) -> rule1)) -> rule5))]
("Dave" "is" "nice" "-")
triple9
((triple7) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple12 triple8) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
@0: Bob is big.[(triple1)] Bob is not kind.[(triple2)] Bob is not white.[(triple4)] Bob is not young.[(triple5)] Bob is smart.[(triple3 OR ((triple1 triple4) -> rule4))] Dave is big.[(triple6)] Dave is furry.[(triple7 OR ((triple11) -> rule1) OR ((((triple12 triple8) -> rule3)) -> rule1))] Dave is kind.[(triple8 OR ((triple7 triple12) -> rule2) OR ((((triple11) -> rule1) triple12) -> rule2))] Dave is nice.[(triple9 OR ((triple7) -> rule5) OR ((((triple11) -> rule1)) -> rule5) OR ((((((triple12 triple8) -> rule3)) -> rule1)) -> rule5))] Dave is smart.[(triple10)] Dave is white.[(triple11 OR ((triple12 triple8) -> rule3) OR ((triple12 ((triple7 triple12) -> rule2)) -> rule3))] Dave is young.[(triple12)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is not kind.
("Bob" "is" "kind" "-")
triple2
Bob is not white.
("Bob" "is" "white" "-")
triple4
Bob is not young.
("Bob" "is" "young" "-")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple3
((triple1 triple4) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is furry.
("Dave" "is" "furry" "+")
triple7
((triple11) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple12 triple8) -> (rule3 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple8
((triple7 triple12) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple11) -> (rule1 % int2)) triple12) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple9
((triple7) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple12 triple8) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
((triple12 triple8) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple12 ((triple7 triple12) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple12