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