Charlie is furry. Erin is not furry. Fiona is cold. All nice things are not quiet. Rough, cold things are nice. Nice, white things are not furry. If something is quiet and nice then it is cold. If something is furry then it is cold. All cold things are rough.
Charlie is furry.
("Charlie" "is" "furry" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Fiona is cold.
("Fiona" "is" "cold" "+")
All nice things are not quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "-"))
Rough, cold things are nice.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Nice, white things are not furry.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "-"))
If something is quiet and nice then it is cold.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
All cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Erin is not furry.
True
1
proof
[(triple2)]
("Erin" "is" "furry" "-")
triple2
Erin is furry.
False
1
inv-proof
[(triple2)]
("Erin" "is" "furry" "+")
triple2
Fiona is rough.
True
2
proof
[(((triple3) -> rule6))]
("Fiona" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is not rough.
False
2
inv-proof
[(((triple3) -> rule6))]
("Fiona" "is" "rough" "-")
((triple3) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Charlie is rough.
True
3
proof
[(((((triple1) -> rule5)) -> rule6))]
("Charlie" "is" "rough" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not rough.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule6))]
("Charlie" "is" "rough" "-")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
True
6
proof
[(((((((triple1) -> rule5)) -> rule6) ((triple1) -> rule5)) -> rule2))]
("Charlie" "is" "nice" "+")
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2)) ((triple1) -> (rule5 % int3))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Fiona is quiet.
False
5
inv-proof
[(((((((triple3) -> rule6) triple3) -> rule2)) -> rule1))]
("Fiona" "is" "quiet" "+")
((((((triple3) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is rough.
Unknown
rconc
[@2: Erin is rough.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Erin" "is" "rough" "+")
Erin is not nice.
Unknown
inv-rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Erin" "is" "nice" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Charlie is furry.[(triple1)] Erin is not furry.[(triple2)] Fiona is cold.[(triple3)] @1: Charlie is cold.[(((triple1) -> rule5))] Fiona is rough.[(((triple3) -> rule6))] @2: Charlie is rough.[(((((triple1) -> rule5)) -> rule6))] Fiona is nice.[(((((triple3) -> rule6) triple3) -> rule2))] @3: Charlie is nice.[(((((((triple1) -> rule5)) -> rule6) ((triple1) -> rule5)) -> rule2))] Fiona is not quiet.[(((((((triple3) -> rule6) triple3) -> rule2)) -> rule1))] @4: Charlie is not quiet.[(((((((((triple1) -> rule5)) -> rule6) ((triple1) -> rule5)) -> rule2)) -> rule1))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Erin is not furry.
("Erin" "is" "furry" "-")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple3) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2)) ((triple1) -> (rule5 % int3))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((((((triple3) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((((((((triple1) -> (rule5 % int4))) -> (rule6 % int3)) ((triple1) -> (rule5 % int4))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4