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