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