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