Anne is nice. Anne is red. Dave is not round. Nice, smart people are not furry. If someone is furry then they are young. Nice people are young. Blue people are not red. If Anne is young and Anne is not nice then Anne is not blue. All young people are smart.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Dave is not round.
("Dave" "is" "round" "-")
Nice, smart people are not furry.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "-"))
If someone is furry then they are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Blue people are not red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "-"))
If Anne is young and Anne is not nice then Anne is not blue.
((("Anne" "is" "young" "+") ("Anne" "is" "nice" "~")) -> ("Anne" "is" "blue" "-"))
All young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Dave is not round.
True
1
proof
[(triple3)]
("Dave" "is" "round" "-")
triple3
Dave is round.
False
1
inv-proof
[(triple3)]
("Dave" "is" "round" "+")
triple3
Anne is young.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "young" "+")
((triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "young" "-")
((triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not smart.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not furry.
True
5
proof
[(((triple1 ((((triple1) -> rule3)) -> rule6)) -> rule1))]
("Anne" "is" "furry" "-")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is furry.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule3)) -> rule6)) -> rule1))]
("Anne" "is" "furry" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is smart.
Unknown
rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Dave" "is" "smart" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is nice.[(triple1)] Anne is red.[(triple2)] Dave is not round.[(triple3)] @1: Anne is young.[(((triple1) -> rule3))] @2: Anne is smart.[(((((triple1) -> rule3)) -> rule6))] @3: Anne is not furry.[(((triple1 ((((triple1) -> rule3)) -> rule6)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Dave is not round.
("Dave" "is" "round" "-")
triple3
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not furry.
("Anne" "is" "furry" "-")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3