Bob is nice. Bob is red. Dave is young. If something is white and not red then it is green. All young things are green. If Dave is kind then Dave is green. If Bob is green and Bob is blue then Bob is not kind. If Bob is not nice and Bob is not red then Bob is white. If Bob is kind and Bob is young then Bob is white. All kind, red things are young. If something is red then it is kind.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is white and not red then it is green.
((("something" "is" "white" "+") ("something" "is" "red" "~")) -> ("something" "is" "green" "+"))
All young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If Dave is kind then Dave is green.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "green" "+"))
If Bob is green and Bob is blue then Bob is not kind.
((("Bob" "is" "green" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "kind" "-"))
If Bob is not nice and Bob is not red then Bob is white.
((("Bob" "is" "nice" "~") ("Bob" "is" "red" "~")) -> ("Bob" "is" "white" "+"))
If Bob is kind and Bob is young then Bob is white.
((("Bob" "is" "kind" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "white" "+"))
All kind, red things are young.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is red then it is kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Dave is young.
True
1
proof
[(triple3)]
("Dave" "is" "young" "+")
triple3
Dave is not young.
False
1
inv-proof
[(triple3)]
("Dave" "is" "young" "-")
triple3
Bob is kind.
True
2
proof
[(((triple2) -> rule8))]
("Bob" "is" "kind" "+")
((triple2) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple2) -> rule8))]
("Bob" "is" "kind" "-")
((triple2) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
True
4
proof
[(((((triple2) -> rule8) triple2) -> rule7))]
("Bob" "is" "young" "+")
((((triple2) -> (rule8 % int2)) triple2) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not young.
False
4
inv-proof
[(((((triple2) -> rule8) triple2) -> rule7))]
("Bob" "is" "young" "-")
((((triple2) -> (rule8 % int2)) triple2) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
True
5
proof
[(((((((triple2) -> rule8) triple2) -> rule7)) -> rule2))]
("Bob" "is" "green" "+")
((((((triple2) -> (rule8 % int3)) triple2) -> (rule7 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not white.
False
7
inv-proof
[(((((triple2) -> rule8) ((((triple2) -> rule8) triple2) -> rule7)) -> rule6))]
("Bob" "is" "white" "-")
((((triple2) -> (rule8 % int3)) ((((triple2) -> (rule8 % int3)) triple2) -> (rule7 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "kind" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Bob is nice.[(triple1)] Bob is red.[(triple2)] Dave is young.[(triple3)] @1: Bob is kind.[(((triple2) -> rule8))] Dave is green.[(((triple3) -> rule2))] @2: Bob is young.[(((((triple2) -> rule8) triple2) -> rule7))] @3: Bob is green.[(((((((triple2) -> rule8) triple2) -> rule7)) -> rule2))] Bob is white.[(((((triple2) -> rule8) ((((triple2) -> rule8) triple2) -> rule7)) -> rule6))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple2) -> (rule8 % int2)) triple2) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple2) -> (rule8 % int3)) triple2) -> (rule7 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((((triple2) -> (rule8 % int3)) ((((triple2) -> (rule8 % int3)) triple2) -> (rule7 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3