Bob is kind. Charlie is cold. Dave is red. Fiona is young. All young people are blue. All kind, nice people are young. Nice, blue people are white. All nice people are white. All nice, kind people are blue. All young, blue people are nice.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is young.
("Fiona" "is" "young" "+")
All young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
All kind, nice people are young.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Nice, blue people are white.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
All nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
All nice, kind people are blue.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
All young, blue people are nice.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Charlie is cold.
True
1
proof
[(triple2)]
("Charlie" "is" "cold" "+")
triple2
Fiona is not young.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "young" "-")
triple4
Fiona is blue.
True
2
proof
[(((triple4) -> rule1))]
("Fiona" "is" "blue" "+")
((triple4) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is not blue.
False
2
inv-proof
[(((triple4) -> rule1))]
("Fiona" "is" "blue" "-")
((triple4) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is nice.
True
4
proof
[(((triple4 ((triple4) -> rule1)) -> rule6))]
("Fiona" "is" "nice" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is not nice.
False
4
inv-proof
[(((triple4 ((triple4) -> rule1)) -> rule6))]
("Fiona" "is" "nice" "-")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
True
5
proof
[(((((triple4 ((triple4) -> rule1)) -> rule6)) -> rule4) OR ((((triple4 ((triple4) -> rule1)) -> rule6) ((triple4) -> rule1)) -> rule3))]
("Fiona" "is" "white" "+")
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule6 % int2)) ((triple4) -> (rule1 % int3))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is not white.
False
5
inv-proof
[(((((triple4 ((triple4) -> rule1)) -> rule6)) -> rule4) OR ((((triple4 ((triple4) -> rule1)) -> rule6) ((triple4) -> rule1)) -> rule3))]
("Fiona" "is" "white" "-")
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule6 % int2)) ((triple4) -> (rule1 % int3))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Bob" "is" "young" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "young" "+")
Dave is not blue.
Unknown
inv-rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "blue" "-")
Bob is nice.
Unknown
rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Bob is kind.[(triple1)] Charlie is cold.[(triple2)] Dave is red.[(triple3)] Fiona is young.[(triple4)] @1: Fiona is blue.[(((triple4) -> rule1))] @2: Fiona is nice.[(((triple4 ((triple4) -> rule1)) -> rule6))] @3: Fiona is white.[(((((triple4 ((triple4) -> rule1)) -> rule6)) -> rule4) OR ((((triple4 ((triple4) -> rule1)) -> rule6) ((triple4) -> rule1)) -> rule3))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Fiona is young.
("Fiona" "is" "young" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple4) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule6 % int2)) ((triple4) -> (rule1 % int3))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3