Bob is blue. Bob is green. Bob is kind. Bob is nice. Bob is quiet. Bob is round. Bob is smart. Dave is blue. Dave is green. Dave is kind. Dave is nice. Dave is quiet. Dave is round. Dave is smart. Smart, green things are blue.
Bob is blue.
("Bob" "is" "blue" "+")
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 smart.
("Bob" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Smart, green things are blue.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Dave is kind.
True
1
proof
[(triple10)]
("Dave" "is" "kind" "+")
triple10
Dave is not round.
False
1
inv-proof
[(triple13)]
("Dave" "is" "round" "-")
triple13
@0: Bob is blue.[(triple1 OR ((triple7 triple2) -> rule1))] Bob is green.[(triple2)] Bob is kind.[(triple3)] Bob is nice.[(triple4)] Bob is quiet.[(triple5)] Bob is round.[(triple6)] Bob is smart.[(triple7)] Dave is blue.[(triple8 OR ((triple14 triple9) -> rule1))] Dave is green.[(triple9)] Dave is kind.[(triple10)] Dave is nice.[(triple11)] Dave is quiet.[(triple12)] Dave is round.[(triple13)] Dave is smart.[(triple14)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple7 triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
((triple14 triple9) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
triple11
Dave is quiet.
("Dave" "is" "quiet" "+")
triple12
Dave is round.
("Dave" "is" "round" "+")
triple13
Dave is smart.
("Dave" "is" "smart" "+")
triple14