Anne is big. Anne is blue. Anne is cold. Anne is furry. Anne is green. Anne is red. Dave is big. Dave is blue. Fiona is not big. Fiona is cold. Fiona is green. Gary is not green. If Dave is rough then Dave is blue. If something is red and green then it is blue. If something is rough and not cold then it is not big. All cold things are green. If something is big and cold then it is rough. All blue things are rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is not green.
("Gary" "is" "green" "-")
If Dave is rough then Dave is blue.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "blue" "+"))
If something is red and green then it is blue.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something is rough and not cold then it is not big.
((("something" "is" "rough" "+") ("something" "is" "cold" "~")) -> ("something" "is" "big" "-"))
All cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is big and cold then it is rough.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Dave is big.
True
1
proof
[(triple7)]
("Dave" "is" "big" "+")
triple7
Anne is not blue.
False
1
inv-proof
[(triple2 OR ((triple6 triple5) -> rule2) OR ((triple6 ((triple3) -> rule4)) -> rule2))]
("Anne" "is" "blue" "-")
triple2
((triple6 triple5) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple6 ((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is rough.
True
2
proof
[(((triple2) -> rule6) OR ((triple1 triple3) -> rule5) OR ((((triple6 triple5) -> rule2)) -> rule6) OR ((((triple6 ((triple3) -> rule4)) -> rule2)) -> rule6))]
("Anne" "is" "rough" "+")
((triple2) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple1 triple3) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple6 triple5) -> (rule2 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple6 ((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Dave is not rough.
False
2
inv-proof
[(((triple8) -> rule6))]
("Dave" "is" "rough" "-")
((triple8) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Fiona is not rough.
Unknown
inv-rconc
[@2: Fiona is rough.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is blue.
Unknown
rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple6 triple5) -> rule2) OR ((triple6 ((triple3) -> rule4)) -> rule2))] Anne is cold.[(triple3)] Anne is furry.[(triple4)] Anne is green.[(triple5 OR ((triple3) -> rule4))] Anne is red.[(triple6)] Dave is big.[(triple7)] Dave is blue.[(triple8)] Fiona is cold.[(triple10)] Fiona is green.[(triple11 OR ((triple10) -> rule4))] Fiona is not big.[(triple9)] Gary is not green.[(triple12)] @1: Anne is rough.[(((triple2) -> rule6) OR ((triple1 triple3) -> rule5) OR ((((triple6 triple5) -> rule2)) -> rule6) OR ((((triple6 ((triple3) -> rule4)) -> rule2)) -> rule6))] Dave is rough.[(((triple8) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple6 triple5) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple6 ((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
Anne is furry.
("Anne" "is" "furry" "+")
triple4
Anne is green.
("Anne" "is" "green" "+")
triple5
((triple3) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple6
Dave is big.
("Dave" "is" "big" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Fiona is cold.
("Fiona" "is" "cold" "+")
triple10
Fiona is green.
("Fiona" "is" "green" "+")
triple11
((triple10) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is not big.
("Fiona" "is" "big" "-")
triple9
Gary is not green.
("Gary" "is" "green" "-")
triple12
Anne is rough.
("Anne" "is" "rough" "+")
((triple2) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple1 triple3) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple6 triple5) -> (rule2 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple6 ((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((triple8) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1