Bob is green. Bob is quiet. Bob is red. Bob is smart. Dave is cold. Dave is nice. Dave is quiet. Dave is red. Dave is smart. Dave is young. If something is smart then it is quiet. Young things are green.
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is smart then it is quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Dave is cold.
True
1
proof
[(triple5)]
("Dave" "is" "cold" "+")
triple5
Dave is not cold.
False
1
inv-proof
[(triple5)]
("Dave" "is" "cold" "-")
triple5
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is green.[(triple1)] Bob is quiet.[(triple2 OR ((triple4) -> rule1))] Bob is red.[(triple3)] Bob is smart.[(triple4)] Dave is cold.[(triple5)] Dave is nice.[(triple6)] Dave is quiet.[(triple7 OR ((triple9) -> rule1))] Dave is red.[(triple8)] Dave is smart.[(triple9)] Dave is young.[(triple10)] @1: Dave is green.[(((triple10) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
((triple4) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
((triple9) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple8
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Dave is green.
("Dave" "is" "green" "+")
((triple10) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1