Dave is red. Harry is nice. If Dave is big then Dave is quiet. All red people are not nice. If someone is big then they are not red. If someone is red and not white then they are big. If Dave is quiet then Dave is cold. If someone is red and not nice then they are furry. Furry people are quiet. If someone is cold and big then they are not quiet.
Dave is red.
("Dave" "is" "red" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If Dave is big then Dave is quiet.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "quiet" "+"))
All red people are not nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "-"))
If someone is big then they are not red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "-"))
If someone is red and not white then they are big.
((("someone" "is" "red" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "big" "+"))
If Dave is quiet then Dave is cold.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "cold" "+"))
If someone is red and not nice then they are furry.
((("someone" "is" "red" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "furry" "+"))
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is cold and big then they are not quiet.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "-"))
Dave is red.
True
1
proof
[(triple1)]
("Dave" "is" "red" "+")
triple1
Harry is not nice.
False
1
inv-proof
[(triple2)]
("Harry" "is" "nice" "-")
triple2
Dave is not nice.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "nice" "-")
((triple1) -> (rule2 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is nice.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is furry.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule6))]
("Dave" "is" "furry" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
Dave is not furry.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule6))]
("Dave" "is" "furry" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
Dave is quiet.
True
5
proof
[(((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule7))]
("Dave" "is" "quiet" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is not quiet.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule7))]
("Dave" "is" "quiet" "-")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "furry" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "big" "+")
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is quiet.
Unknown
rconc
[@2: Harry is quiet.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Harry" "is" "quiet" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Dave is red.[(triple1)] Harry is nice.[(triple2)] @1: Dave is not nice.[(((triple1) -> rule2))] @2: Dave is furry.[(((triple1 ((triple1) -> rule2)) -> rule6))] @3: Dave is quiet.[(((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule7))] @4: Dave is cold.[(((((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule7)) -> rule5))]
Dave is red.
("Dave" "is" "red" "+")
triple1
Harry is nice.
("Harry" "is" "nice" "+")
triple2
Dave is not nice.
("Dave" "is" "nice" "-")
((triple1) -> (rule2 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple1 ((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not nice.
("Dave" "is" "nice" "-")
int4