Anne is young. Charlie is not green. Fiona is cold. If Fiona is young then Fiona is nice. If something is young then it is blue. If something is smart and kind then it is blue. If Anne is kind then Anne is young. All green things are not smart. If Anne is blue and Anne is young then Anne is green. All kind things are green. All blue things are kind.
Anne is young.
("Anne" "is" "young" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Fiona is cold.
("Fiona" "is" "cold" "+")
If Fiona is young then Fiona is nice.
((("Fiona" "is" "young" "+")) -> ("Fiona" "is" "nice" "+"))
If something is young then it is blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is smart and kind then it is blue.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If Anne is kind then Anne is young.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "young" "+"))
All green things are not smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "-"))
If Anne is blue and Anne is young then Anne is green.
((("Anne" "is" "blue" "+") ("Anne" "is" "young" "+")) -> ("Anne" "is" "green" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Anne is young.
True
1
proof
[(triple1)]
("Anne" "is" "young" "+")
triple1
Charlie is green.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "green" "+")
triple2
Anne is blue.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "blue" "-")
((triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule6) OR ((((((triple1) -> rule2)) -> rule8)) -> rule7))]
("Anne" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is not green.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule6) OR ((((((triple1) -> rule2)) -> rule8)) -> rule7))]
("Anne" "is" "green" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is not smart.
True
5
proof
[(((((((triple1) -> rule2) triple1) -> rule6)) -> rule5) OR ((((((((triple1) -> rule2)) -> rule8)) -> rule7)) -> rule5))]
("Anne" "is" "smart" "-")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is smart.
False
5
inv-proof
[(((((((triple1) -> rule2) triple1) -> rule6)) -> rule5) OR ((((((((triple1) -> rule2)) -> rule8)) -> rule7)) -> rule5))]
("Anne" "is" "smart" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is nice.
Unknown
rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "nice" "+")
Charlie is not kind.
Unknown
inv-rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule8 <- rule2 <- FAIL)]]
("Charlie" "is" "kind" "-")
Fiona is kind.
Unknown
rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule8 <- rule2 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Anne is young.[(triple1)] Charlie is not green.[(triple2)] Fiona is cold.[(triple3)] @1: Anne is blue.[(((triple1) -> rule2))] @2: Anne is green.[(((((triple1) -> rule2) triple1) -> rule6) OR ((((((triple1) -> rule2)) -> rule8)) -> rule7))] Anne is kind.[(((((triple1) -> rule2)) -> rule8))] @3: Anne is not smart.[(((((((triple1) -> rule2) triple1) -> rule6)) -> rule5) OR ((((((((triple1) -> rule2)) -> rule8)) -> rule7)) -> rule5))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Charlie is not green.
("Charlie" "is" "green" "-")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not smart.
("Anne" "is" "smart" "-")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4