Bob is nice. Charlie is round. Young, red people are blue. Round, red people are not young. All round people are red. If someone is round and rough then they are not cold. If Charlie is not young then Charlie is not cold. If Bob is rough and Bob is not cold then Bob is nice.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Young, red people are blue.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Round, red people are not young.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "-"))
All round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is round and rough then they are not cold.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "-"))
If Charlie is not young then Charlie is not cold.
((("Charlie" "is" "young" "~")) -> ("Charlie" "is" "cold" "-"))
If Bob is rough and Bob is not cold then Bob is nice.
((("Bob" "is" "rough" "+") ("Bob" "is" "cold" "~")) -> ("Bob" "is" "nice" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Charlie is not round.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "round" "-")
triple2
Charlie is red.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "red" "+")
((triple2) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "red" "-")
((triple2) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not young.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule2))]
("Charlie" "is" "young" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is young.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule2))]
("Charlie" "is" "young" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not cold.
True
5
proof
[(((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule5))]
("Charlie" "is" "cold" "-")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is cold.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule5))]
("Charlie" "is" "cold" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "blue" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "+")
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "red" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Bob is nice.[(triple1)] Charlie is round.[(triple2)] @1: Charlie is red.[(((triple2) -> rule3))] @2: Charlie is not young.[(((triple2 ((triple2) -> rule3)) -> rule2))] @3: Charlie is not cold.[(((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule5))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
((triple2) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not cold.
("Charlie" "is" "cold" "-")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3