Bob is big. Bob is not red. Bob is white. Dave is kind. Dave is red. Gary is red. Gary is white. If something is red and not big then it is not blue. If something is young then it is white. Big things are smart. All white things are smart. Kind things are young. If something is kind and not blue then it is young.
Bob is big.
("Bob" "is" "big" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is white.
("Bob" "is" "white" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
If something is red and not big then it is not blue.
((("something" "is" "red" "+") ("something" "is" "big" "~")) -> ("something" "is" "blue" "-"))
If something is young then it is white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
All white things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is kind and not blue then it is young.
((("something" "is" "kind" "+") ("something" "is" "blue" "~")) -> ("something" "is" "young" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Dave is not kind.
False
1
inv-proof
[(triple4)]
("Dave" "is" "kind" "-")
triple4
Bob is smart.
True
2
proof
[(((triple1) -> rule3) OR ((triple3) -> rule4))]
("Bob" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple3) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple7) -> rule4))]
("Gary" "is" "smart" "-")
((triple7) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Dave is white.
True
3
proof
[(((((triple4) -> rule5)) -> rule2))]
("Dave" "is" "white" "+")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not white.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule2))]
("Dave" "is" "white" "-")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
True
4
proof
[(((((((triple4) -> rule5)) -> rule2)) -> rule4))]
("Dave" "is" "smart" "+")
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not smart.
False
4
inv-proof
[(((((((triple4) -> rule5)) -> rule2)) -> rule4))]
("Dave" "is" "smart" "-")
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "young" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "young" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Bob is big.[(triple1)] Bob is not red.[(triple2)] Bob is white.[(triple3)] Dave is kind.[(triple4)] Dave is red.[(triple5)] Gary is red.[(triple6)] Gary is white.[(triple7)] @1: Bob is smart.[(((triple1) -> rule3) OR ((triple3) -> rule4))] Dave is young.[(((triple4) -> rule5))] Gary is smart.[(((triple7) -> rule4))] @2: Dave is white.[(((((triple4) -> rule5)) -> rule2))] @3: Dave is smart.[(((((((triple4) -> rule5)) -> rule2)) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is not red.
("Bob" "is" "red" "-")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple3) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple4) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple7) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3