Anne is not kind. Charlie is cold. Fiona is kind. Harry is blue. If Anne is blue then Anne is not kind. If someone is cold then they are kind. If Fiona is smart then Fiona is red. If Fiona is quiet then Fiona is not red. Kind people are red. Green people are blue. All red people are not blue. If Charlie is kind then Charlie is quiet.
Anne is not kind.
("Anne" "is" "kind" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If Anne is blue then Anne is not kind.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "kind" "-"))
If someone is cold then they are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If Fiona is smart then Fiona is red.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "red" "+"))
If Fiona is quiet then Fiona is not red.
((("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "red" "-"))
Kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
Green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
All red people are not blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "-"))
If Charlie is kind then Charlie is quiet.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "quiet" "+"))
Fiona is kind.
True
1
proof
[(triple3)]
("Fiona" "is" "kind" "+")
triple3
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Charlie is kind.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple3) -> rule5))]
("Fiona" "is" "red" "-")
((triple3) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not blue.
True
3
proof
[(((((triple3) -> rule5)) -> rule7))]
("Fiona" "is" "blue" "-")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is blue.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule7))]
("Fiona" "is" "blue" "+")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Charlie is not blue.
True
4
proof
[(((((((triple2) -> rule2)) -> rule5)) -> rule7))]
("Charlie" "is" "blue" "-")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is blue.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule5)) -> rule7))]
("Charlie" "is" "blue" "+")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "blue" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "kind" "+")
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "red" "-")
Harry is red.
Unknown
rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Harry" "is" "red" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Anne is not kind.[(triple1)] Charlie is cold.[(triple2)] Fiona is kind.[(triple3)] Harry is blue.[(triple4)] @1: Charlie is kind.[(((triple2) -> rule2))] Fiona is red.[(((triple3) -> rule5))] @2: Charlie is quiet.[(((((triple2) -> rule2)) -> rule8))] Charlie is red.[(((((triple2) -> rule2)) -> rule5))] Fiona is not blue.[(((((triple3) -> rule5)) -> rule7))] @3: Charlie is not blue.[(((((((triple2) -> rule2)) -> rule5)) -> rule7))]
Anne is not kind.
("Anne" "is" "kind" "-")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple3) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Fiona is not blue.
("Fiona" "is" "blue" "-")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Charlie is not blue.
("Charlie" "is" "blue" "-")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3