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