Anne is big. Dave is kind. Fiona is not green. If someone is white then they are not green. Big people are white. All green people are not white. All nice people are rough. Big, rough people are nice. If someone is white and not nice then they are kind. If someone is big and not green then they are kind. All green people are kind.
Anne is big.
("Anne" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is not green.
("Fiona" "is" "green" "-")
If someone is white then they are not green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "-"))
Big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
All green people are not white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "-"))
All nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Big, rough people are nice.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is white and not nice then they are kind.
((("someone" "is" "white" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "kind" "+"))
If someone is big and not green then they are kind.
((("someone" "is" "big" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "kind" "+"))
All green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Dave is kind.
True
1
proof
[(triple2)]
("Dave" "is" "kind" "+")
triple2
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is white.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "white" "+")
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "white" "-")
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not green.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "green" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is kind.
True
5
proof
[(((triple1 ((((triple1) -> rule2)) -> rule1)) -> rule7))]
("Anne" "is" "kind" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not green.
("Anne" "is" "green" "-")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not kind.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule2)) -> rule1)) -> rule7))]
("Anne" "is" "kind" "-")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not green.
("Anne" "is" "green" "-")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not nice.
Unknown
inv-rconc
[@2: Anne is nice.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Anne" "is" "nice" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "+")
Dave is not rough.
Unknown
inv-rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Dave" "is" "rough" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "kind" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Anne is big.[(triple1)] Dave is kind.[(triple2)] Fiona is not green.[(triple3)] @1: Anne is white.[(((triple1) -> rule2))] @2: Anne is not green.[(((((triple1) -> rule2)) -> rule1))] @3: Anne is kind.[(((triple1 ((((triple1) -> rule2)) -> rule1)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Fiona is not green.
("Fiona" "is" "green" "-")
triple3
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not green.
("Anne" "is" "green" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not green.
("Anne" "is" "green" "-")
int2
Anne is white.
("Anne" "is" "white" "+")
int3