Anne is big. Anne is kind. Anne is nice. Anne is red. Bob is big. Bob is blue. Bob is kind. Bob is nice. Bob is red. Dave is blue. Dave is kind. Dave is red. All nice things are big. If Bob is kind then Bob is nice. Blue things are nice. White things are blue. If something is kind then it is quiet. All white things are nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If Bob is kind then Bob is nice.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "nice" "+"))
Blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
White things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If something is kind then it is quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
All white things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Dave is blue.
True
1
proof
[(triple10)]
("Dave" "is" "blue" "+")
triple10
Anne is not big.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule1))]
("Anne" "is" "big" "-")
triple1
((triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "blue" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is big.[(triple1 OR ((triple3) -> rule1))] Anne is kind.[(triple2)] Anne is nice.[(triple3)] Anne is red.[(triple4)] Bob is big.[(triple5 OR ((triple8) -> rule1) OR ((((triple6) -> rule3)) -> rule1) OR ((((triple7) -> rule2)) -> rule1))] Bob is blue.[(triple6)] Bob is kind.[(triple7)] Bob is nice.[(triple8 OR ((triple6) -> rule3) OR ((triple7) -> rule2))] Bob is red.[(triple9)] Dave is blue.[(triple10)] Dave is kind.[(triple11)] Dave is red.[(triple12)] @1: Anne is quiet.[(((triple2) -> rule5))] Bob is quiet.[(((triple7) -> rule5))] Dave is nice.[(((triple10) -> rule3))] Dave is quiet.[(((triple11) -> rule5))] @2: Dave is big.[(((((triple10) -> rule3)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
triple5
((triple8) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
triple6
Bob is kind.
("Bob" "is" "kind" "+")
triple7
Bob is nice.
("Bob" "is" "nice" "+")
triple8
((triple6) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple7) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple9
Dave is blue.
("Dave" "is" "blue" "+")
triple10
Dave is kind.
("Dave" "is" "kind" "+")
triple11
Dave is red.
("Dave" "is" "red" "+")
triple12
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple7) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple10) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple11) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2