Bob is not big. Bob is not white. Charlie is blue. Charlie is red. Charlie is young. Dave is big. Dave is blue. Gary is not blue. Gary is furry. Gary is not nice. Gary is red. Gary is white. If Dave is young then Dave is white. If someone is blue then they are young. White, blue people are nice. If Charlie is blue and Charlie is furry then Charlie is red. All nice, young people are red. If someone is white and not young then they are red.
Bob is not big.
("Bob" "is" "big" "-")
Bob is not white.
("Bob" "is" "white" "-")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is not nice.
("Gary" "is" "nice" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
If Dave is young then Dave is white.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "white" "+"))
If someone is blue then they are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
White, blue people are nice.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is blue and Charlie is furry then Charlie is red.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "red" "+"))
All nice, young people are red.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is white and not young then they are red.
((("someone" "is" "white" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "red" "+"))
Charlie is blue.
True
1
proof
[(triple3)]
("Charlie" "is" "blue" "+")
triple3
Gary is not furry.
False
1
inv-proof
[(triple9)]
("Gary" "is" "furry" "-")
triple9
Dave is young.
True
2
proof
[(((triple7) -> rule2))]
("Dave" "is" "young" "+")
((triple7) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple7) -> rule2))]
("Dave" "is" "young" "-")
((triple7) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
True
3
proof
[(((((triple7) -> rule2)) -> rule1))]
("Dave" "is" "white" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not white.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule1))]
("Dave" "is" "white" "-")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
True
5
proof
[(((((((triple7) -> rule2)) -> rule1) triple7) -> rule3))]
("Dave" "is" "nice" "+")
((((((triple7) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not nice.
False
5
inv-proof
[(((((((triple7) -> rule2)) -> rule1) triple7) -> rule3))]
("Dave" "is" "nice" "-")
((((((triple7) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "young" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not red.
Unknown
inv-rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Bob" "is" "red" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "nice" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Bob is not big.[(triple1)] Bob is not white.[(triple2)] Charlie is blue.[(triple3)] Charlie is red.[(triple4)] Charlie is young.[(triple5 OR ((triple3) -> rule2))] Dave is big.[(triple6)] Dave is blue.[(triple7)] Gary is furry.[(triple9)] Gary is not blue.[(triple8)] Gary is not nice.[(triple10)] Gary is red.[(triple11)] Gary is white.[(triple12)] @1: Dave is young.[(((triple7) -> rule2))] @2: Dave is white.[(((((triple7) -> rule2)) -> rule1))] @3: Dave is nice.[(((((((triple7) -> rule2)) -> rule1) triple7) -> rule3))] @4: Dave is red.[(((((((((triple7) -> rule2)) -> rule1) triple7) -> rule3) ((triple7) -> rule2)) -> rule5))]
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is not white.
("Bob" "is" "white" "-")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
((triple3) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is blue.
("Dave" "is" "blue" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple9
Gary is not blue.
("Gary" "is" "blue" "-")
triple8
Gary is not nice.
("Gary" "is" "nice" "-")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
Dave is young.
("Dave" "is" "young" "+")
((triple7) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple7) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((((((triple7) -> (rule2 % int4))) -> (rule1 % int3)) triple7) -> (rule3 % int2)) ((triple7) -> (rule2 % int4))) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4