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