Bob is blue. Charlie is young. Dave is blue. Gary is white. Young things are white. If something is white then it is blue. If something is big and young then it is nice. White things are big. All green things are nice. All kind, green things are young.
Bob is blue.
("Bob" "is" "blue" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Gary is white.
("Gary" "is" "white" "+")
Young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is white then it is blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If something is big and young then it is nice.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
All kind, green things are young.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Dave is not blue.
False
1
inv-proof
[(triple3)]
("Dave" "is" "blue" "-")
triple3
Charlie is white.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "white" "+")
((triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "white" "-")
((triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("Charlie" "is" "blue" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not blue.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("Charlie" "is" "blue" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
True
5
proof
[(((((((triple2) -> rule1)) -> rule4) triple2) -> rule3))]
("Charlie" "is" "nice" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not nice.
False
5
inv-proof
[(((((((triple2) -> rule1)) -> rule4) triple2) -> rule3))]
("Charlie" "is" "nice" "-")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Gary is not nice.
Unknown
inv-rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Gary" "is" "nice" "-")
Dave is white.
Unknown
rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Dave" "is" "white" "+")
Bob is not big.
Unknown
inv-rconc
[@3: Bob is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule6 <- FAIL)]]
("Bob" "is" "big" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "young" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Bob is blue.[(triple1)] Charlie is young.[(triple2)] Dave is blue.[(triple3)] Gary is white.[(triple4)] @1: Charlie is white.[(((triple2) -> rule1))] Gary is big.[(((triple4) -> rule4))] Gary is blue.[(((triple4) -> rule2))] @2: Charlie is big.[(((((triple2) -> rule1)) -> rule4))] Charlie is blue.[(((((triple2) -> rule1)) -> rule2))] @3: Charlie is nice.[(((((((triple2) -> rule1)) -> rule4) triple2) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Gary is white.
("Gary" "is" "white" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple4) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple4) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3