Bob is white. Charlie is red. Dave is young. Gary is big. If Charlie is young and Charlie is white then Charlie is big. If someone is young then they are nice. All nice people are big. All blue people are white. All white people are big. If someone is white and blue then they are red.
Bob is white.
("Bob" "is" "white" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
If Charlie is young and Charlie is white then Charlie is big.
((("Charlie" "is" "young" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "big" "+"))
If someone is young then they are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
All nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
All blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
All white people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is white and blue then they are red.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
Charlie is red.
True
1
proof
[(triple2)]
("Charlie" "is" "red" "+")
triple2
Gary is not big.
False
1
inv-proof
[(triple4)]
("Gary" "is" "big" "-")
triple4
Bob is big.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "big" "+")
((triple1) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "nice" "-")
((triple3) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Dave" "is" "big" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Dave" "is" "big" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "white" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "red" "+")
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "nice" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Bob is white.[(triple1)] Charlie is red.[(triple2)] Dave is young.[(triple3)] Gary is big.[(triple4)] @1: Bob is big.[(((triple1) -> rule5))] Dave is nice.[(((triple3) -> rule2))] @2: Dave is big.[(((((triple3) -> rule2)) -> rule3))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2