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