Charlie is red. Erin is red. Fiona is white. All red people are nice. If someone is nice then they are white. If someone is white then they are smart. If someone is blue then they are young. Smart people are blue. If Fiona is rough then Fiona is young. If Fiona is not nice and Fiona is not white then Fiona is not rough. If someone is red and not smart then they are rough.
Charlie is red.
("Charlie" "is" "red" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is white.
("Fiona" "is" "white" "+")
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If someone is white then they are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is blue then they are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If Fiona is rough then Fiona is young.
((("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "young" "+"))
If Fiona is not nice and Fiona is not white then Fiona is not rough.
((("Fiona" "is" "nice" "~") ("Fiona" "is" "white" "~")) -> ("Fiona" "is" "rough" "-"))
If someone is red and not smart then they are rough.
((("someone" "is" "red" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "rough" "+"))
Fiona is white.
True
1
proof
[(triple3)]
("Fiona" "is" "white" "+")
triple3
Erin is not red.
False
1
inv-proof
[(triple2)]
("Erin" "is" "red" "-")
triple2
Erin is nice.
True
2
proof
[(((triple2) -> rule1))]
("Erin" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "nice" "-")
((triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Fiona is not blue.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule5))]
("Fiona" "is" "blue" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "rough" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "rough" "+")
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Charlie is red.[(triple1)] Erin is red.[(triple2)] Fiona is white.[(triple3)] @1: Charlie is nice.[(((triple1) -> rule1))] Erin is nice.[(((triple2) -> rule1))] Fiona is smart.[(((triple3) -> rule3))] @2: Charlie is white.[(((((triple1) -> rule1)) -> rule2))] Erin is white.[(((((triple2) -> rule1)) -> rule2))] Fiona is blue.[(((((triple3) -> rule3)) -> rule5))] @3: Charlie is smart.[(((((((triple1) -> rule1)) -> rule2)) -> rule3))] Erin is smart.[(((((((triple2) -> rule1)) -> rule2)) -> rule3))] Fiona is young.[(((((((triple3) -> rule3)) -> rule5)) -> rule4))] @4: Charlie is blue.[(((((((((triple1) -> rule1)) -> rule2)) -> rule3)) -> rule5))] Erin is blue.[(((((((((triple2) -> rule1)) -> rule2)) -> rule3)) -> rule5))] @5: Charlie is young.[(((((((((((triple1) -> rule1)) -> rule2)) -> rule3)) -> rule5)) -> rule4))] Erin is young.[(((((((((((triple2) -> rule1)) -> rule2)) -> rule3)) -> rule5)) -> rule4))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
((((((((triple2) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5
Erin is young.
("Erin" "is" "young" "+")
((((((((((triple2) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
int5