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