Anne is green. Anne is quiet. Anne is not white. Charlie is blue. Charlie is not quiet. Charlie is rough. Charlie is not white. Dave is blue. Dave is cold. Dave is green. Dave is quiet. Dave is rough. Fiona is cold. Fiona is green. Fiona is quiet. Green, white people are rough. All quiet people are rough. All blue people are big. Green, cold people are blue. All white people are blue. If Charlie is rough then Charlie is blue. If someone is quiet and big then they are green. If Dave is blue and Dave is white then Dave is quiet.
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not white.
("Anne" "is" "white" "-")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Green, white people are rough.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
All quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
All blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Green, cold people are blue.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
All white people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is rough then Charlie is blue.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "blue" "+"))
If someone is quiet and big then they are green.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If Dave is blue and Dave is white then Dave is quiet.
((("Dave" "is" "blue" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "quiet" "+"))
Dave is quiet.
True
1
proof
[(triple11)]
("Dave" "is" "quiet" "+")
triple11
Dave is not blue.
False
1
inv-proof
[(triple8 OR ((triple10 triple9) -> rule4))]
("Dave" "is" "blue" "-")
triple8
((triple10 triple9) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Charlie is big.
True
2
proof
[(((triple4) -> rule3) OR ((((triple6) -> rule6)) -> rule3))]
("Charlie" "is" "big" "+")
((triple4) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Anne is not rough.
False
2
inv-proof
[(((triple2) -> rule2))]
("Anne" "is" "rough" "-")
((triple2) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Fiona is big.
True
4
proof
[(((((triple14 triple13) -> rule4)) -> rule3))]
("Fiona" "is" "big" "+")
((((triple14 triple13) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is not big.
False
4
inv-proof
[(((((triple14 triple13) -> rule4)) -> rule3))]
("Fiona" "is" "big" "-")
((((triple14 triple13) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "green" "-")
Anne is big.
Unknown
rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "blue" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Anne is green.[(triple1)] Anne is not white.[(triple3)] Anne is quiet.[(triple2)] Charlie is blue.[(triple4 OR ((triple6) -> rule6))] Charlie is not quiet.[(triple5)] Charlie is not white.[(triple7)] Charlie is rough.[(triple6)] Dave is blue.[(triple8 OR ((triple10 triple9) -> rule4))] Dave is cold.[(triple9)] Dave is green.[(triple10 OR ((triple11 ((triple8) -> rule3)) -> rule7))] Dave is quiet.[(triple11)] Dave is rough.[(triple12 OR ((triple11) -> rule2))] Fiona is cold.[(triple13)] Fiona is green.[(triple14)] Fiona is quiet.[(triple15)] @1: Anne is rough.[(((triple2) -> rule2))] Charlie is big.[(((triple4) -> rule3) OR ((((triple6) -> rule6)) -> rule3))] Dave is big.[(((triple8) -> rule3) OR ((((triple10 triple9) -> rule4)) -> rule3))] Fiona is blue.[(((triple14 triple13) -> rule4))] Fiona is rough.[(((triple15) -> rule2))] @2: Fiona is big.[(((((triple14 triple13) -> rule4)) -> rule3))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is not white.
("Anne" "is" "white" "-")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
((triple6) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple5
Charlie is not white.
("Charlie" "is" "white" "-")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Dave is blue.
("Dave" "is" "blue" "+")
triple8
((triple10 triple9) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple9
Dave is green.
("Dave" "is" "green" "+")
triple10
((triple11 ((triple8) -> (rule3 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple11
Dave is rough.
("Dave" "is" "rough" "+")
triple12
((triple11) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple13
Fiona is green.
("Fiona" "is" "green" "+")
triple14
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple15
Anne is rough.
("Anne" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple4) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((triple8) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple10 triple9) -> (rule4 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple14 triple13) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple15) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((((triple14 triple13) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2