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