Dave is not red. Harry is cold. Big people are quiet. All quiet people are not cold. Cold people are round. Red people are not rough. If someone is cold and big then they are rough. Round people are red. If someone is rough and not round then they are red. If Dave is cold and Dave is red then Dave is nice.
Dave is not red.
("Dave" "is" "red" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are not cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "-"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Red people are not rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "-"))
If someone is cold and big then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is rough and not round then they are red.
((("someone" "is" "rough" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "red" "+"))
If Dave is cold and Dave is red then Dave is nice.
((("Dave" "is" "cold" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "nice" "+"))
Harry is cold.
True
1
proof
[(triple2)]
("Harry" "is" "cold" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple2)]
("Harry" "is" "cold" "-")
triple2
Harry is round.
True
2
proof
[(((triple2) -> rule3))]
("Harry" "is" "round" "+")
((triple2) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple2) -> rule3))]
("Harry" "is" "round" "-")
((triple2) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
True
3
proof
[(((((triple2) -> rule3)) -> rule6))]
("Harry" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not red.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule6))]
("Harry" "is" "red" "-")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not rough.
True
4
proof
[(((((((triple2) -> rule3)) -> rule6)) -> rule4))]
("Harry" "is" "rough" "-")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is rough.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule6)) -> rule4))]
("Harry" "is" "rough" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "nice" "+")
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "quiet" "-")
Harry is quiet.
Unknown
rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "quiet" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is not red.[(triple1)] Harry is cold.[(triple2)] @1: Harry is round.[(((triple2) -> rule3))] @2: Harry is red.[(((((triple2) -> rule3)) -> rule6))] @3: Harry is not rough.[(((((((triple2) -> rule3)) -> rule6)) -> rule4))]
Dave is not red.
("Dave" "is" "red" "-")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
((triple2) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not rough.
("Harry" "is" "rough" "-")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3