Charlie is blue. Erin is nice. Gary is young. All nice people are blue. If someone is green and not blue then they are rough. If someone is blue then they are not red. If someone is blue and rough then they are red. Rough people are red. If someone is blue and not red then they are young.
Charlie is blue.
("Charlie" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is young.
("Gary" "is" "young" "+")
All nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is green and not blue then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "rough" "+"))
If someone is blue then they are not red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "-"))
If someone is blue and rough then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
Rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and not red then they are young.
((("someone" "is" "blue" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "young" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
Charlie is not red.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "red" "-")
((triple1) -> (rule3 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is red.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "red" "+")
((triple1) -> (rule3 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is young.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule6))]
("Charlie" "is" "young" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not red.
("Charlie" "is" "red" "-")
int2
Erin is red.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Erin" "is" "red" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is young.
True
6
proof
[(((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule6))]
("Erin" "is" "young" "+")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not red.
("Erin" "is" "red" "-")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not young.
False
6
inv-proof
[(((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule6))]
("Erin" "is" "young" "-")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not red.
("Erin" "is" "red" "-")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "rough" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "rough" "+")
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "blue" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "rough" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Charlie is blue.[(triple1)] Erin is nice.[(triple2)] Gary is young.[(triple3)] @1: Charlie is not red.[(((triple1) -> rule3))] Erin is blue.[(((triple2) -> rule1))] @2: Charlie is young.[(((triple1 ((triple1) -> rule3)) -> rule6))] Erin is not red.[(((((triple2) -> rule1)) -> rule3))] @3: Erin is young.[(((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule6))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Charlie is not red.
("Charlie" "is" "red" "-")
((triple1) -> (rule3 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not red.
("Charlie" "is" "red" "-")
int2
Erin is not red.
("Erin" "is" "red" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not red.
("Erin" "is" "red" "-")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3