Anne is smart. Bob is kind. Charlie is blue. Erin is red. Blue people are rough. If someone is kind and smart then they are rough. Round people are not red. If someone is blue and round then they are kind. If someone is rough then they are round. Smart, white people are round.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Erin is red.
("Erin" "is" "red" "+")
Blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind and smart then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Round people are not red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "-"))
If someone is blue and round then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If someone is rough then they are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
Smart, white people are round.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Erin is red.
True
1
proof
[(triple4)]
("Erin" "is" "red" "+")
triple4
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
triple1
Charlie is rough.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "rough" "-")
((triple3) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
True
3
proof
[(((((triple3) -> rule1)) -> rule5))]
("Charlie" "is" "round" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not round.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule5))]
("Charlie" "is" "round" "-")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not red.
True
4
proof
[(((((((triple3) -> rule1)) -> rule5)) -> rule3))]
("Charlie" "is" "red" "-")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not kind.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule1)) -> rule5)) -> rule4))]
("Charlie" "is" "kind" "-")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "kind" "-")
Bob is round.
Unknown
rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Bob" "is" "round" "+")
Anne is not rough.
Unknown
inv-rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "kind" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is smart.[(triple1)] Bob is kind.[(triple2)] Charlie is blue.[(triple3)] Erin is red.[(triple4)] @1: Charlie is rough.[(((triple3) -> rule1))] @2: Charlie is round.[(((((triple3) -> rule1)) -> rule5))] @3: Charlie is kind.[(((triple3 ((((triple3) -> rule1)) -> rule5)) -> rule4))] Charlie is not red.[(((((((triple3) -> rule1)) -> rule5)) -> rule3))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not red.
("Charlie" "is" "red" "-")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3