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