Charlie is nice. Fiona is big. Fiona is rough. All nice, kind people are cold. If someone is nice and cold then they are rough. All nice people are kind. All kind, big people are cold. If someone is green then they are cold. If someone is big then they are rough.
Charlie is nice.
("Charlie" "is" "nice" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
All nice, kind people are cold.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice and cold then they are rough.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
All nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All kind, big people are cold.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is big then they are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Charlie is nice.
True
1
proof
[(triple1)]
("Charlie" "is" "nice" "+")
triple1
Fiona is not big.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "big" "-")
triple2
Charlie is kind.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule1))]
("Charlie" "is" "cold" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule1))]
("Charlie" "is" "cold" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
True
6
proof
[(((triple1 ((triple1 ((triple1) -> rule3)) -> rule1)) -> rule2))]
("Charlie" "is" "rough" "+")
((triple1 ((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not rough.
False
6
inv-proof
[(((triple1 ((triple1 ((triple1) -> rule3)) -> rule1)) -> rule2))]
("Charlie" "is" "rough" "-")
((triple1 ((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Fiona is not cold.
Unknown
inv-rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Charlie is nice.[(triple1)] Fiona is big.[(triple2)] Fiona is rough.[(triple3 OR ((triple2) -> rule6))] @1: Charlie is kind.[(((triple1) -> rule3))] @2: Charlie is cold.[(((triple1 ((triple1) -> rule3)) -> rule1))] @3: Charlie is rough.[(((triple1 ((triple1 ((triple1) -> rule3)) -> rule1)) -> rule2))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Fiona is big.
("Fiona" "is" "big" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
((triple2) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1 ((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3