Anne is blue. Anne is young. Dave is not cold. Dave is not smart. Gary is blue. Gary is nice. Gary is not smart. Blue things are not cold. If something is smart and not young then it is kind. If something is rough then it is not kind. Cold things are not blue. All nice things are rough. Cold, young things are not rough. Blue things are nice. If something is cold then it is nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is not smart.
("Dave" "is" "smart" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
Blue things are not cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "-"))
If something is smart and not young then it is kind.
((("something" "is" "smart" "+") ("something" "is" "young" "~")) -> ("something" "is" "kind" "+"))
If something is rough then it is not kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "-"))
Cold things are not blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "-"))
All nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Cold, young things are not rough.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "-"))
Blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Gary is blue.
True
1
proof
[(triple5)]
("Gary" "is" "blue" "+")
triple5
Gary is smart.
False
1
inv-proof
[(triple7)]
("Gary" "is" "smart" "+")
triple7
Gary is rough.
True
2
proof
[(((triple6) -> rule5) OR ((((triple5) -> rule7)) -> rule5))]
("Gary" "is" "rough" "+")
((triple6) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple5) -> (rule7 % int2))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Anne is cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is rough.
True
3
proof
[(((((triple1) -> rule7)) -> rule5))]
("Anne" "is" "rough" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not rough.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule5))]
("Anne" "is" "rough" "-")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not kind.
True
4
proof
[(((((((triple1) -> rule7)) -> rule5)) -> rule3))]
("Anne" "is" "kind" "-")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is kind.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule5)) -> rule3))]
("Anne" "is" "kind" "+")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Dave is not rough.
Unknown
inv-rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "nice" "+")
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Anne is blue.[(triple1)] Anne is young.[(triple2)] Dave is not cold.[(triple3)] Dave is not smart.[(triple4)] Gary is blue.[(triple5)] Gary is nice.[(triple6 OR ((triple5) -> rule7))] Gary is not smart.[(triple7)] @1: Anne is nice.[(((triple1) -> rule7))] Anne is not cold.[(((triple1) -> rule1))] Gary is not cold.[(((triple5) -> rule1))] Gary is rough.[(((triple6) -> rule5) OR ((((triple5) -> rule7)) -> rule5))] @2: Anne is rough.[(((((triple1) -> rule7)) -> rule5))] Gary is not kind.[(((((triple6) -> rule5)) -> rule3) OR ((((((triple5) -> rule7)) -> rule5)) -> rule3))] @3: Anne is not kind.[(((((((triple1) -> rule7)) -> rule5)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Dave is not cold.
("Dave" "is" "cold" "-")
triple3
Dave is not smart.
("Dave" "is" "smart" "-")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
((triple5) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not smart.
("Gary" "is" "smart" "-")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not cold.
("Anne" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Gary is not cold.
("Gary" "is" "cold" "-")
((triple5) -> (rule1 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple6) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple5) -> (rule7 % int2))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Gary is not kind.
("Gary" "is" "kind" "-")
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((((triple5) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Anne is not kind.
("Anne" "is" "kind" "-")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3