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