Anne is cold. Anne is kind. Anne is round. Fiona is not rough. Fiona is not round. Gary is kind. Gary is young. If someone is kind then they are smart. If someone is rough and not kind then they are smart. If someone is green and cold then they are young. All smart people are green. Young, kind people are cold. If Fiona is not smart then Fiona is round.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Fiona is not rough.
("Fiona" "is" "rough" "-")
Fiona is not round.
("Fiona" "is" "round" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is kind then they are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is rough and not kind then they are smart.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "smart" "+"))
If someone is green and cold then they are young.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Young, kind people are cold.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If Fiona is not smart then Fiona is round.
((("Fiona" "is" "smart" "~")) -> ("Fiona" "is" "round" "+"))
Anne is round.
True
1
proof
[(triple3)]
("Anne" "is" "round" "+")
triple3
Anne is not kind.
False
1
inv-proof
[(triple2)]
("Anne" "is" "kind" "-")
triple2
Gary is smart.
True
2
proof
[(((triple6) -> rule1))]
("Gary" "is" "smart" "+")
((triple6) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple2) -> rule1))]
("Anne" "is" "smart" "-")
((triple2) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is green.
True
3
proof
[(((((triple6) -> rule1)) -> rule4))]
("Gary" "is" "green" "+")
((((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is not green.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4))]
("Anne" "is" "green" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
True
5
proof
[(((((((triple2) -> rule1)) -> rule4) triple1) -> rule3))]
("Anne" "is" "young" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not young.
False
5
inv-proof
[(((((((triple2) -> rule1)) -> rule4) triple1) -> rule3))]
("Anne" "is" "young" "-")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Fiona is not young.
Unknown
inv-rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Fiona" "is" "young" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is green.
Unknown
rconc
[@2: Fiona is green.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Fiona" "is" "green" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Anne is kind.[(triple2)] Anne is round.[(triple3)] Fiona is not rough.[(triple4)] Fiona is not round.[(triple5)] Gary is kind.[(triple6)] Gary is young.[(triple7)] @1: Anne is smart.[(((triple2) -> rule1))] Gary is cold.[(((triple7 triple6) -> rule5))] Gary is smart.[(((triple6) -> rule1))] @2: Anne is green.[(((((triple2) -> rule1)) -> rule4))] Gary is green.[(((((triple6) -> rule1)) -> rule4))] @3: Anne is young.[(((((((triple2) -> rule1)) -> rule4) triple1) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple4
Fiona is not round.
("Fiona" "is" "round" "-")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple7 triple6) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple6) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3