Anne is kind. Anne is red. Anne is rough. Bob is red. Bob is rough. Bob is not smart. Bob is white. Dave is red. Dave is smart. Dave is young. All rough, young things are white. Nice things are white. If something is rough then it is young. If something is white then it is not nice. If something is smart and not white then it is red. If Bob is not nice then Bob is red.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is white.
("Bob" "is" "white" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
All rough, young things are white.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
Nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If something is rough then it is young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is white then it is not nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "-"))
If something is smart and not white then it is red.
((("something" "is" "smart" "+") ("something" "is" "white" "~")) -> ("something" "is" "red" "+"))
If Bob is not nice then Bob is red.
((("Bob" "is" "nice" "~")) -> ("Bob" "is" "red" "+"))
Anne is red.
True
1
proof
[(triple2)]
("Anne" "is" "red" "+")
triple2
Bob is not red.
False
1
inv-proof
[(triple4 OR ((((triple7) -> rule4)) -> rule6) OR ((((((triple5 ((triple5) -> rule3)) -> rule1)) -> rule4)) -> rule6))]
("Bob" "is" "red" "-")
triple4
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
int2
((((((triple5 ((triple5) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Anne is young.
True
2
proof
[(((triple3) -> rule3))]
("Anne" "is" "young" "+")
((triple3) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is nice.
False
2
inv-proof
[(((triple7) -> rule4) OR ((((triple5 ((triple5) -> rule3)) -> rule1)) -> rule4))]
("Bob" "is" "nice" "+")
((triple7) -> (rule4 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
((((triple5 ((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Anne is white.
True
4
proof
[(((triple3 ((triple3) -> rule3)) -> rule1))]
("Anne" "is" "white" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not white.
False
4
inv-proof
[(((triple3 ((triple3) -> rule3)) -> rule1))]
("Anne" "is" "white" "-")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "white" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Anne is red.[(triple2)] Anne is rough.[(triple3)] Bob is not smart.[(triple6)] Bob is red.[(triple4 OR ((((triple7) -> rule4)) -> rule6) OR ((((((triple5 ((triple5) -> rule3)) -> rule1)) -> rule4)) -> rule6))] Bob is rough.[(triple5)] Bob is white.[(triple7 OR ((triple5 ((triple5) -> rule3)) -> rule1))] Dave is red.[(triple8)] Dave is smart.[(triple9)] Dave is young.[(triple10)] @1: Anne is young.[(((triple3) -> rule3))] Bob is not nice.[(((triple7) -> rule4) OR ((((triple5 ((triple5) -> rule3)) -> rule1)) -> rule4))] Bob is young.[(((triple5) -> rule3))] @2: Anne is white.[(((triple3 ((triple3) -> rule3)) -> rule1))] @3: Anne is not nice.[(((((triple3 ((triple3) -> rule3)) -> rule1)) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Bob is not smart.
("Bob" "is" "smart" "-")
triple6
Bob is red.
("Bob" "is" "red" "+")
triple4
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
int2
((((((triple5 ((triple5) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple5 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple8
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Anne is young.
("Anne" "is" "young" "+")
((triple3) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
((triple7) -> (rule4 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
((((triple5 ((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
((triple5) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not nice.
("Anne" "is" "nice" "-")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3