Anne is green. Anne is quiet. Anne is red. Anne is rough. Dave is blue. Dave is green. Dave is red. Dave is rough. Dave is round. Dave is white. Fiona is green. Harry is blue. Harry is red. Harry is rough. Harry is round. If Dave is rough and Dave is quiet then Dave is white. Blue, rough things are quiet. All green, quiet things are white. If something is red then it is rough. All green, white things are quiet. All red things are quiet.
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
If Dave is rough and Dave is quiet then Dave is white.
((("Dave" "is" "rough" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "white" "+"))
Blue, rough things are quiet.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All green, quiet things are white.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
All green, white things are quiet.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
All red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Harry is blue.
True
1
proof
[(triple12)]
("Harry" "is" "blue" "+")
triple12
Harry is not rough.
False
1
inv-proof
[(triple14 OR ((triple13) -> rule4))]
("Harry" "is" "rough" "-")
triple14
((triple13) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Dave is quiet.
True
2
proof
[(((triple7) -> rule6) OR ((triple5 triple8) -> rule2) OR ((triple6 triple10) -> rule5) OR ((triple5 ((triple7) -> rule4)) -> rule2))]
("Dave" "is" "quiet" "+")
((triple7) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple5 triple8) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple6 triple10) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple5 ((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not quiet.
False
2
inv-proof
[(((triple7) -> rule6) OR ((triple5 triple8) -> rule2) OR ((triple6 triple10) -> rule5) OR ((triple5 ((triple7) -> rule4)) -> rule2))]
("Dave" "is" "quiet" "-")
((triple7) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple5 triple8) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple6 triple10) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple5 ((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "white" "-")
Fiona is quiet.
Unknown
rconc
[@3: Fiona is quiet.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule2 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is green.[(triple1)] Anne is quiet.[(triple2 OR ((triple3) -> rule6))] Anne is red.[(triple3)] Anne is rough.[(triple4 OR ((triple3) -> rule4))] Dave is blue.[(triple5)] Dave is green.[(triple6)] Dave is red.[(triple7)] Dave is rough.[(triple8 OR ((triple7) -> rule4))] Dave is round.[(triple9)] Dave is white.[(triple10 OR ((triple6 ((triple7) -> rule6)) -> rule3) OR ((triple6 ((triple5 triple8) -> rule2)) -> rule3) OR ((triple8 ((triple7) -> rule6)) -> rule1) OR ((triple8 ((triple5 triple8) -> rule2)) -> rule1) OR ((((triple7) -> rule4) ((triple7) -> rule6)) -> rule1) OR ((((triple7) -> rule4) ((triple5 triple8) -> rule2)) -> rule1) OR ((triple6 ((triple5 ((triple7) -> rule4)) -> rule2)) -> rule3) OR ((triple8 ((triple5 ((triple7) -> rule4)) -> rule2)) -> rule1) OR ((((triple7) -> rule4) ((triple5 ((triple7) -> rule4)) -> rule2)) -> rule1))] Fiona is green.[(triple11)] Harry is blue.[(triple12)] Harry is red.[(triple13)] Harry is rough.[(triple14 OR ((triple13) -> rule4))] Harry is round.[(triple15)] @1: Anne is white.[(((triple1 triple2) -> rule3) OR ((triple1 ((triple3) -> rule6)) -> rule3))] Dave is quiet.[(((triple7) -> rule6) OR ((triple5 triple8) -> rule2) OR ((triple6 triple10) -> rule5) OR ((triple5 ((triple7) -> rule4)) -> rule2))] Harry is quiet.[(((triple13) -> rule6) OR ((triple12 triple14) -> rule2) OR ((triple12 ((triple13) -> rule4)) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((triple3) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple3) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple7
Dave is rough.
("Dave" "is" "rough" "+")
triple8
((triple7) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple9
Dave is white.
("Dave" "is" "white" "+")
triple10
((triple6 ((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((triple6 ((triple5 triple8) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((triple8 ((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((triple8 ((triple5 triple8) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple7) -> (rule4 % int3)) ((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple7) -> (rule4 % int3)) ((triple5 triple8) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((triple6 ((triple5 ((triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((triple8 ((triple5 ((triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple7) -> (rule4 % int3)) ((triple5 ((triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
((triple13) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple15
Anne is white.
("Anne" "is" "white" "+")
((triple1 triple2) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple1 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple7) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple5 triple8) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple6 triple10) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple5 ((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple13) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple12 triple14) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple12 ((triple13) -> (rule4 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2