Charlie is white. Fiona is big. Harry is white. All kind, big people are smart. If Charlie is kind then Charlie is big. All white people are kind.
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Harry is white.
("Harry" "is" "white" "+")
All kind, big people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is kind then Charlie is big.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "big" "+"))
All white people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
Fiona is big.
True
1
proof
[(triple2)]
("Fiona" "is" "big" "+")
triple2
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
Harry is not kind.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "kind" "-")
((triple3) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Charlie is big.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not big.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "big" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
True
6
proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule2)) -> rule1))]
("Charlie" "is" "smart" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not smart.
False
6
inv-proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule2)) -> rule1))]
("Charlie" "is" "smart" "-")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "kind" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "smart" "+")
Fiona is not smart.
Unknown
inv-rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is white.[(triple1)] Fiona is big.[(triple2)] Harry is white.[(triple3)] @1: Charlie is kind.[(((triple1) -> rule3))] Harry is kind.[(((triple3) -> rule3))] @2: Charlie is big.[(((((triple1) -> rule3)) -> rule2))] @3: Charlie is smart.[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule2)) -> rule1))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Fiona is big.
("Fiona" "is" "big" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3