Charlie is not cold. Charlie is quiet. Charlie is smart. Dave is kind. Dave is red. Dave is smart. Erin is big. If someone is quiet then they are kind. If Erin is smart then Erin is quiet. If someone is kind then they are not rough. If someone is big then they are not red. If Charlie is not rough then Charlie is big. If Dave is cold and Dave is not kind then Dave is not red.
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
If someone is quiet then they are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If Erin is smart then Erin is quiet.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "quiet" "+"))
If someone is kind then they are not rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "-"))
If someone is big then they are not red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "-"))
If Charlie is not rough then Charlie is big.
((("Charlie" "is" "rough" "~")) -> ("Charlie" "is" "big" "+"))
If Dave is cold and Dave is not kind then Dave is not red.
((("Dave" "is" "cold" "+") ("Dave" "is" "kind" "~")) -> ("Dave" "is" "red" "-"))
Dave is red.
True
1
proof
[(triple5)]
("Dave" "is" "red" "+")
triple5
Dave is not smart.
False
1
inv-proof
[(triple6)]
("Dave" "is" "smart" "-")
triple6
Charlie is kind.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "kind" "+")
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is red.
False
2
inv-proof
[(((triple7) -> rule4))]
("Erin" "is" "red" "+")
((triple7) -> (rule4 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Charlie is not rough.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "rough" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
True
4
proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule5))]
("Charlie" "is" "big" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not big.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule5))]
("Charlie" "is" "big" "-")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is kind.
Unknown
rconc
[@2: Erin is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Erin" "is" "kind" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Charlie is not cold.[(triple1)] Charlie is quiet.[(triple2)] Charlie is smart.[(triple3)] Dave is kind.[(triple4)] Dave is red.[(triple5)] Dave is smart.[(triple6)] Erin is big.[(triple7)] @1: Charlie is kind.[(((triple2) -> rule1))] Dave is not rough.[(((triple4) -> rule3))] Erin is not red.[(((triple7) -> rule4))] @2: Charlie is not rough.[(((((triple2) -> rule1)) -> rule3))] @3: Charlie is big.[(((((((triple2) -> rule1)) -> rule3)) -> rule5))] @4: Charlie is not red.[(((((((((triple2) -> rule1)) -> rule3)) -> rule5)) -> rule4))]
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Erin is big.
("Erin" "is" "big" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is not rough.
("Dave" "is" "rough" "-")
((triple4) -> (rule3 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Erin is not red.
("Erin" "is" "red" "-")
((triple7) -> (rule4 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not red.
("Charlie" "is" "red" "-")
((((((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not rough.
("Charlie" "is" "rough" "-")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4